Mercurial > cpdt > repo

annotate 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
rev   line source
adam@297 1 (* Copyright (c) 2008-2009, 2011, Adam Chlipala
adamc@182 2 *
adamc@182 3 * This work is licensed under a
adamc@182 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@182 5 * Unported License.
adamc@182 6 * The license text is available at:
adamc@182 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@182 8 *)
adamc@182 9
adamc@257 10 (* begin hide *)
adam@297 11 Require Import Arith Eqdep List FunctionalExtensionality.
adamc@257 12
adam@297 13 Require Import DepList Tactics.
adamc@257 14
adamc@257 15 Set Implicit Arguments.
adamc@257 16 (* end hide *)
adamc@257 17
adamc@184 18
adamc@182 19 (** %\chapter{Intensional Transformations}% *)
adamc@182 20
adamc@260 21 (** The essential benefit of higher-order encodings is that variable contexts are implicit. We represent the object language's contexts within the meta language's contexts. For translations like CPS conversion, this is a clear win, since such translations do not need to keep track of details of which variables are available. Other important translations, including closure conversion, need to work with variables as first-class, analyzable values.
adamc@260 22
adamc@260 23 Another example is conversion from PHOAS terms to de Bruijn terms. The output format makes the structure of variables explicit, so the translation requires explicit reasoning about variable identity. In this chapter, we implement verified translations in both directions between last chapter's PHOAS language and a de Bruijn version of it. Along the way, we show one approach to avoiding the use of axioms with PHOAS. *)
adamc@260 24
adamc@257 25 (* begin hide *)
adamc@257 26
adamc@257 27 Inductive type : Type :=
adamc@257 28 | Nat : type
adamc@257 29 | Arrow : type -> type -> type.
adamc@257 30
adamc@257 31 Infix "-->" := Arrow (right associativity, at level 60).
adamc@257 32
adamc@257 33 Fixpoint typeDenote (t : type) : Set :=
adamc@257 34 match t with
adamc@257 35 | Nat => nat
adamc@257 36 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@257 37 end.
adamc@257 38
adamc@257 39 Module Phoas.
adamc@257 40 Section vars.
adamc@257 41 Variable var : type -> Type.
adamc@257 42
adamc@257 43 Inductive exp : type -> Type :=
adamc@257 44 | Var : forall t,
adamc@257 45 var t
adamc@257 46 -> exp t
adamc@257 47
adamc@257 48 | Const : nat -> exp Nat
adamc@257 49 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@257 50
adamc@257 51 | App : forall t1 t2,
adamc@257 52 exp (t1 --> t2)
adamc@257 53 -> exp t1
adamc@257 54 -> exp t2
adamc@257 55 | Abs : forall t1 t2,
adamc@257 56 (var t1 -> exp t2)
adamc@257 57 -> exp (t1 --> t2).
adamc@257 58 End vars.
adamc@257 59
adamc@257 60 Definition Exp t := forall var, exp var t.
adamc@257 61
adamc@257 62 Implicit Arguments Var [var t].
adamc@257 63 Implicit Arguments Const [var].
adamc@257 64 Implicit Arguments Plus [var].
adamc@257 65 Implicit Arguments App [var t1 t2].
adamc@257 66 Implicit Arguments Abs [var t1 t2].
adamc@257 67
adamc@257 68 Notation "# v" := (Var v) (at level 70).
adamc@257 69
adamc@257 70 Notation "^ n" := (Const n) (at level 70).
adamc@257 71 Infix "+^" := Plus (left associativity, at level 79).
adamc@257 72
adamc@257 73 Infix "@" := App (left associativity, at level 77).
adamc@257 74 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@257 75 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@257 76
adamc@257 77 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@257 78 match e with
adamc@257 79 | Var _ v => v
adamc@257 80
adamc@257 81 | Const n => n
adamc@257 82 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@257 83
adamc@257 84 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@257 85 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@257 86 end.
adamc@257 87
adamc@257 88 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@257 89
adamc@257 90 Section exp_equiv.
adamc@257 91 Variables var1 var2 : type -> Type.
adamc@257 92
adamc@257 93 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type
adamc@257 94 -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@257 95 | EqVar : forall G t (v1 : var1 t) v2,
adamc@257 96 In (existT _ t (v1, v2)) G
adamc@257 97 -> exp_equiv G (#v1) (#v2)
adamc@257 98
adamc@257 99 | EqConst : forall G n,
adamc@257 100 exp_equiv G (^n) (^n)
adamc@257 101 | EqPlus : forall G x1 y1 x2 y2,
adamc@257 102 exp_equiv G x1 x2
adamc@257 103 -> exp_equiv G y1 y2
adamc@257 104 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@257 105
adamc@257 106 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@257 107 exp_equiv G f1 f2
adamc@257 108 -> exp_equiv G x1 x2
adamc@257 109 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@257 110 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@257 111 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@257 112 -> exp_equiv G (Abs f1) (Abs f2).
adamc@257 113 End exp_equiv.
adamc@258 114
adamc@258 115 Definition Wf t (E : Exp t) := forall var1 var2, exp_equiv nil (E var1) (E var2).
adamc@257 116 End Phoas.
adamc@257 117 (* end hide *)
adamc@257 118
adamc@260 119 (** The de Bruijn version of simply-typed lambda calculus is defined in a manner that should be old hat by now. *)
adamc@260 120
adamc@257 121 Module DeBruijn.
adamc@257 122 Inductive exp : list type -> type -> Type :=
adamc@257 123 | Var : forall G t,
adamc@257 124 member t G
adamc@257 125 -> exp G t
adamc@257 126
adamc@257 127 | Const : forall G, nat -> exp G Nat
adamc@257 128 | Plus : forall G, exp G Nat -> exp G Nat -> exp G Nat
adamc@257 129
adamc@257 130 | App : forall G t1 t2,
adamc@257 131 exp G (t1 --> t2)
adamc@257 132 -> exp G t1
adamc@257 133 -> exp G t2
adamc@257 134 | Abs : forall G t1 t2,
adamc@257 135 exp (t1 :: G) t2
adamc@257 136 -> exp G (t1 --> t2).
adamc@257 137
adamc@257 138 Implicit Arguments Const [G].
adamc@257 139
adamc@257 140 Fixpoint expDenote G t (e : exp G t) : hlist typeDenote G -> typeDenote t :=
adamc@257 141 match e with
adamc@257 142 | Var _ _ v => fun s => hget s v
adamc@257 143
adamc@257 144 | Const _ n => fun _ => n
adamc@257 145 | Plus _ e1 e2 => fun s => expDenote e1 s + expDenote e2 s
adamc@257 146
adamc@257 147 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adamc@257 148 | Abs _ _ _ e' => fun s x => expDenote e' (x ::: s)
adamc@257 149 end.
adamc@257 150 End DeBruijn.
adamc@257 151
adamc@257 152 Import Phoas DeBruijn.
adamc@257 153
adamc@257 154
adamc@257 155 (** * From De Bruijn to PHOAS *)
adamc@257 156
adamc@260 157 (** The heart of the translation into PHOAS is this function [phoasify], which is parameterized by an [hlist] that represents a mapping from de Bruijn variables to PHOAS variables. *)
adamc@260 158
adamc@257 159 Section phoasify.
adamc@257 160 Variable var : type -> Type.
adamc@257 161
adamc@257 162 Fixpoint phoasify G t (e : DeBruijn.exp G t) : hlist var G -> Phoas.exp var t :=
adamc@257 163 match e with
adamc@257 164 | Var _ _ v => fun s => #(hget s v)
adamc@257 165
adamc@257 166 | Const _ n => fun _ => ^n
adamc@257 167 | Plus _ e1 e2 => fun s => phoasify e1 s +^ phoasify e2 s
adamc@257 168
adamc@257 169 | App _ _ _ e1 e2 => fun s => phoasify e1 s @ phoasify e2 s
adamc@257 170 | Abs _ _ _ e' => fun s => \x, phoasify e' (x ::: s)
adamc@257 171 end.
adamc@257 172 End phoasify.
adamc@257 173
adamc@257 174 Definition Phoasify t (e : DeBruijn.exp nil t) : Phoas.Exp t :=
adamc@257 175 fun _ => phoasify e HNil.
adamc@257 176
adamc@260 177 (** It turns out to be trivial to establish the translation's soundness. *)
adamc@260 178
adamc@257 179 Theorem phoasify_sound : forall G t (e : DeBruijn.exp G t) s,
adamc@257 180 Phoas.expDenote (phoasify e s) = DeBruijn.expDenote e s.
adam@297 181 induction e; crush; (let x := fresh in extensionality x); crush.
adamc@257 182 Qed.
adamc@257 183
adamc@260 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. *)
adamc@260 185
adamc@260 186 Print Wf.
adamc@260 187 (** %\vspace{-.15in}% [[
adamc@260 188 Wf =
adamc@260 189 fun (t : type) (E : Exp t) =>
adamc@260 190 forall var1 var2 : type -> Type, exp_equiv nil (E var1) (E var2)
adamc@260 191 : forall t : type, Exp t -> Prop
adamc@260 192 ]] *)
adamc@260 193
adamc@257 194 Section vars.
adamc@257 195 Variables var1 var2 : type -> Type.
adamc@257 196
adamc@260 197 (** In the course of proving well-formedness, we will need to translate back and forth between the de Bruijn and PHOAS representations of free variable information. The function [zip] combines two de Bruijn substitutions into a single PHOAS context. *)
adamc@260 198
adamc@260 199 Fixpoint zip G (s1 : hlist var1 G)
adamc@260 200 : hlist var2 G -> list {t : type & var1 t * var2 t}%type :=
adamc@257 201 match s1 with
adamc@257 202 | HNil => fun _ => nil
adamc@257 203 | HCons _ _ v1 s1' => fun s2 => existT _ _ (v1, hhd s2) :: zip s1' (htl s2)
adamc@257 204 end.
adamc@257 205
adamc@260 206 (** Two simple lemmas about [zip] will make useful hints. *)
adamc@260 207
adamc@257 208 Lemma In_zip : forall t G (s1 : hlist _ G) s2 (m : member t G),
adamc@257 209 In (existT _ t (hget s1 m, hget s2 m)) (zip s1 s2).
adamc@257 210 induction s1; intro s2; dep_destruct s2; intro m; dep_destruct m; crush.
adamc@257 211 Qed.
adamc@257 212
adamc@257 213 Lemma unsimpl_zip : forall t (v1 : var1 t) (v2 : var2 t)
adamc@257 214 G (s1 : hlist _ G) s2 t' (e1 : Phoas.exp _ t') e2,
adamc@257 215 exp_equiv (zip (v1 ::: s1) (v2 ::: s2)) e1 e2
adamc@257 216 -> exp_equiv (existT _ _ (v1, v2) :: zip s1 s2) e1 e2.
adamc@257 217 trivial.
adamc@257 218 Qed.
adamc@257 219
adamc@257 220 Hint Resolve In_zip unsimpl_zip.
adamc@257 221
adamc@260 222 (** Now it is trivial to prove the main inductive lemma about well-formedness. *)
adamc@260 223
adamc@260 224 Lemma phoasify_wf : forall G t (e : DeBruijn.exp G t) s1 s2,
adamc@257 225 exp_equiv (zip s1 s2) (phoasify e s1) (phoasify e s2).
adamc@257 226 Hint Constructors exp_equiv.
adamc@257 227
adamc@257 228 induction e; crush.
adamc@257 229 Qed.
adamc@257 230 End vars.
adamc@257 231
adamc@260 232 (** We apply [phoasify_wf] manually to prove the final theorem. *)
adamc@260 233
adamc@258 234 Theorem Phoasify_wf : forall t (e : DeBruijn.exp nil t),
adamc@258 235 Wf (Phoasify e).
adamc@258 236 unfold Wf, Phoasify; intros;
adamc@258 237 apply (phoasify_wf e (HNil (B := var1)) (HNil (B := var2))).
adamc@258 238 Qed.
adamc@258 239
adamc@260 240 (** Now, if we compose [Phoasify] with any translation over PHOAS terms, we can verify the composed translation without relying on axioms. The conclusion of [Phoasify_wf] is robustly useful in verifying a wide variety of translations that use a wide variety of [var] instantiations. *)
adamc@260 241
adamc@257 242
adamc@257 243 (** * From PHOAS to De Bruijn *)
adamc@258 244
adamc@260 245 (** The translation to de Bruijn terms is more involved. We will essentially be instantiating and using a PHOAS term following a convention isomorphic to %\textit{%#<i>#de Bruijn levels#</i>#%}%, which are different from the de Bruijn indices that we have treated so far. With levels, a given bound variable is referred to by the same number at each of its occurrences. In any expression, the binders that are not enclosed by other binders are assigned level 0, a binder with just one enclosing binder is assigned level 1, and so on. The uniformity of references to any binder will be critical to our translation, since it is compatible with the pattern of filling in all of a PHOAS variable's locations at once by applying a function.
adamc@260 246
adamc@260 247 We implement a special lookup function, for reading a numbered variable's type out of a de Bruijn level typing context. The last variable in the list is taken to have level 0, the next-to-last level 1, and so on. *)
adamc@260 248
adamc@260 249 Fixpoint lookup (ts : list type) (n : nat) : option type :=
adamc@260 250 match ts with
adamc@258 251 | nil => None
adamc@260 252 | t :: ts' => if eq_nat_dec n (length ts') then Some t else lookup ts' n
adamc@258 253 end.
adamc@258 254
adamc@258 255 Infix "##" := lookup (left associativity, at level 1).
adamc@258 256
adamc@260 257 (** With [lookup], we can define a notion of well-formedness for PHOAS expressions that we are treating according to the de Bruijn level convention. *)
adamc@260 258
adamc@258 259 Fixpoint wf (ts : list type) t (e : Phoas.exp (fun _ => nat) t) : Prop :=
adamc@258 260 match e with
adamc@258 261 | Phoas.Var t n => ts ## n = Some t
adamc@258 262 | Phoas.Const _ => True
adamc@258 263 | Phoas.Plus e1 e2 => wf ts e1 /\ wf ts e2
adamc@258 264 | Phoas.App _ _ e1 e2 => wf ts e1 /\ wf ts e2
adamc@258 265 | Phoas.Abs t1 _ e1 => wf (t1 :: ts) (e1 (length ts))
adamc@258 266 end.
adamc@258 267
adamc@260 268 (** ** Connecting Notions of Well-Formedness *)
adamc@260 269
adamc@260 270 (** Our first order of business now is to prove that any well-formed [Exp] instantiates to a well-formed de Bruijn level expression. We start by characterizing, as a function of de Bruijn level contexts, the set of PHOAS contexts that will occur in the proof, where we will be inducting over an [exp_equiv] derivation. *)
adamc@260 271
adamc@258 272 Fixpoint makeG (ts : list type) : list { t : type & nat * nat }%type :=
adamc@258 273 match ts with
adamc@258 274 | nil => nil
adamc@258 275 | t :: ts' => existT _ t (length ts', length ts') :: makeG ts'
adamc@258 276 end.
adamc@258 277
adamc@260 278 (** Now we prove a connection between [lookup] and [makeG], by way of a lemma about [lookup]. *)
adamc@260 279
adamc@258 280 Opaque eq_nat_dec.
adamc@258 281 Hint Extern 1 (_ >= _) => omega.
adamc@258 282
adamc@258 283 Lemma lookup_contra' : forall t ts n,
adamc@258 284 ts ## n = Some t
adamc@258 285 -> n >= length ts
adamc@258 286 -> False.
adamc@258 287 induction ts; crush;
adamc@258 288 match goal with
adamc@258 289 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E; crush
adamc@258 290 end; eauto.
adamc@258 291 Qed.
adamc@258 292
adamc@258 293 Lemma lookup_contra : forall t ts,
adamc@258 294 ts ## (length ts) = Some t
adamc@258 295 -> False.
adamc@258 296 intros; eapply lookup_contra'; eauto.
adamc@258 297 Qed.
adamc@258 298
adamc@258 299 Hint Resolve lookup_contra.
adamc@258 300
adamc@258 301 Lemma lookup_In : forall t v1 v2 ts,
adamc@258 302 In (existT (fun _ : type => (nat * nat)%type) t (v1, v2)) (makeG ts)
adamc@258 303 -> ts ## v1 = Some t.
adamc@258 304 induction ts; crush;
adamc@258 305 match goal with
adamc@258 306 | [ |- context[if ?E then _ else _] ] => destruct E; crush
adamc@258 307 end; elimtype False; eauto.
adamc@258 308 Qed.
adamc@258 309
adamc@258 310 Hint Resolve lookup_In.
adamc@258 311
adamc@260 312 (** We can prove the main inductive lemma by induction over [exp_equiv] derivations. *)
adamc@260 313
adamc@258 314 Hint Extern 1 (_ :: _ = makeG (_ :: _)) => reflexivity.
adamc@258 315
adamc@258 316 Lemma Wf_wf' : forall G t e1 (e2 : Phoas.exp (fun _ => nat) t),
adamc@258 317 exp_equiv G e1 e2
adamc@258 318 -> forall ts, G = makeG ts
adamc@258 319 -> wf ts e1.
adamc@258 320 induction 1; crush; eauto.
adamc@258 321 Qed.
adamc@258 322
adamc@258 323 Lemma Wf_wf : forall t (E : Exp t),
adamc@258 324 Wf E
adamc@258 325 -> wf nil (E (fun _ => nat)).
adamc@258 326 intros; eapply Wf_wf'; eauto.
adamc@258 327 Qed.
adamc@259 328
adamc@260 329 (** ** The Translation *)
adamc@260 330
adamc@260 331 (** Implementing the translation itself will require some proofs. Our main function [dbify] will take [wf] proofs as arguments, and these proofs will be critical to constructing de Bruijn index terms. First, we use [congruence] to prove two basic theorems about [option]s. *)
adamc@260 332
adamc@259 333 Theorem None_Some : forall T (x : T),
adamc@259 334 None = Some x
adamc@259 335 -> False.
adamc@259 336 congruence.
adamc@259 337 Qed.
adamc@259 338
adamc@259 339 Theorem Some_Some : forall T (x y : T),
adamc@259 340 Some x = Some y
adamc@259 341 -> x = y.
adamc@259 342 congruence.
adamc@259 343 Qed.
adamc@259 344
adamc@260 345 (** We can use these theorems to implement [makeVar], which translates a proof about [lookup] into a de Bruijn index variable with a closely related type. *)
adamc@260 346
adamc@259 347 Fixpoint makeVar {ts n t} : ts ## n = Some t -> member t ts :=
adamc@260 348 match ts with
adamc@259 349 | nil => fun Heq => match None_Some Heq with end
adamc@260 350 | t' :: ts' => if eq_nat_dec n (length ts') as b return (if b then _ else _) = _ -> _
adamc@260 351 then fun Heq => match Some_Some Heq with refl_equal => HFirst end
adamc@259 352 else fun Heq => HNext (makeVar Heq)
adamc@259 353 end.
adamc@259 354
adamc@260 355 (** Now [dbify] is straightforward to define. We use the functions [proj1] and [proj2] to decompose proofs of conjunctions. *)
adamc@259 356
adamc@259 357 Fixpoint dbify {ts} t (e : Phoas.exp (fun _ => nat) t) : wf ts e -> DeBruijn.exp ts t :=
adamc@259 358 match e in Phoas.exp _ t return wf ts e -> DeBruijn.exp ts t with
adamc@259 359 | Phoas.Var _ n => fun wf => DeBruijn.Var (makeVar wf)
adamc@259 360
adamc@259 361 | Phoas.Const n => fun _ => DeBruijn.Const n
adamc@260 362 | Phoas.Plus e1 e2 => fun wf =>
adamc@260 363 DeBruijn.Plus (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
adamc@259 364
adamc@260 365 | Phoas.App _ _ e1 e2 => fun wf =>
adamc@260 366 DeBruijn.App (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
adamc@259 367 | Phoas.Abs _ _ e1 => fun wf => DeBruijn.Abs (dbify (e1 (length ts)) wf)
adamc@259 368 end.
adamc@259 369
adamc@260 370 (** We define the parametric translation [Dbify] by appealing to the well-formedness translation theorem [Wf_wf] that we proved earlier. *)
adamc@260 371
adamc@259 372 Definition Dbify t (E : Phoas.Exp t) (W : Wf E) : DeBruijn.exp nil t :=
adamc@259 373 dbify (E _) (Wf_wf W).
adamc@259 374
adamc@260 375 (** To prove soundness, it is helpful to classify a set of contexts which depends on a de Bruijn index substitution. *)
adamc@260 376
adamc@260 377 Fixpoint makeG' ts (s : hlist typeDenote ts)
adamc@260 378 : list { t : type & nat * typeDenote t }%type :=
adamc@259 379 match s with
adamc@259 380 | HNil => nil
adamc@259 381 | HCons _ ts' v s' => existT _ _ (length ts', v) :: makeG' s'
adamc@259 382 end.
adamc@259 383
adamc@260 384 (** We prove an analogous lemma to the one we proved connecting [makeG] and [lookup]. This time, we connect [makeG'] and [hget]. *)
adamc@260 385
adamc@259 386 Lemma In_makeG'_contra' : forall t v2 ts (s : hlist _ ts) n,
adamc@259 387 In (existT _ t (n, v2)) (makeG' s)
adamc@259 388 -> n >= length ts
adamc@259 389 -> False.
adamc@259 390 induction s; crush; eauto.
adamc@259 391 Qed.
adamc@259 392
adamc@259 393 Lemma In_makeG'_contra : forall t v2 ts (s : hlist _ ts),
adamc@259 394 In (existT _ t (length ts, v2)) (makeG' s)
adamc@259 395 -> False.
adamc@259 396 intros; eapply In_makeG'_contra'; eauto.
adamc@259 397 Qed.
adamc@259 398
adamc@259 399 Hint Resolve In_makeG'_contra.
adamc@259 400
adamc@259 401 Lemma In_makeG' : forall t v1 v2 ts s (w : ts ## v1 = Some t),
adamc@259 402 In (existT _ t (v1, v2)) (makeG' s)
adamc@259 403 -> hget s (makeVar w) = v2.
adamc@259 404 induction s; crush;
adamc@259 405 match goal with
adamc@259 406 | [ |- context[if ?E then _ else _] ] => destruct E; crush
adamc@259 407 end;
adamc@259 408 repeat match goal with
adamc@260 409 | [ |- context[match ?pf with refl_equal => _ end] ] =>
adamc@260 410 rewrite (UIP_refl _ _ pf)
adamc@259 411 end; crush; elimtype False; eauto.
adamc@259 412 Qed.
adamc@259 413
adamc@259 414 Hint Resolve In_makeG'.
adamc@259 415
adamc@260 416 (** Now the main inductive lemma can be stated and proved simply. *)
adamc@260 417
adamc@259 418 Lemma dbify_sound : forall G t (e1 : Phoas.exp _ t) (e2 : Phoas.exp _ t),
adamc@259 419 exp_equiv G e1 e2
adamc@259 420 -> forall ts (w : wf ts e1) s,
adamc@259 421 G = makeG' s
adamc@259 422 -> DeBruijn.expDenote (dbify e1 w) s = Phoas.expDenote e2.
adam@297 423 induction 1; crush; (let x := fresh in extensionality x); crush.
adamc@259 424 Qed.
adamc@259 425
adamc@260 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. *)
adamc@260 427
adamc@259 428 Theorem Dbify_sound : forall t (E : Exp t) (W : Wf E),
adamc@259 429 DeBruijn.expDenote (Dbify W) HNil = Phoas.ExpDenote E.
adamc@259 430 unfold Dbify, Phoas.ExpDenote; intros; eapply dbify_sound; eauto.
adamc@259 431 Qed.