Mercurial > urweb

comparison src/coq/Semantics.v @ 616:d26d1f3acfd6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Semantics for ordered rows only
author Adam Chlipala <adamc@hcoop.net>
date Wed, 18 Feb 2009 09:32:17 -0500
parents 3c77133afd9a
children 5b358e8f9f09
comparison
equal deleted inserted replaced
615:3c77133afd9a 616:d26d1f3acfd6
23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) 23 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE 24 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
25 * POSSIBILITY OF SUCH DAMAGE. 25 * POSSIBILITY OF SUCH DAMAGE.
26 *) 26 *)
27 27
28 Require Import Arith List Omega TheoryList. 28 Require Import Arith List TheoryList.
29 29
30 Require Import Axioms.
30 Require Import Syntax. 31 Require Import Syntax.
31 32
32 Set Implicit Arguments. 33 Set Implicit Arguments.
33 34
34 35
35 Section row'. 36 Definition row (T : Type) := list (name * T).
36 Variable A : Type.
37 37
38 Inductive row' : list name -> Type := 38 Fixpoint record (r : row Set) : Set :=
39 | Nil : row' nil 39 match r with
40 | Cons : forall n ls, A -> AllS (lt n) ls -> row' ls -> row' (n :: ls). 40 | nil => unit
41 End row'. 41 | (_, T) :: r' => T * record r'
42 42 end%type.
43 Implicit Arguments Nil [A].
44
45 Record row (A : Type) : Type := Row {
46 keys : list name;
47 data : row' A keys
48 }.
49
50 Inductive record' : forall ls, row' Set ls -> Set :=
51 | RNil : record' Nil
52 | RCons : forall n ls (T : Set) (pf : AllS (lt n) ls) r, T -> record' r -> record' (Cons T pf r).
53
54 Definition record (r : row Set) := record' (data r).
55 43
56 Fixpoint kDen (k : kind) : Type := 44 Fixpoint kDen (k : kind) : Type :=
57 match k with 45 match k with
58 | KType => Set 46 | KType => Set
59 | KName => name 47 | KName => name
60 | KArrow k1 k2 => kDen k1 -> kDen k2 48 | KArrow k1 k2 => kDen k1 -> kDen k2
61 | KRecord k1 => row (kDen k1) 49 | KRecord k1 => row (kDen k1)
62 end. 50 end.
63 51
64 Axiom cheat : forall T, T. 52 Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') (r : row T) {struct r} : T' :=
65
66 Fixpoint cinsert (n : name) (ls : list name) {struct ls} : list name :=
67 match ls with
68 | nil => n :: nil
69 | n' :: ls' =>
70 if eq_nat_dec n n'
71 then ls
72 else if le_lt_dec n n'
73 then n :: ls
74 else n' :: cinsert n ls'
75 end.
76
77 Hint Constructors AllS.
78 Hint Extern 1 (_ < _) => omega.
79
80 Lemma insert_front' : forall n n',
81 n <> n'
82 -> n <= n'
83 -> forall ls, AllS (lt n') ls
84 -> AllS (lt n) ls.
85 induction 3; auto.
86 Qed.
87
88 Lemma insert_front : forall n n',
89 n <> n'
90 -> n <= n'
91 -> forall ls, AllS (lt n') ls
92 -> AllS (lt n) (n' :: ls).
93 Hint Resolve insert_front'.
94 eauto.
95 Qed.
96
97 Lemma insert_continue : forall n n',
98 n <> n'
99 -> n' < n
100 -> forall ls, AllS (lt n') ls
101 -> AllS (lt n') (cinsert n ls).
102 induction 3; simpl; auto;
103 repeat (match goal with
104 | [ |- context[if ?E then _ else _] ] => destruct E
105 end; auto).
106 Qed.
107
108 Fixpoint insert T (n : name) (v : T) ls (r : row' T ls) {struct r} : row' T (cinsert n ls) :=
109 match r in row' _ ls return row' T (cinsert n ls) with
110 | Nil => Cons (n := n) v (allS_nil _) Nil
111 | Cons n' ls' v' pf r' =>
112 match eq_nat_dec n n' as END
113 return row' _ (if END then _ else _) with
114 | left _ => Cons (n := n') v' pf r'
115 | right pfNe =>
116 match le_lt_dec n n' as LLD
117 return row' _ (if LLD then _ else _) with
118 | left pfLe => Cons (n := n) v (insert_front pfNe pfLe pf) (Cons (n := n') v' pf r')
119 | right pfLt => Cons (n := n') v' (insert_continue pfNe pfLt pf) (insert n v r')
120 end
121 end
122 end.
123
124 Fixpoint cconcat (ls1 ls2 : list name) {struct ls1} : list name :=
125 match ls1 with
126 | nil => ls2
127 | n :: ls1' => cinsert n (cconcat ls1' ls2)
128 end.
129
130 Fixpoint concat T ls1 ls2 (r1 : row' T ls1) (r2 : row' T ls2) {struct r1} : row' T (cconcat ls1 ls2) :=
131 match r1 in row' _ ls1 return row' _ (cconcat ls1 _) with
132 | Nil => r2
133 | Cons n _ v _ r1' => insert n v (concat r1' r2)
134 end.
135
136 Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') ls (r : row' T ls) {struct r} : T' :=
137 match r with 53 match r with
138 | Nil => i 54 | nil => i
139 | Cons n _ v _ r' => f n v (cfold f i r') 55 | (n, v) :: r' => f n v (cfold f i r')
140 end. 56 end.
141 57
142 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := 58 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
143 match c in con _ k return kDen k with 59 match c in con _ k return kDen k with
144 | CVar _ x => x 60 | CVar _ x => x
146 | Poly _ c1 => forall x, cDen (c1 x) 62 | Poly _ c1 => forall x, cDen (c1 x)
147 | CAbs _ _ c1 => fun x => cDen (c1 x) 63 | CAbs _ _ c1 => fun x => cDen (c1 x)
148 | CApp _ _ c1 c2 => (cDen c1) (cDen c2) 64 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
149 | Name n => n 65 | Name n => n
150 | TRecord c1 => record (cDen c1) 66 | TRecord c1 => record (cDen c1)
151 | CEmpty _ => Row Nil 67 | CEmpty _ => nil
152 | CSingle _ c1 c2 => Row (Cons (n := cDen c1) (cDen c2) (allS_nil _) Nil) 68 | CSingle _ c1 c2 => (cDen c1, cDen c2) :: nil
153 | CConcat _ c1 c2 => Row (concat (data (cDen c1)) (data (cDen c2))) 69 | CConcat _ c1 c2 => cDen c1 ++ cDen c2
154 | CFold k1 k2 => fun f i r => cfold f i (data r) 70 | CFold k1 k2 => @cfold _ _
155 | CGuarded _ _ _ _ c => cDen c 71 | CGuarded _ _ _ _ c => cDen c
156 end. 72 end.
73
74 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
75 subs c1 c2 c2'
76 -> cDen (c2 (cDen c1)) = cDen c2'.
77 induction 1; simpl; intuition; try (apply ext_eq_forallS || apply ext_eq);
78 repeat match goal with
79 | [ H : _ |- _ ] => rewrite H
80 end; intuition.
81 Qed.
82
83 Definition disjoint T (r1 r2 : row T) :=
84 AllS (fun p1 => AllS (fun p2 => fst p1 <> fst p2) r2) r1.
85 Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
86 disjoint (cDen c1) (cDen c2).
87
88 Lemma AllS_app : forall T P (ls2 : list T),
89 AllS P ls2
90 -> forall ls1, AllS P ls1
91 -> AllS P (ls1 ++ ls2).
92 induction 2; simpl; intuition.
93 Qed.
94
95 Lemma AllS_weaken : forall T (P P' : T -> Prop),
96 (forall x, P x -> P' x)
97 -> forall ls,
98 AllS P ls
99 -> AllS P' ls.
100 induction 2; simpl; intuition.
101 Qed.
102
103 Theorem disjoint_symm : forall T (r1 r2 : row T),
104 disjoint r1 r2
105 -> disjoint r2 r1.
106 Hint Constructors AllS.
107 Hint Resolve AllS_weaken.
108
109 unfold disjoint; induction r2; simpl; intuition.
110 constructor.
111 eapply AllS_weaken; eauto.
112 intuition.
113 inversion H0; auto.
114
115 apply IHr2.
116 eapply AllS_weaken; eauto.
117 intuition.
118 inversion H0; auto.
119 Qed.
120
121 Lemma map_id : forall k (r : row k),
122 cfold (fun x x0 (x1 : row _) => (x, x0) :: x1) nil r = r.
123 induction r; simpl; intuition;
124 match goal with
125 | [ H : _ |- _ ] => rewrite H
126 end; intuition.
127 Qed.
128
129 Lemma map_dist : forall T1 T2 (f : T1 -> T2) (r2 r1 : row T1),
130 cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil (r1 ++ r2)
131 = cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r1
132 ++ cfold (fun x x0 (x1 : row _) => (x, f x0) :: x1) nil r2.
133 induction r1; simpl; intuition;
134 match goal with
135 | [ H : _ |- _ ] => rewrite H
136 end; intuition.
137 Qed.
138
139 Lemma fold_fuse : forall T1 T2 T3 (f : name -> T1 -> T2 -> T2) (i : T2) (f' : T3 -> T1) (c : row T3),
140 cfold f i (cfold (fun x x0 (x1 : row _) => (x, f' x0) :: x1) nil c)
141 = cfold (fun x x0 => f x (f' x0)) i c.
142 induction c; simpl; intuition;
143 match goal with
144 | [ H : _ |- _ ] => rewrite <- H
145 end; intuition.
146 Qed.
147
148 Scheme deq_mut := Minimality for deq Sort Prop
149 with disj_mut := Minimality for disj Sort Prop.
150
151 Theorem deq_correct : forall k (c1 c2 : con kDen k),
152 deq dvar c1 c2
153 -> cDen c1 = cDen c2.
154 Hint Resolve map_id map_dist fold_fuse AllS_app disjoint_symm.
155 Hint Extern 1 (_ = _) => unfold row; symmetry; apply app_ass.
156
157 apply (deq_mut (dvar := dvar)
158 (fun k (c1 c2 : con kDen k) =>
159 cDen c1 = cDen c2)
160 (fun k (c1 c2 : con kDen (KRecord k)) =>
161 disjoint (cDen c1) (cDen c2)));
162 simpl; intuition;
163 repeat (match goal with
164 | [ H : _ |- _ ] => rewrite H
165 | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
166 end; simpl; intuition); try congruence; unfold disjoint in *; intuition;
167 fold kDen in *; repeat match goal with
168 | [ H : AllS _ (_ :: _) |- _ ] => inversion H; clear H; subst; simpl in *
169 end; auto.
170 Qed.