Mercurial > cpdt > repo

comparison src/Intensional.v @ 258:4c9031b62cd0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Wf_wf
author Adam Chlipala <adamc@hcoop.net>
date Wed, 16 Dec 2009 16:21:29 -0500
parents 108ec446fbaf
children 0c5fb678bfe2
comparison
equal deleted inserted replaced
257:108ec446fbaf 258:4c9031b62cd0
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import List. 11 Require Import Arith List.
12 12
13 Require Import Axioms DepList Tactics. 13 Require Import Axioms DepList Tactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
105 -> exp_equiv G (f1 @ x1) (f2 @ x2) 105 -> exp_equiv G (f1 @ x1) (f2 @ x2)
106 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2, 106 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
107 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2)) 107 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
108 -> exp_equiv G (Abs f1) (Abs f2). 108 -> exp_equiv G (Abs f1) (Abs f2).
109 End exp_equiv. 109 End exp_equiv.
110
111 Definition Wf t (E : Exp t) := forall var1 var2, exp_equiv nil (E var1) (E var2).
110 End Phoas. 112 End Phoas.
111 (* end hide *) 113 (* end hide *)
112 114
113 Module DeBruijn. 115 Module DeBruijn.
114 Inductive exp : list type -> type -> Type := 116 Inductive exp : list type -> type -> Type :=
198 200
199 induction e; crush. 201 induction e; crush.
200 Qed. 202 Qed.
201 End vars. 203 End vars.
202 204
205 Theorem Phoasify_wf : forall t (e : DeBruijn.exp nil t),
206 Wf (Phoasify e).
207 unfold Wf, Phoasify; intros;
208 apply (phoasify_wf e (HNil (B := var1)) (HNil (B := var2))).
209 Qed.
210
203 211
204 (** * From PHOAS to De Bruijn *) 212 (** * From PHOAS to De Bruijn *)
213
214 Fixpoint lookup (G : list type) (n : nat) : option type :=
215 match G with
216 | nil => None
217 | t :: G' => if eq_nat_dec n (length G') then Some t else lookup G' n
218 end.
219
220 Infix "##" := lookup (left associativity, at level 1).
221
222 Fixpoint wf (ts : list type) t (e : Phoas.exp (fun _ => nat) t) : Prop :=
223 match e with
224 | Phoas.Var t n => ts ## n = Some t
225 | Phoas.Const _ => True
226 | Phoas.Plus e1 e2 => wf ts e1 /\ wf ts e2
227 | Phoas.App _ _ e1 e2 => wf ts e1 /\ wf ts e2
228 | Phoas.Abs t1 _ e1 => wf (t1 :: ts) (e1 (length ts))
229 end.
230
231 Fixpoint makeG (ts : list type) : list { t : type & nat * nat }%type :=
232 match ts with
233 | nil => nil
234 | t :: ts' => existT _ t (length ts', length ts') :: makeG ts'
235 end.
236
237 Opaque eq_nat_dec.
238 Hint Extern 1 (_ >= _) => omega.
239
240 Lemma lookup_contra' : forall t ts n,
241 ts ## n = Some t
242 -> n >= length ts
243 -> False.
244 induction ts; crush;
245 match goal with
246 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E; crush
247 end; eauto.
248 Qed.
249
250 Lemma lookup_contra : forall t ts,
251 ts ## (length ts) = Some t
252 -> False.
253 intros; eapply lookup_contra'; eauto.
254 Qed.
255
256 Hint Resolve lookup_contra.
257
258 Lemma lookup_In : forall t v1 v2 ts,
259 In (existT (fun _ : type => (nat * nat)%type) t (v1, v2)) (makeG ts)
260 -> ts ## v1 = Some t.
261 induction ts; crush;
262 match goal with
263 | [ |- context[if ?E then _ else _] ] => destruct E; crush
264 end; elimtype False; eauto.
265 Qed.
266
267 Hint Resolve lookup_In.
268
269 Hint Extern 1 (_ :: _ = makeG (_ :: _)) => reflexivity.
270
271 Lemma Wf_wf' : forall G t e1 (e2 : Phoas.exp (fun _ => nat) t),
272 exp_equiv G e1 e2
273 -> forall ts, G = makeG ts
274 -> wf ts e1.
275 induction 1; crush; eauto.
276 Qed.
277
278 Lemma Wf_wf : forall t (E : Exp t),
279 Wf E
280 -> wf nil (E (fun _ => nat)).
281 intros; eapply Wf_wf'; eauto.
282 Qed.