Mercurial > cpdt > repo

comparison src/Intensional.v @ 259:0c5fb678bfe2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Dbify_sound
author Adam Chlipala <adamc@hcoop.net>
date Wed, 16 Dec 2009 16:45:50 -0500
parents 4c9031b62cd0
children 9632f7316c29
comparison
equal deleted inserted replaced
258:4c9031b62cd0 259:0c5fb678bfe2
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 Arith List. 11 Require Import Arith Eqdep 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 *)
278 Lemma Wf_wf : forall t (E : Exp t), 278 Lemma Wf_wf : forall t (E : Exp t),
279 Wf E 279 Wf E
280 -> wf nil (E (fun _ => nat)). 280 -> wf nil (E (fun _ => nat)).
281 intros; eapply Wf_wf'; eauto. 281 intros; eapply Wf_wf'; eauto.
282 Qed. 282 Qed.
283
284 Theorem None_Some : forall T (x : T),
285 None = Some x
286 -> False.
287 congruence.
288 Qed.
289
290 Theorem Some_Some : forall T (x y : T),
291 Some x = Some y
292 -> x = y.
293 congruence.
294 Qed.
295
296 Fixpoint makeVar {ts n t} : ts ## n = Some t -> member t ts :=
297 match ts return ts ## n = Some t -> member t ts with
298 | nil => fun Heq => match None_Some Heq with end
299 | t' :: ts' => if eq_nat_dec n (length ts') as b
300 return (if b then Some t' else lookup ts' n) = Some t -> member t (t' :: ts')
301 then fun Heq => match Some_Some Heq in _ = t0 return member t0 (t' :: ts') with
302 | refl_equal => HFirst
303 end
304 else fun Heq => HNext (makeVar Heq)
305 end.
306
307 Axiom cheat : forall T, T.
308
309 Fixpoint dbify {ts} t (e : Phoas.exp (fun _ => nat) t) : wf ts e -> DeBruijn.exp ts t :=
310 match e in Phoas.exp _ t return wf ts e -> DeBruijn.exp ts t with
311 | Phoas.Var _ n => fun wf => DeBruijn.Var (makeVar wf)
312
313 | Phoas.Const n => fun _ => DeBruijn.Const n
314 | Phoas.Plus e1 e2 => fun wf => DeBruijn.Plus (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
315
316 | Phoas.App _ _ e1 e2 => fun wf => DeBruijn.App (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
317 | Phoas.Abs _ _ e1 => fun wf => DeBruijn.Abs (dbify (e1 (length ts)) wf)
318 end.
319
320 Definition Dbify t (E : Phoas.Exp t) (W : Wf E) : DeBruijn.exp nil t :=
321 dbify (E _) (Wf_wf W).
322
323 Fixpoint makeG' ts (s : hlist typeDenote ts) : list { t : type & nat * typeDenote t }%type :=
324 match s with
325 | HNil => nil
326 | HCons _ ts' v s' => existT _ _ (length ts', v) :: makeG' s'
327 end.
328
329 Lemma In_makeG'_contra' : forall t v2 ts (s : hlist _ ts) n,
330 In (existT _ t (n, v2)) (makeG' s)
331 -> n >= length ts
332 -> False.
333 induction s; crush; eauto.
334 Qed.
335
336 Lemma In_makeG'_contra : forall t v2 ts (s : hlist _ ts),
337 In (existT _ t (length ts, v2)) (makeG' s)
338 -> False.
339 intros; eapply In_makeG'_contra'; eauto.
340 Qed.
341
342 Hint Resolve In_makeG'_contra.
343
344 Lemma In_makeG' : forall t v1 v2 ts s (w : ts ## v1 = Some t),
345 In (existT _ t (v1, v2)) (makeG' s)
346 -> hget s (makeVar w) = v2.
347 induction s; crush;
348 match goal with
349 | [ |- context[if ?E then _ else _] ] => destruct E; crush
350 end;
351 repeat match goal with
352 | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf)
353 end; crush; elimtype False; eauto.
354 Qed.
355
356 Hint Resolve In_makeG'.
357
358 Lemma dbify_sound : forall G t (e1 : Phoas.exp _ t) (e2 : Phoas.exp _ t),
359 exp_equiv G e1 e2
360 -> forall ts (w : wf ts e1) s,
361 G = makeG' s
362 -> DeBruijn.expDenote (dbify e1 w) s = Phoas.expDenote e2.
363 induction 1; crush; ext_eq; crush.
364 Qed.
365
366 Theorem Dbify_sound : forall t (E : Exp t) (W : Wf E),
367 DeBruijn.expDenote (Dbify W) HNil = Phoas.ExpDenote E.
368 unfold Dbify, Phoas.ExpDenote; intros; eapply dbify_sound; eauto.
369 Qed.