Mercurial > urweb

comparison src/coq/Semantics.v @ 618:be88d2d169f6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Most of expression semantics
author Adam Chlipala <adamc@hcoop.net>
date Sat, 21 Feb 2009 13:17:06 -0500
parents 5b358e8f9f09
children f38e009009bb
comparison
equal deleted inserted replaced
617:5b358e8f9f09 618:be88d2d169f6
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 Eqdep.
29
28 Require Import Axioms. 30 Require Import Axioms.
29 Require Import Syntax. 31 Require Import Syntax.
30 32
31 Set Implicit Arguments. 33 Set Implicit Arguments.
32 34
86 disjoint (cDen c1) (cDen c2). 88 disjoint (cDen c1) (cDen c2).
87 89
88 Scheme deq_mut := Minimality for deq Sort Prop 90 Scheme deq_mut := Minimality for deq Sort Prop
89 with disj_mut := Minimality for disj Sort Prop. 91 with disj_mut := Minimality for disj Sort Prop.
90 92
91 Theorem deq_correct : forall k (c1 c2 : con kDen k), 93 Ltac deq_disj_correct scm :=
92 deq dvar c1 c2 94 let t := repeat progress (simpl; intuition; subst) in
93 -> cDen c1 = cDen c2. 95
94 Ltac t := repeat progress (simpl; intuition; subst). 96 let rec use_disjoint' notDone E :=
95
96 Ltac use_disjoint' notDone E :=
97 match goal with 97 match goal with
98 | [ H : disjoint _ _ |- _ ] => 98 | [ H : disjoint _ _ |- _ ] =>
99 notDone H; generalize (H E); use_disjoint' 99 notDone H; generalize (H E); use_disjoint'
100 ltac:(fun H' => 100 ltac:(fun H' =>
101 match H' with 101 match H' with
102 | H => fail 1 102 | H => fail 1
103 | _ => notDone H' 103 | _ => notDone H'
104 end) E 104 end) E
105 | _ => idtac 105 | _ => idtac
106 end. 106 end in
107 Ltac use_disjoint := use_disjoint' ltac:(fun _ => idtac). 107 let use_disjoint := use_disjoint' ltac:(fun _ => idtac) in
108 108
109 apply (deq_mut (dvar := dvar) 109 apply (scm _ dvar
110 (fun k (c1 c2 : con kDen k) => 110 (fun k (c1 c2 : con kDen k) =>
111 cDen c1 = cDen c2) 111 cDen c1 = cDen c2)
112 (fun k (c1 c2 : con kDen (KRecord k)) => 112 (fun k (c1 c2 : con kDen (KRecord k)) =>
113 disjoint (cDen c1) (cDen c2))); t; 113 disjoint (cDen c1) (cDen c2))); t;
114 repeat ((unfold row; apply ext_eq) 114 repeat ((unfold row; apply ext_eq)
123 | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] => 123 | [ |- context[if name_eq_dec ?N1 ?N2 then _ else _] ] =>
124 use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2) 124 use_disjoint N1; use_disjoint N2; destruct (name_eq_dec N1 N2)
125 | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] => 125 | [ _ : context[match cDen ?C ?E with Some _ => _ | None => _ end] |- _ ] =>
126 use_disjoint E; destruct (cDen C E) 126 use_disjoint E; destruct (cDen C E)
127 end; t). 127 end; t).
128 Qed. 128
129 Theorem deq_correct : forall k (c1 c2 : con kDen k),
130 deq dvar c1 c2
131 -> cDen c1 = cDen c2.
132 deq_disj_correct deq_mut.
133 Qed.
134
135 Theorem disj_correct : forall k (c1 c2 : con kDen (KRecord k)),
136 disj dvar c1 c2
137 -> disjoint (cDen c1) (cDen c2).
138 deq_disj_correct disj_mut.
139 Qed.
140
141 Axiom cheat : forall T, T.
142
143 Definition tDen (t : con kDen KType) : Set := cDen t.
144
145 Theorem name_eq_dec_refl : forall n, name_eq_dec n n = left _ (refl_equal n).
146 intros; destruct (name_eq_dec n n); intuition; [
147 match goal with
148 | [ e : _ = _ |- _ ] => rewrite (UIP_refl _ _ e); reflexivity
149 end
150 | elimtype False; tauto
151 ].
152 Qed.
153
154 Theorem cut_disjoint : forall n1 v r,
155 disjoint (fun n => if name_eq_dec n n1 then Some v else None) r
156 -> unit = match r n1 with
157 | Some T => T
158 | None => unit
159 end.
160 intros;
161 match goal with
162 | [ H : disjoint _ _ |- _ ] => generalize (H n1)
163 end; rewrite name_eq_dec_refl;
164 destruct (r n1); intuition.
165 Qed.
166
167 Implicit Arguments cut_disjoint [v r].
168
169 Fixpoint eDen t (e : exp dvar tDen t) {struct e} : tDen t :=
170 match e in exp _ _ t return tDen t with
171 | Var _ x => x
172 | App _ _ e1 e2 => (eDen e1) (eDen e2)
173 | Abs _ _ e1 => fun x => eDen (e1 x)
174 | ECApp _ c _ _ e1 Hsub => match subs_correct Hsub in _ = T return T with
175 | refl_equal => (eDen e1) (cDen c)
176 end
177 | ECAbs _ _ e1 => fun X => eDen (e1 X)
178 | Cast _ _ Heq e1 => match deq_correct Heq in _ = T return T with
179 | refl_equal => eDen e1
180 end
181 | Empty => fun _ => tt
182 | Single c _ e1 => fun n => if name_eq_dec n (cDen c) as B
183 return (match (match (if B then _ else _) with Some _ => if B then _ else _ | None => _ end)
184 with Some _ => _ | None => unit end)
185 then eDen e1 else tt
186 | Proj c _ _ e1 =>
187 match name_eq_dec_refl (cDen c) in _ = B
188 return (match (match (if B then _ else _) with
189 | Some _ => if B then _ else _
190 | None => _ end)
191 return Set
192 with Some _ => _ | None => _ end) with
193 | refl_equal => (eDen e1) (cDen c)
194 end
195 | Cut c _ c' Hdisj e1 => fun n =>
196 match name_eq_dec n (cDen c) as B return (match (match (if B then Some _ else None) with Some _ => if B then _ else _ | None => (cDen c') n end)
197 with Some T => T | None => unit end
198 -> match (cDen c') n with
199 | None => unit
200 | Some T => T
201 end) with
202 | left Heq => fun _ =>
203 match sym_eq Heq in _ = n' return match cDen c' n' return Set with Some _ => _ | None => _ end with
204 | refl_equal =>
205 match cut_disjoint _ (disj_correct Hdisj) in _ = T return T with
206 | refl_equal => tt
207 end
208 end
209 | right _ => fun x => x
210 end ((eDen e1) n)
211
212 | _ => cheat _
213 end.