adamc@615: (* Copyright (c) 2009, Adam Chlipala
adamc@615:  * All rights reserved.
adamc@615:  *
adamc@615:  * Redistribution and use in source and binary forms, with or without
adamc@615:  * modification, are permitted provided that the following conditions are met:
adamc@615:  *
adamc@615:  * - Redistributions of source code must retain the above copyright notice,
adamc@615:  *   this list of conditions and the following disclaimer.
adamc@615:  * - Redistributions in binary form must reproduce the above copyright notice,
adamc@615:  *   this list of conditions and the following disclaimer in the documentation
adamc@615:  *   and/or other materials provided with the distribution.
adamc@615:  * - The names of contributors may not be used to endorse or promote products
adamc@615:  *   derived from this software without specific prior written permission.
adamc@615:  *
adamc@615:  * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
adamc@615:  * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
adamc@615:  * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
adamc@615:  * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE
adamc@615:  * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR 
adamc@615:  * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
adamc@615:  * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
adamc@615:  * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
adamc@615:  * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
adamc@615:  * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
adamc@615:  * POSSIBILITY OF SUCH DAMAGE.
adamc@615:  *)
adamc@615: 
adamc@616: Require Import Arith List TheoryList.
adamc@615: 
adamc@616: Require Import Axioms.
adamc@615: Require Import Syntax.
adamc@615: 
adamc@615: Set Implicit Arguments.
adamc@615: 
adamc@615: 
adamc@616: Definition row (T : Type) := list (name * T).
adamc@615: 
adamc@616: Fixpoint record (r : row Set) : Set :=
adamc@616:   match r with
adamc@616:     | nil => unit
adamc@616:     | (_, T) :: r' => T * record r'
adamc@616:   end%type.
adamc@615: 
adamc@615: Fixpoint kDen (k : kind) : Type :=
adamc@615:   match k with
adamc@615:     | KType => Set
adamc@615:     | KName => name
adamc@615:     | KArrow k1 k2 => kDen k1 -> kDen k2
adamc@615:     | KRecord k1 => row (kDen k1)
adamc@615:   end.
adamc@615: 
adamc@616: Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') (r : row T) {struct r} : T' :=
adamc@615:   match r with
adamc@616:     | nil => i
adamc@616:     | (n, v) :: r' => f n v (cfold f i r')
adamc@615:   end.
adamc@615: 
adamc@615: Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
adamc@615:   match c in con _ k return kDen k with
adamc@615:     | CVar _ x => x
adamc@615:     | Arrow c1 c2 => cDen c1 -> cDen c2
adamc@615:     | Poly _ c1 => forall x, cDen (c1 x)
adamc@615:     | CAbs _ _ c1 => fun x => cDen (c1 x)
adamc@615:     | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
adamc@615:     | Name n => n
adamc@615:     | TRecord c1 => record (cDen c1)
adamc@616:     | CEmpty _ => nil
adamc@616:     | CSingle _ c1 c2 => (cDen c1, cDen c2) :: nil
adamc@616:     | CConcat _ c1 c2 => cDen c1 ++ cDen c2
adamc@616:     | CFold k1 k2 => @cfold _ _
adamc@615:     | CGuarded _ _ _ _ c => cDen c
adamc@615:   end.
adamc@616: 
adamc@616: Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
adamc@616:   subs c1 c2 c2'
adamc@616:   -> cDen (c2 (cDen c1)) = cDen c2'.
adamc@616:   induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq);
adamc@616:     repeat match goal with
adamc@616:              | [ H : _ |- _ ] => rewrite H
adamc@616:            end; intuition.
adamc@616: Qed.
adamc@616: 
adamc@616: Definition disjoint T (r1 r2 : row T) :=
adamc@616:   AllS (fun p1 => AllS (fun p2 => fst p1 <> fst p2) r2) r1.
adamc@616: Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
adamc@616:   disjoint (cDen c1) (cDen c2).
adamc@616: 
adamc@616: Lemma AllS_app : forall T P (ls2 : list T),
adamc@616:   AllS P ls2
adamc@616:   -> forall ls1, AllS P ls1
adamc@616:     -> AllS P (ls1 ++ ls2).
adamc@616:   induction 2; simpl; intuition.
adamc@616: Qed.
adamc@616: 
adamc@616: Lemma AllS_weaken : forall T (P P' : T -> Prop),
adamc@616:   (forall x, P x -> P' x)
adamc@616:   -> forall ls,
adamc@616:     AllS P ls
adamc@616:     -> AllS P' ls.
adamc@616:   induction 2; simpl; intuition.
adamc@616: Qed.
adamc@616: 
adamc@616: Theorem disjoint_symm : forall T (r1 r2 : row T),
adamc@616:   disjoint r1 r2
adamc@616:   -> disjoint r2 r1.
adamc@616:   Hint Constructors AllS.
adamc@616:   Hint Resolve AllS_weaken.
adamc@616:   
adamc@616:   unfold disjoint; induction r2; simpl; intuition.
adamc@616:   constructor.
adamc@616:   eapply AllS_weaken; eauto.
adamc@616:   intuition.
adamc@616:   inversion H0; auto.
adamc@616: 
adamc@616:   apply IHr2.
adamc@616:   eapply AllS_weaken; eauto.
adamc@616:   intuition.
adamc@616:   inversion H0; auto.
adamc@616: Qed.  
adamc@616: 
adamc@616: Lemma map_id : forall k (r : row k),
adamc@616:   cfold (fun x x0 (x1 : row _) => (x, x0) :: x1) nil r = r.
adamc@616:   induction r; simpl; intuition;
adamc@616:     match goal with
adamc@616:       | [ H : _ |- _ ] => rewrite H
adamc@616:     end; intuition.
adamc@616: Qed.
adamc@616: 
adamc@616: Lemma map_dist : forall T1 T2 (f : T1 -> T2) (r2 r1 : row T1),
adamc@616:   cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil (r1 ++ r2)
adamc@616:   = cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r1
adamc@616:   ++ cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r2.
adamc@616:   induction r1; simpl; intuition;
adamc@616:     match goal with
adamc@616:       | [ H : _ |- _ ] => rewrite H
adamc@616:     end; intuition.
adamc@616: Qed.
adamc@616: 
adamc@616: Lemma fold_fuse : forall T1 T2 T3 (f : name -> T1 -> T2 -> T2) (i : T2) (f' : T3 -> T1) (c : row T3),
adamc@616:   cfold f i (cfold (fun x x0 (x1 : row _) => (x, f' x0) :: x1) nil c)
adamc@616:   = cfold (fun x x0 => f x (f' x0)) i c.
adamc@616:   induction c; simpl; intuition;
adamc@616:     match goal with
adamc@616:       | [ H : _ |- _ ] => rewrite <- H
adamc@616:     end; intuition.
adamc@616: Qed.
adamc@616: 
adamc@616: Scheme deq_mut := Minimality for deq Sort Prop
adamc@616: with disj_mut := Minimality for disj Sort Prop.
adamc@616: 
adamc@616: Theorem deq_correct : forall k (c1 c2 : con kDen k),
adamc@616:   deq dvar c1 c2
adamc@616:   -> cDen c1 = cDen c2.
adamc@616:   Hint Resolve map_id map_dist fold_fuse AllS_app disjoint_symm.
adamc@616:   Hint Extern 1 (_ = _) => unfold row; symmetry; apply app_ass.
adamc@616: 
adamc@616:   apply (deq_mut (dvar := dvar)
adamc@616:     (fun k (c1 c2 : con kDen k) =>
adamc@616:       cDen c1 = cDen c2)
adamc@616:     (fun k (c1 c2 : con kDen (KRecord k)) =>
adamc@616:       disjoint (cDen c1) (cDen c2)));
adamc@616:   simpl; intuition;
adamc@616:     repeat (match goal with
adamc@616:               | [ H : _ |- _ ] => rewrite H
adamc@616:               | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
adamc@616:             end; simpl; intuition); try congruence; unfold disjoint in *; intuition;
adamc@616:     fold kDen in *; repeat match goal with
adamc@616:                              | [ H : AllS _ (_ :: _) |- _ ] => inversion H; clear H; subst; simpl in *
adamc@616:                            end; auto.
adamc@616: Qed.