diff options
Diffstat (limited to 'src/coq')
| -rw-r--r-- | src/coq/Axioms.v | 49 | ||||
| -rw-r--r-- | src/coq/Semantics.v | 212 | ||||
| -rw-r--r-- | src/coq/Syntax.v | 31 |
3 files changed, 164 insertions, 128 deletions
diff --git a/src/coq/Axioms.v b/src/coq/Axioms.v new file mode 100644 index 00000000..f89bc1e8 --- /dev/null +++ b/src/coq/Axioms.v @@ -0,0 +1,49 @@ +(* Copyright (c) 2009, Adam Chlipala + * All rights reserved. + * + * Redistribution and use in source and binary forms, with or without + * modification, are permitted provided that the following conditions are met: + * + * - Redistributions of source code must retain the above copyright notice, + * this list of conditions and the following disclaimer. + * - Redistributions in binary form must reproduce the above copyright notice, + * this list of conditions and the following disclaimer in the documentation + * and/or other materials provided with the distribution. + * - The names of contributors may not be used to endorse or promote products + * derived from this software without specific prior written permission. + * + * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" + * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE + * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE + * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER OR CONTRIBUTORS BE + * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR + * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF + * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS + * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN + * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) + * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE + * POSSIBILITY OF SUCH DAMAGE. + *) + +Require Import Syntax. + +Set Implicit Arguments. + + +Axiom ext_eq : forall dom ran (f g : forall x : dom, ran x), + (forall x, f x = g x) + -> f = g. + +Theorem ext_eq_forall : forall dom (f g : forall x : dom, Type), + (forall x, f x = g x) + -> (forall x, f x) = (forall x, g x). + intros. + rewrite (ext_eq _ f g H); reflexivity. +Qed. + +Theorem ext_eq_forallS : forall dom (f g : forall x : dom, Set), + (forall x, f x = g x) + -> (forall x, f x) = (forall x, g x). + intros. + rewrite (ext_eq _ f g H); reflexivity. +Qed. diff --git a/src/coq/Semantics.v b/src/coq/Semantics.v index c3e99b5d..a60ae102 100644 --- a/src/coq/Semantics.v +++ b/src/coq/Semantics.v @@ -25,33 +25,21 @@ * POSSIBILITY OF SUCH DAMAGE. *) -Require Import Arith List Omega TheoryList. +Require Import Arith List TheoryList. +Require Import Axioms. Require Import Syntax. Set Implicit Arguments. -Section row'. - Variable A : Type. +Definition row (T : Type) := list (name * T). - Inductive row' : list name -> Type := - | Nil : row' nil - | Cons : forall n ls, A -> AllS (lt n) ls -> row' ls -> row' (n :: ls). -End row'. - -Implicit Arguments Nil [A]. - -Record row (A : Type) : Type := Row { - keys : list name; - data : row' A keys -}. - -Inductive record' : forall ls, row' Set ls -> Set := -| RNil : record' Nil -| RCons : forall n ls (T : Set) (pf : AllS (lt n) ls) r, T -> record' r -> record' (Cons T pf r). - -Definition record (r : row Set) := record' (data r). +Fixpoint record (r : row Set) : Set := + match r with + | nil => unit + | (_, T) :: r' => T * record r' + end%type. Fixpoint kDen (k : kind) : Type := match k with @@ -61,82 +49,10 @@ Fixpoint kDen (k : kind) : Type := | KRecord k1 => row (kDen k1) end. -Axiom cheat : forall T, T. - -Fixpoint cinsert (n : name) (ls : list name) {struct ls} : list name := - match ls with - | nil => n :: nil - | n' :: ls' => - if eq_nat_dec n n' - then ls - else if le_lt_dec n n' - then n :: ls - else n' :: cinsert n ls' - end. - -Hint Constructors AllS. -Hint Extern 1 (_ < _) => omega. - -Lemma insert_front' : forall n n', - n <> n' - -> n <= n' - -> forall ls, AllS (lt n') ls - -> AllS (lt n) ls. - induction 3; auto. -Qed. - -Lemma insert_front : forall n n', - n <> n' - -> n <= n' - -> forall ls, AllS (lt n') ls - -> AllS (lt n) (n' :: ls). - Hint Resolve insert_front'. - eauto. -Qed. - -Lemma insert_continue : forall n n', - n <> n' - -> n' < n - -> forall ls, AllS (lt n') ls - -> AllS (lt n') (cinsert n ls). - induction 3; simpl; auto; - repeat (match goal with - | [ |- context[if ?E then _ else _] ] => destruct E - end; auto). -Qed. - -Fixpoint insert T (n : name) (v : T) ls (r : row' T ls) {struct r} : row' T (cinsert n ls) := - match r in row' _ ls return row' T (cinsert n ls) with - | Nil => Cons (n := n) v (allS_nil _) Nil - | Cons n' ls' v' pf r' => - match eq_nat_dec n n' as END - return row' _ (if END then _ else _) with - | left _ => Cons (n := n') v' pf r' - | right pfNe => - match le_lt_dec n n' as LLD - return row' _ (if LLD then _ else _) with - | left pfLe => Cons (n := n) v (insert_front pfNe pfLe pf) (Cons (n := n') v' pf r') - | right pfLt => Cons (n := n') v' (insert_continue pfNe pfLt pf) (insert n v r') - end - end - end. - -Fixpoint cconcat (ls1 ls2 : list name) {struct ls1} : list name := - match ls1 with - | nil => ls2 - | n :: ls1' => cinsert n (cconcat ls1' ls2) - end. - -Fixpoint concat T ls1 ls2 (r1 : row' T ls1) (r2 : row' T ls2) {struct r1} : row' T (cconcat ls1 ls2) := - match r1 in row' _ ls1 return row' _ (cconcat ls1 _) with - | Nil => r2 - | Cons n _ v _ r1' => insert n v (concat r1' r2) - end. - -Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') ls (r : row' T ls) {struct r} : T' := +Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') (r : row T) {struct r} : T' := match r with - | Nil => i - | Cons n _ v _ r' => f n v (cfold f i r') + | nil => i + | (n, v) :: r' => f n v (cfold f i r') end. Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := @@ -148,9 +64,107 @@ Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := | CApp _ _ c1 c2 => (cDen c1) (cDen c2) | Name n => n | TRecord c1 => record (cDen c1) - | CEmpty _ => Row Nil - | CSingle _ c1 c2 => Row (Cons (n := cDen c1) (cDen c2) (allS_nil _) Nil) - | CConcat _ c1 c2 => Row (concat (data (cDen c1)) (data (cDen c2))) - | CFold k1 k2 => fun f i r => cfold f i (data r) + | CEmpty _ => nil + | CSingle _ c1 c2 => (cDen c1, cDen c2) :: nil + | CConcat _ c1 c2 => cDen c1 ++ cDen c2 + | CFold k1 k2 => @cfold _ _ | CGuarded _ _ _ _ c => cDen c end. + +Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2', + subs c1 c2 c2' + -> cDen (c2 (cDen c1)) = cDen c2'. + induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq); + repeat match goal with + | [ H : _ |- _ ] => rewrite H + end; intuition. +Qed. + +Definition disjoint T (r1 r2 : row T) := + AllS (fun p1 => AllS (fun p2 => fst p1 <> fst p2) r2) r1. +Definition dvar k (c1 c2 : con kDen (KRecord k)) := + disjoint (cDen c1) (cDen c2). + +Lemma AllS_app : forall T P (ls2 : list T), + AllS P ls2 + -> forall ls1, AllS P ls1 + -> AllS P (ls1 ++ ls2). + induction 2; simpl; intuition. +Qed. + +Lemma AllS_weaken : forall T (P P' : T -> Prop), + (forall x, P x -> P' x) + -> forall ls, + AllS P ls + -> AllS P' ls. + induction 2; simpl; intuition. +Qed. + +Theorem disjoint_symm : forall T (r1 r2 : row T), + disjoint r1 r2 + -> disjoint r2 r1. + Hint Constructors AllS. + Hint Resolve AllS_weaken. + + unfold disjoint; induction r2; simpl; intuition. + constructor. + eapply AllS_weaken; eauto. + intuition. + inversion H0; auto. + + apply IHr2. + eapply AllS_weaken; eauto. + intuition. + inversion H0; auto. +Qed. + +Lemma map_id : forall k (r : row k), + cfold (fun x x0 (x1 : row _) => (x, x0) :: x1) nil r = r. + induction r; simpl; intuition; + match goal with + | [ H : _ |- _ ] => rewrite H + end; intuition. +Qed. + +Lemma map_dist : forall T1 T2 (f : T1 -> T2) (r2 r1 : row T1), + cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil (r1 ++ r2) + = cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r1 + ++ cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r2. + induction r1; simpl; intuition; + match goal with + | [ H : _ |- _ ] => rewrite H + end; intuition. +Qed. + +Lemma fold_fuse : forall T1 T2 T3 (f : name -> T1 -> T2 -> T2) (i : T2) (f' : T3 -> T1) (c : row T3), + cfold f i (cfold (fun x x0 (x1 : row _) => (x, f' x0) :: x1) nil c) + = cfold (fun x x0 => f x (f' x0)) i c. + induction c; simpl; intuition; + match goal with + | [ H : _ |- _ ] => rewrite <- H + end; intuition. +Qed. + +Scheme deq_mut := Minimality for deq Sort Prop +with disj_mut := Minimality for disj Sort Prop. + +Theorem deq_correct : forall k (c1 c2 : con kDen k), + deq dvar c1 c2 + -> cDen c1 = cDen c2. + Hint Resolve map_id map_dist fold_fuse AllS_app disjoint_symm. + Hint Extern 1 (_ = _) => unfold row; symmetry; apply app_ass. + + apply (deq_mut (dvar := dvar) + (fun k (c1 c2 : con kDen k) => + cDen c1 = cDen c2) + (fun k (c1 c2 : con kDen (KRecord k)) => + disjoint (cDen c1) (cDen c2))); + simpl; intuition; + repeat (match goal with + | [ H : _ |- _ ] => rewrite H + | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H) + end; simpl; intuition); try congruence; unfold disjoint in *; intuition; + fold kDen in *; repeat match goal with + | [ H : AllS _ (_ :: _) |- _ ] => inversion H; clear H; subst; simpl in * + end; auto. +Qed. diff --git a/src/coq/Syntax.v b/src/coq/Syntax.v index 786751d0..d73f5361 100644 --- a/src/coq/Syntax.v +++ b/src/coq/Syntax.v @@ -145,15 +145,14 @@ Section vars. | Eq_Concat_Empty : forall k c, deq (CConcat (CEmpty k) c) c - | Eq_Concat_Comm : forall k (c1 c2 : con (KRecord k)), - deq (CConcat c1 c2) (CConcat c2 c1) | Eq_Concat_Assoc : forall k (c1 c2 c3 : con (KRecord k)), deq (CConcat c1 (CConcat c2 c3)) (CConcat (CConcat c1 c2) c3) | Eq_Fold_Empty : forall k1 k2 f i, deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CEmpty _)) i | Eq_Fold_Cons : forall k1 k2 f i c1 c2 c3, - deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3)) + disj (CSingle c1 c2) c3 + -> deq (CApp (CApp (CApp (CFold k1 k2) f) i) (CConcat (CSingle c1 c2) c3)) (CApp (CApp (CApp f c1) c2) (CApp (CApp (CApp (CFold k1 k2) f) i) c3)) | Eq_Guarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), @@ -184,30 +183,4 @@ Section vars. (CApp (CApp (CApp (CFold k3 k2) (CAbs (fun x1 => CAbs (fun x2 => CApp (CApp f (CVar x1)) (CApp f' (CVar x2)))))) i) c). - - Inductive wf : forall k, con k -> Type := - | HK_CVar : forall k (x : cvar k), - wf (CVar x) - | HK_Arrow : forall c1 c2, - wf c1 -> wf c2 -> wf (Arrow c1 c2) - | HK_Poly : forall k (c1 : cvar k -> _), - (forall x, wf (c1 x)) -> wf (Poly c1) - | HK_CAbs : forall k1 k2 (c1 : cvar k1 -> con k2), - (forall x, wf (c1 x)) -> wf (CAbs c1) - | HK_CApp : forall k1 k2 (c1 : con (KArrow k1 k2)) c2, - wf c1 -> wf c2 -> wf (CApp c1 c2) - | HK_Name : forall X, - wf (Name X) - | HK_TRecord : forall c, - wf c -> wf (TRecord c) - | HK_CEmpty : forall k, - wf (CEmpty k) - | HK_CSingle : forall k c1 (c2 : con k), - wf c1 -> wf c2 -> wf (CSingle c1 c2) - | HK_CConcat : forall k (c1 c2 : con (KRecord k)), - wf c2 -> wf c2 -> disj c1 c2 -> wf (CConcat c1 c2) - | HK_CFold : forall k1 k2, - wf (CFold k1 k2) - | HK_CGuarded : forall k1 k2 (c1 c2 : con (KRecord k1)) (c : con k2), - wf c1 -> wf c2 -> (disj c1 c2 -> wf c) -> wf (CGuarded c1 c2 c). End vars. |