Mercurial > cpdt > repo

annotate src/Intensional.v @ 314:d5787b70cf48

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rename Tactics; change 'principal typing' to 'principal types'
author Adam Chlipala <adam@chlipala.net>
date Wed, 07 Sep 2011 13:47:24 -0400
parents 7b38729be069
children
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@314 13 Require Import DepList CpdtTactics.
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
adam@302 192 ]]
adam@302 193 *)
adamc@260 194
adamc@257 195 Section vars.
adamc@257 196 Variables var1 var2 : type -> Type.
adamc@257 197
adamc@260 198 (** 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 199
adamc@260 200 Fixpoint zip G (s1 : hlist var1 G)
adamc@260 201 : hlist var2 G -> list {t : type & var1 t * var2 t}%type :=
adamc@257 202 match s1 with
adamc@257 203 | HNil => fun _ => nil
adamc@257 204 | HCons _ _ v1 s1' => fun s2 => existT _ _ (v1, hhd s2) :: zip s1' (htl s2)
adamc@257 205 end.
adamc@257 206
adamc@260 207 (** Two simple lemmas about [zip] will make useful hints. *)
adamc@260 208
adamc@257 209 Lemma In_zip : forall t G (s1 : hlist _ G) s2 (m : member t G),
adamc@257 210 In (existT _ t (hget s1 m, hget s2 m)) (zip s1 s2).
adamc@257 211 induction s1; intro s2; dep_destruct s2; intro m; dep_destruct m; crush.
adamc@257 212 Qed.
adamc@257 213
adamc@257 214 Lemma unsimpl_zip : forall t (v1 : var1 t) (v2 : var2 t)
adamc@257 215 G (s1 : hlist _ G) s2 t' (e1 : Phoas.exp _ t') e2,
adamc@257 216 exp_equiv (zip (v1 ::: s1) (v2 ::: s2)) e1 e2
adamc@257 217 -> exp_equiv (existT _ _ (v1, v2) :: zip s1 s2) e1 e2.
adamc@257 218 trivial.
adamc@257 219 Qed.
adamc@257 220
adamc@257 221 Hint Resolve In_zip unsimpl_zip.
adamc@257 222
adamc@260 223 (** Now it is trivial to prove the main inductive lemma about well-formedness. *)
adamc@260 224
adamc@260 225 Lemma phoasify_wf : forall G t (e : DeBruijn.exp G t) s1 s2,
adamc@257 226 exp_equiv (zip s1 s2) (phoasify e s1) (phoasify e s2).
adamc@257 227 Hint Constructors exp_equiv.
adamc@257 228
adamc@257 229 induction e; crush.
adamc@257 230 Qed.
adamc@257 231 End vars.
adamc@257 232
adamc@260 233 (** We apply [phoasify_wf] manually to prove the final theorem. *)
adamc@260 234
adamc@258 235 Theorem Phoasify_wf : forall t (e : DeBruijn.exp nil t),
adamc@258 236 Wf (Phoasify e).
adamc@258 237 unfold Wf, Phoasify; intros;
adamc@258 238 apply (phoasify_wf e (HNil (B := var1)) (HNil (B := var2))).
adamc@258 239 Qed.
adamc@258 240
adamc@260 241 (** 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 242
adamc@257 243
adamc@257 244 (** * From PHOAS to De Bruijn *)
adamc@258 245
adamc@260 246 (** 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 247
adamc@260 248 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 249
adamc@260 250 Fixpoint lookup (ts : list type) (n : nat) : option type :=
adamc@260 251 match ts with
adamc@258 252 | nil => None
adamc@260 253 | t :: ts' => if eq_nat_dec n (length ts') then Some t else lookup ts' n
adamc@258 254 end.
adamc@258 255
adamc@258 256 Infix "##" := lookup (left associativity, at level 1).
adamc@258 257
adamc@260 258 (** 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 259
adamc@258 260 Fixpoint wf (ts : list type) t (e : Phoas.exp (fun _ => nat) t) : Prop :=
adamc@258 261 match e with
adamc@258 262 | Phoas.Var t n => ts ## n = Some t
adamc@258 263 | Phoas.Const _ => True
adamc@258 264 | Phoas.Plus e1 e2 => wf ts e1 /\ wf ts e2
adamc@258 265 | Phoas.App _ _ e1 e2 => wf ts e1 /\ wf ts e2
adamc@258 266 | Phoas.Abs t1 _ e1 => wf (t1 :: ts) (e1 (length ts))
adamc@258 267 end.
adamc@258 268
adamc@260 269 (** ** Connecting Notions of Well-Formedness *)
adamc@260 270
adamc@260 271 (** 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 272
adamc@258 273 Fixpoint makeG (ts : list type) : list { t : type & nat * nat }%type :=
adamc@258 274 match ts with
adamc@258 275 | nil => nil
adamc@258 276 | t :: ts' => existT _ t (length ts', length ts') :: makeG ts'
adamc@258 277 end.
adamc@258 278
adamc@260 279 (** Now we prove a connection between [lookup] and [makeG], by way of a lemma about [lookup]. *)
adamc@260 280
adamc@258 281 Opaque eq_nat_dec.
adamc@258 282 Hint Extern 1 (_ >= _) => omega.
adamc@258 283
adamc@258 284 Lemma lookup_contra' : forall t ts n,
adamc@258 285 ts ## n = Some t
adamc@258 286 -> n >= length ts
adamc@258 287 -> False.
adamc@258 288 induction ts; crush;
adamc@258 289 match goal with
adamc@258 290 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E; crush
adamc@258 291 end; eauto.
adamc@258 292 Qed.
adamc@258 293
adamc@258 294 Lemma lookup_contra : forall t ts,
adamc@258 295 ts ## (length ts) = Some t
adamc@258 296 -> False.
adamc@258 297 intros; eapply lookup_contra'; eauto.
adamc@258 298 Qed.
adamc@258 299
adamc@258 300 Hint Resolve lookup_contra.
adamc@258 301
adamc@258 302 Lemma lookup_In : forall t v1 v2 ts,
adamc@258 303 In (existT (fun _ : type => (nat * nat)%type) t (v1, v2)) (makeG ts)
adamc@258 304 -> ts ## v1 = Some t.
adamc@258 305 induction ts; crush;
adamc@258 306 match goal with
adamc@258 307 | [ |- context[if ?E then _ else _] ] => destruct E; crush
adamc@258 308 end; elimtype False; eauto.
adamc@258 309 Qed.
adamc@258 310
adamc@258 311 Hint Resolve lookup_In.
adamc@258 312
adamc@260 313 (** We can prove the main inductive lemma by induction over [exp_equiv] derivations. *)
adamc@260 314
adamc@258 315 Hint Extern 1 (_ :: _ = makeG (_ :: _)) => reflexivity.
adamc@258 316
adamc@258 317 Lemma Wf_wf' : forall G t e1 (e2 : Phoas.exp (fun _ => nat) t),
adamc@258 318 exp_equiv G e1 e2
adamc@258 319 -> forall ts, G = makeG ts
adamc@258 320 -> wf ts e1.
adamc@258 321 induction 1; crush; eauto.
adamc@258 322 Qed.
adamc@258 323
adamc@258 324 Lemma Wf_wf : forall t (E : Exp t),
adamc@258 325 Wf E
adamc@258 326 -> wf nil (E (fun _ => nat)).
adamc@258 327 intros; eapply Wf_wf'; eauto.
adamc@258 328 Qed.
adamc@259 329
adamc@260 330 (** ** The Translation *)
adamc@260 331
adamc@260 332 (** 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 333
adamc@259 334 Theorem None_Some : forall T (x : T),
adamc@259 335 None = Some x
adamc@259 336 -> False.
adamc@259 337 congruence.
adamc@259 338 Qed.
adamc@259 339
adamc@259 340 Theorem Some_Some : forall T (x y : T),
adamc@259 341 Some x = Some y
adamc@259 342 -> x = y.
adamc@259 343 congruence.
adamc@259 344 Qed.
adamc@259 345
adamc@260 346 (** 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 347
adamc@259 348 Fixpoint makeVar {ts n t} : ts ## n = Some t -> member t ts :=
adamc@260 349 match ts with
adamc@259 350 | nil => fun Heq => match None_Some Heq with end
adamc@260 351 | t' :: ts' => if eq_nat_dec n (length ts') as b return (if b then _ else _) = _ -> _
adamc@260 352 then fun Heq => match Some_Some Heq with refl_equal => HFirst end
adamc@259 353 else fun Heq => HNext (makeVar Heq)
adamc@259 354 end.
adamc@259 355
adamc@260 356 (** Now [dbify] is straightforward to define. We use the functions [proj1] and [proj2] to decompose proofs of conjunctions. *)
adamc@259 357
adamc@259 358 Fixpoint dbify {ts} t (e : Phoas.exp (fun _ => nat) t) : wf ts e -> DeBruijn.exp ts t :=
adamc@259 359 match e in Phoas.exp _ t return wf ts e -> DeBruijn.exp ts t with
adamc@259 360 | Phoas.Var _ n => fun wf => DeBruijn.Var (makeVar wf)
adamc@259 361
adamc@259 362 | Phoas.Const n => fun _ => DeBruijn.Const n
adamc@260 363 | Phoas.Plus e1 e2 => fun wf =>
adamc@260 364 DeBruijn.Plus (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
adamc@259 365
adamc@260 366 | Phoas.App _ _ e1 e2 => fun wf =>
adamc@260 367 DeBruijn.App (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
adamc@259 368 | Phoas.Abs _ _ e1 => fun wf => DeBruijn.Abs (dbify (e1 (length ts)) wf)
adamc@259 369 end.
adamc@259 370
adamc@260 371 (** We define the parametric translation [Dbify] by appealing to the well-formedness translation theorem [Wf_wf] that we proved earlier. *)
adamc@260 372
adamc@259 373 Definition Dbify t (E : Phoas.Exp t) (W : Wf E) : DeBruijn.exp nil t :=
adamc@259 374 dbify (E _) (Wf_wf W).
adamc@259 375
adamc@260 376 (** To prove soundness, it is helpful to classify a set of contexts which depends on a de Bruijn index substitution. *)
adamc@260 377
adamc@260 378 Fixpoint makeG' ts (s : hlist typeDenote ts)
adamc@260 379 : list { t : type & nat * typeDenote t }%type :=
adamc@259 380 match s with
adamc@259 381 | HNil => nil
adamc@259 382 | HCons _ ts' v s' => existT _ _ (length ts', v) :: makeG' s'
adamc@259 383 end.
adamc@259 384
adamc@260 385 (** We prove an analogous lemma to the one we proved connecting [makeG] and [lookup]. This time, we connect [makeG'] and [hget]. *)
adamc@260 386
adamc@259 387 Lemma In_makeG'_contra' : forall t v2 ts (s : hlist _ ts) n,
adamc@259 388 In (existT _ t (n, v2)) (makeG' s)
adamc@259 389 -> n >= length ts
adamc@259 390 -> False.
adamc@259 391 induction s; crush; eauto.
adamc@259 392 Qed.
adamc@259 393
adamc@259 394 Lemma In_makeG'_contra : forall t v2 ts (s : hlist _ ts),
adamc@259 395 In (existT _ t (length ts, v2)) (makeG' s)
adamc@259 396 -> False.
adamc@259 397 intros; eapply In_makeG'_contra'; eauto.
adamc@259 398 Qed.
adamc@259 399
adamc@259 400 Hint Resolve In_makeG'_contra.
adamc@259 401
adamc@259 402 Lemma In_makeG' : forall t v1 v2 ts s (w : ts ## v1 = Some t),
adamc@259 403 In (existT _ t (v1, v2)) (makeG' s)
adamc@259 404 -> hget s (makeVar w) = v2.
adamc@259 405 induction s; crush;
adamc@259 406 match goal with
adamc@259 407 | [ |- context[if ?E then _ else _] ] => destruct E; crush
adamc@259 408 end;
adamc@259 409 repeat match goal with
adamc@260 410 | [ |- context[match ?pf with refl_equal => _ end] ] =>
adamc@260 411 rewrite (UIP_refl _ _ pf)
adamc@259 412 end; crush; elimtype False; eauto.
adamc@259 413 Qed.
adamc@259 414
adamc@259 415 Hint Resolve In_makeG'.
adamc@259 416
adamc@260 417 (** Now the main inductive lemma can be stated and proved simply. *)
adamc@260 418
adamc@259 419 Lemma dbify_sound : forall G t (e1 : Phoas.exp _ t) (e2 : Phoas.exp _ t),
adamc@259 420 exp_equiv G e1 e2
adamc@259 421 -> forall ts (w : wf ts e1) s,
adamc@259 422 G = makeG' s
adamc@259 423 -> DeBruijn.expDenote (dbify e1 w) s = Phoas.expDenote e2.
adam@297 424 induction 1; crush; (let x := fresh in extensionality x); crush.
adamc@259 425 Qed.
adamc@259 426
adamc@260 427 (** 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 428
adamc@259 429 Theorem Dbify_sound : forall t (E : Exp t) (W : Wf E),
adamc@259 430 DeBruijn.expDenote (Dbify W) HNil = Phoas.ExpDenote E.
adamc@259 431 unfold Dbify, Phoas.ExpDenote; intros; eapply dbify_sound; eauto.
adamc@259 432 Qed.