Mercurial > cpdt > repo

comparison src/Intensional.v @ 297:b441010125d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Everything compiles in Coq 8.3pl1
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:39:12 -0500
parents 9632f7316c29
children 7b38729be069
comparison
equal deleted inserted replaced
296:559ec7328410 297:b441010125d4
1 (* Copyright (c) 2008-2009, Adam Chlipala 1 (* Copyright (c) 2008-2009, 2011, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
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 Eqdep List. 11 Require Import Arith Eqdep List FunctionalExtensionality.
12 12
13 Require Import Axioms DepList Tactics. 13 Require Import DepList Tactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
176 176
177 (** It turns out to be trivial to establish the translation's soundness. *) 177 (** It turns out to be trivial to establish the translation's soundness. *)
178 178
179 Theorem phoasify_sound : forall G t (e : DeBruijn.exp G t) s, 179 Theorem phoasify_sound : forall G t (e : DeBruijn.exp G t) s,
180 Phoas.expDenote (phoasify e s) = DeBruijn.expDenote e s. 180 Phoas.expDenote (phoasify e s) = DeBruijn.expDenote e s.
181 induction e; crush; ext_eq; crush. 181 induction e; crush; (let x := fresh in extensionality x); crush.
182 Qed. 182 Qed.
183 183
184 (** We can prove that any output of [Phoasify] is well-formed, in a sense strong enough to let us avoid asserting last chapter's axiom. *) 184 (** We can prove that any output of [Phoasify] is well-formed, in a sense strong enough to let us avoid asserting last chapter's axiom. *)
185 185
186 Print Wf. 186 Print Wf.
418 Lemma dbify_sound : forall G t (e1 : Phoas.exp _ t) (e2 : Phoas.exp _ t), 418 Lemma dbify_sound : forall G t (e1 : Phoas.exp _ t) (e2 : Phoas.exp _ t),
419 exp_equiv G e1 e2 419 exp_equiv G e1 e2
420 -> forall ts (w : wf ts e1) s, 420 -> forall ts (w : wf ts e1) s,
421 G = makeG' s 421 G = makeG' s
422 -> DeBruijn.expDenote (dbify e1 w) s = Phoas.expDenote e2. 422 -> DeBruijn.expDenote (dbify e1 w) s = Phoas.expDenote e2.
423 induction 1; crush; ext_eq; crush. 423 induction 1; crush; (let x := fresh in extensionality x); crush.
424 Qed. 424 Qed.
425 425
426 (** In the usual way, we wrap [dbify_sound] into the final soundness theorem, formally establishing the expressive equivalence of PHOAS and de Bruijn index terms. *) 426 (** In the usual way, we wrap [dbify_sound] into the final soundness theorem, formally establishing the expressive equivalence of PHOAS and de Bruijn index terms. *)
427 427
428 Theorem Dbify_sound : forall t (E : Exp t) (W : Wf E), 428 Theorem Dbify_sound : forall t (E : Exp t) (W : Wf E),