Mercurial > urweb

comparison src/coq/Semantics.v @ 617:5b358e8f9f09

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
map-only syntax and semantics
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 11:23:24 -0500
parents d26d1f3acfd6
children be88d2d169f6
comparison
equal deleted inserted replaced
616:d26d1f3acfd6 617:5b358e8f9f09
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 TheoryList.
29
30 Require Import Axioms. 28 Require Import Axioms.
31 Require Import Syntax. 29 Require Import Syntax.
32 30
33 Set Implicit Arguments. 31 Set Implicit Arguments.
34 32
35 33
36 Definition row (T : Type) := list (name * T). 34 Definition row (A : Type) : Type := name -> option A.
37 35
38 Fixpoint record (r : row Set) : Set := 36 Definition record (r : row Set) := forall n, match r n with
39 match r with 37 | None => unit
40 | nil => unit 38 | Some T => T
41 | (_, T) :: r' => T * record r' 39 end.
42 end%type.
43 40
44 Fixpoint kDen (k : kind) : Type := 41 Fixpoint kDen (k : kind) : Type :=
45 match k with 42 match k with
46 | KType => Set 43 | KType => Set
47 | KName => name 44 | KName => name
48 | KArrow k1 k2 => kDen k1 -> kDen k2 45 | KArrow k1 k2 => kDen k1 -> kDen k2
49 | KRecord k1 => row (kDen k1) 46 | KRecord k1 => row (kDen k1)
50 end.
51
52 Fixpoint cfold T T' (f : name -> T -> T' -> T') (i : T') (r : row T) {struct r} : T' :=
53 match r with
54 | nil => i
55 | (n, v) :: r' => f n v (cfold f i r')
56 end. 47 end.
57 48
58 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k := 49 Fixpoint cDen k (c : con kDen k) {struct c} : kDen k :=
59 match c in con _ k return kDen k with 50 match c in con _ k return kDen k with
60 | CVar _ x => x 51 | CVar _ x => x
62 | Poly _ c1 => forall x, cDen (c1 x) 53 | Poly _ c1 => forall x, cDen (c1 x)
63 | CAbs _ _ c1 => fun x => cDen (c1 x) 54 | CAbs _ _ c1 => fun x => cDen (c1 x)
64 | CApp _ _ c1 c2 => (cDen c1) (cDen c2) 55 | CApp _ _ c1 c2 => (cDen c1) (cDen c2)
65 | Name n => n 56 | Name n => n
66 | TRecord c1 => record (cDen c1) 57 | TRecord c1 => record (cDen c1)
67 | CEmpty _ => nil 58 | CEmpty _ => fun _ => None
68 | CSingle _ c1 c2 => (cDen c1, cDen c2) :: nil 59 | CSingle _ c1 c2 => fun n => if name_eq_dec n (cDen c1) then Some (cDen c2) else None
69 | CConcat _ c1 c2 => cDen c1 ++ cDen c2 60 | CConcat _ c1 c2 => fun n => match (cDen c1) n with
70 | CFold k1 k2 => @cfold _ _ 61 | None => (cDen c2) n
62 | v => v
63 end
64 | CMap k1 k2 => fun f r n => match r n with
65 | None => None
66 | Some T => Some (f T)
67 end
71 | CGuarded _ _ _ _ c => cDen c 68 | CGuarded _ _ _ _ c => cDen c
72 end. 69 end.
73 70
74 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2', 71 Theorem subs_correct : forall k1 (c1 : con kDen k1) k2 (c2 : _ -> con kDen k2) c2',
75 subs c1 c2 c2' 72 subs c1 c2 c2'
79 | [ H : _ |- _ ] => rewrite H 76 | [ H : _ |- _ ] => rewrite H
80 end; intuition. 77 end; intuition.
81 Qed. 78 Qed.
82 79
83 Definition disjoint T (r1 r2 : row T) := 80 Definition disjoint T (r1 r2 : row T) :=
84 AllS (fun p1 => AllS (fun p2 => fst p1 <> fst p2) r2) r1. 81 forall n, match r1 n, r2 n with
82 | Some _, Some _ => False
83 | _, _ => True
84 end.
85 Definition dvar k (c1 c2 : con kDen (KRecord k)) := 85 Definition dvar k (c1 c2 : con kDen (KRecord k)) :=
86 disjoint (cDen c1) (cDen c2). 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 87
148 Scheme deq_mut := Minimality for deq Sort Prop 88 Scheme deq_mut := Minimality for deq Sort Prop
149 with disj_mut := Minimality for disj Sort Prop. 89 with disj_mut := Minimality for disj Sort Prop.
150 90
151 Theorem deq_correct : forall k (c1 c2 : con kDen k), 91 Theorem deq_correct : forall k (c1 c2 : con kDen k),
152 deq dvar c1 c2 92 deq dvar c1 c2
153 -> cDen c1 = cDen c2. 93 -> cDen c1 = cDen c2.
154 Hint Resolve map_id map_dist fold_fuse AllS_app disjoint_symm. 94 Ltac t := repeat progress (simpl; intuition; subst).
155 Hint Extern 1 (_ = _) => unfold row; symmetry; apply app_ass. 95
96 Ltac use_disjoint' notDone E :=
97 match goal with
98 | [ H : disjoint _ _ |- _ ] =>
99 notDone H; generalize (H E); use_disjoint'
100 ltac:(fun H' =>
101 match H' with
102 | H => fail 1
103 | _ => notDone H'
104 end) E
105 | _ => idtac
106 end.
107 Ltac use_disjoint := use_disjoint' ltac:(fun _ => idtac).
156 108
157 apply (deq_mut (dvar := dvar) 109 apply (deq_mut (dvar := dvar)
158 (fun k (c1 c2 : con kDen k) => 110 (fun k (c1 c2 : con kDen k) =>
159 cDen c1 = cDen c2) 111 cDen c1 = cDen c2)
160 (fun k (c1 c2 : con kDen (KRecord k)) => 112 (fun k (c1 c2 : con kDen (KRecord k)) =>
161 disjoint (cDen c1) (cDen c2))); 113 disjoint (cDen c1) (cDen c2))); t;
162 simpl; intuition; 114 repeat ((unfold row; apply ext_eq)
115 || (match goal with
116 | [ H : _ |- _ ] => rewrite H
117 | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H)
118 end); t);
119 unfold disjoint; t;
163 repeat (match goal with 120 repeat (match goal with
164 | [ H : _ |- _ ] => rewrite H 121 | [ |- context[match cDen ?C ?E with Some _ => _ | None => _ end] ] =>
165 | [ H : subs _ _ _ |- _ ] => rewrite <- (subs_correct H) 122 use_disjoint E; destruct (cDen C E)
166 end; simpl; intuition); try congruence; unfold disjoint in *; intuition; 123 | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] =>
167 fold kDen in *; repeat match goal with 124 use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2)
168 | [ H : AllS _ (_ :: _) |- _ ] => inversion H; clear H; subst; simpl in * 125 | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] =>
169 end; auto. 126 use_disjoint E; destruct (cDen C E)
127 end; t).
170 Qed. 128 Qed.