Mercurial > cpdt > repo

annotate 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
rev   line source
adamc@223 1 (* Copyright (c) 2008-2009, 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 *)
adamc@259 11 Require Import Arith Eqdep List.
adamc@257 12
adamc@257 13 Require Import Axioms 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@257 21 (* begin hide *)
adamc@257 22
adamc@257 23 Inductive type : Type :=
adamc@257 24 | Nat : type
adamc@257 25 | Arrow : type -> type -> type.
adamc@257 26
adamc@257 27 Infix "-->" := Arrow (right associativity, at level 60).
adamc@257 28
adamc@257 29 Fixpoint typeDenote (t : type) : Set :=
adamc@257 30 match t with
adamc@257 31 | Nat => nat
adamc@257 32 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@257 33 end.
adamc@257 34
adamc@257 35 Module Phoas.
adamc@257 36 Section vars.
adamc@257 37 Variable var : type -> Type.
adamc@257 38
adamc@257 39 Inductive exp : type -> Type :=
adamc@257 40 | Var : forall t,
adamc@257 41 var t
adamc@257 42 -> exp t
adamc@257 43
adamc@257 44 | Const : nat -> exp Nat
adamc@257 45 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@257 46
adamc@257 47 | App : forall t1 t2,
adamc@257 48 exp (t1 --> t2)
adamc@257 49 -> exp t1
adamc@257 50 -> exp t2
adamc@257 51 | Abs : forall t1 t2,
adamc@257 52 (var t1 -> exp t2)
adamc@257 53 -> exp (t1 --> t2).
adamc@257 54 End vars.
adamc@257 55
adamc@257 56 Definition Exp t := forall var, exp var t.
adamc@257 57
adamc@257 58 Implicit Arguments Var [var t].
adamc@257 59 Implicit Arguments Const [var].
adamc@257 60 Implicit Arguments Plus [var].
adamc@257 61 Implicit Arguments App [var t1 t2].
adamc@257 62 Implicit Arguments Abs [var t1 t2].
adamc@257 63
adamc@257 64 Notation "# v" := (Var v) (at level 70).
adamc@257 65
adamc@257 66 Notation "^ n" := (Const n) (at level 70).
adamc@257 67 Infix "+^" := Plus (left associativity, at level 79).
adamc@257 68
adamc@257 69 Infix "@" := App (left associativity, at level 77).
adamc@257 70 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@257 71 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@257 72
adamc@257 73 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@257 74 match e with
adamc@257 75 | Var _ v => v
adamc@257 76
adamc@257 77 | Const n => n
adamc@257 78 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@257 79
adamc@257 80 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@257 81 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@257 82 end.
adamc@257 83
adamc@257 84 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@257 85
adamc@257 86 Section exp_equiv.
adamc@257 87 Variables var1 var2 : type -> Type.
adamc@257 88
adamc@257 89 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type
adamc@257 90 -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@257 91 | EqVar : forall G t (v1 : var1 t) v2,
adamc@257 92 In (existT _ t (v1, v2)) G
adamc@257 93 -> exp_equiv G (#v1) (#v2)
adamc@257 94
adamc@257 95 | EqConst : forall G n,
adamc@257 96 exp_equiv G (^n) (^n)
adamc@257 97 | EqPlus : forall G x1 y1 x2 y2,
adamc@257 98 exp_equiv G x1 x2
adamc@257 99 -> exp_equiv G y1 y2
adamc@257 100 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@257 101
adamc@257 102 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@257 103 exp_equiv G f1 f2
adamc@257 104 -> exp_equiv G x1 x2
adamc@257 105 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@257 106 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@257 107 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@257 108 -> exp_equiv G (Abs f1) (Abs f2).
adamc@257 109 End exp_equiv.
adamc@258 110
adamc@258 111 Definition Wf t (E : Exp t) := forall var1 var2, exp_equiv nil (E var1) (E var2).
adamc@257 112 End Phoas.
adamc@257 113 (* end hide *)
adamc@257 114
adamc@257 115 Module DeBruijn.
adamc@257 116 Inductive exp : list type -> type -> Type :=
adamc@257 117 | Var : forall G t,
adamc@257 118 member t G
adamc@257 119 -> exp G t
adamc@257 120
adamc@257 121 | Const : forall G, nat -> exp G Nat
adamc@257 122 | Plus : forall G, exp G Nat -> exp G Nat -> exp G Nat
adamc@257 123
adamc@257 124 | App : forall G t1 t2,
adamc@257 125 exp G (t1 --> t2)
adamc@257 126 -> exp G t1
adamc@257 127 -> exp G t2
adamc@257 128 | Abs : forall G t1 t2,
adamc@257 129 exp (t1 :: G) t2
adamc@257 130 -> exp G (t1 --> t2).
adamc@257 131
adamc@257 132 Implicit Arguments Const [G].
adamc@257 133
adamc@257 134 Fixpoint expDenote G t (e : exp G t) : hlist typeDenote G -> typeDenote t :=
adamc@257 135 match e with
adamc@257 136 | Var _ _ v => fun s => hget s v
adamc@257 137
adamc@257 138 | Const _ n => fun _ => n
adamc@257 139 | Plus _ e1 e2 => fun s => expDenote e1 s + expDenote e2 s
adamc@257 140
adamc@257 141 | App _ _ _ e1 e2 => fun s => (expDenote e1 s) (expDenote e2 s)
adamc@257 142 | Abs _ _ _ e' => fun s x => expDenote e' (x ::: s)
adamc@257 143 end.
adamc@257 144 End DeBruijn.
adamc@257 145
adamc@257 146 Import Phoas DeBruijn.
adamc@257 147
adamc@257 148
adamc@257 149 (** * From De Bruijn to PHOAS *)
adamc@257 150
adamc@257 151 Section phoasify.
adamc@257 152 Variable var : type -> Type.
adamc@257 153
adamc@257 154 Fixpoint phoasify G t (e : DeBruijn.exp G t) : hlist var G -> Phoas.exp var t :=
adamc@257 155 match e with
adamc@257 156 | Var _ _ v => fun s => #(hget s v)
adamc@257 157
adamc@257 158 | Const _ n => fun _ => ^n
adamc@257 159 | Plus _ e1 e2 => fun s => phoasify e1 s +^ phoasify e2 s
adamc@257 160
adamc@257 161 | App _ _ _ e1 e2 => fun s => phoasify e1 s @ phoasify e2 s
adamc@257 162 | Abs _ _ _ e' => fun s => \x, phoasify e' (x ::: s)
adamc@257 163 end.
adamc@257 164 End phoasify.
adamc@257 165
adamc@257 166 Definition Phoasify t (e : DeBruijn.exp nil t) : Phoas.Exp t :=
adamc@257 167 fun _ => phoasify e HNil.
adamc@257 168
adamc@257 169 Theorem phoasify_sound : forall G t (e : DeBruijn.exp G t) s,
adamc@257 170 Phoas.expDenote (phoasify e s) = DeBruijn.expDenote e s.
adamc@257 171 induction e; crush; ext_eq; crush.
adamc@257 172 Qed.
adamc@257 173
adamc@257 174 Section vars.
adamc@257 175 Variables var1 var2 : type -> Type.
adamc@257 176
adamc@257 177 Fixpoint zip G (s1 : hlist var1 G) : hlist var2 G -> list {t : type & var1 t * var2 t}%type :=
adamc@257 178 match s1 with
adamc@257 179 | HNil => fun _ => nil
adamc@257 180 | HCons _ _ v1 s1' => fun s2 => existT _ _ (v1, hhd s2) :: zip s1' (htl s2)
adamc@257 181 end.
adamc@257 182
adamc@257 183 Lemma In_zip : forall t G (s1 : hlist _ G) s2 (m : member t G),
adamc@257 184 In (existT _ t (hget s1 m, hget s2 m)) (zip s1 s2).
adamc@257 185 induction s1; intro s2; dep_destruct s2; intro m; dep_destruct m; crush.
adamc@257 186 Qed.
adamc@257 187
adamc@257 188 Lemma unsimpl_zip : forall t (v1 : var1 t) (v2 : var2 t)
adamc@257 189 G (s1 : hlist _ G) s2 t' (e1 : Phoas.exp _ t') e2,
adamc@257 190 exp_equiv (zip (v1 ::: s1) (v2 ::: s2)) e1 e2
adamc@257 191 -> exp_equiv (existT _ _ (v1, v2) :: zip s1 s2) e1 e2.
adamc@257 192 trivial.
adamc@257 193 Qed.
adamc@257 194
adamc@257 195 Hint Resolve In_zip unsimpl_zip.
adamc@257 196
adamc@257 197 Theorem phoasify_wf : forall G t (e : DeBruijn.exp G t) s1 s2,
adamc@257 198 exp_equiv (zip s1 s2) (phoasify e s1) (phoasify e s2).
adamc@257 199 Hint Constructors exp_equiv.
adamc@257 200
adamc@257 201 induction e; crush.
adamc@257 202 Qed.
adamc@257 203 End vars.
adamc@257 204
adamc@258 205 Theorem Phoasify_wf : forall t (e : DeBruijn.exp nil t),
adamc@258 206 Wf (Phoasify e).
adamc@258 207 unfold Wf, Phoasify; intros;
adamc@258 208 apply (phoasify_wf e (HNil (B := var1)) (HNil (B := var2))).
adamc@258 209 Qed.
adamc@258 210
adamc@257 211
adamc@257 212 (** * From PHOAS to De Bruijn *)
adamc@258 213
adamc@258 214 Fixpoint lookup (G : list type) (n : nat) : option type :=
adamc@258 215 match G with
adamc@258 216 | nil => None
adamc@258 217 | t :: G' => if eq_nat_dec n (length G') then Some t else lookup G' n
adamc@258 218 end.
adamc@258 219
adamc@258 220 Infix "##" := lookup (left associativity, at level 1).
adamc@258 221
adamc@258 222 Fixpoint wf (ts : list type) t (e : Phoas.exp (fun _ => nat) t) : Prop :=
adamc@258 223 match e with
adamc@258 224 | Phoas.Var t n => ts ## n = Some t
adamc@258 225 | Phoas.Const _ => True
adamc@258 226 | Phoas.Plus e1 e2 => wf ts e1 /\ wf ts e2
adamc@258 227 | Phoas.App _ _ e1 e2 => wf ts e1 /\ wf ts e2
adamc@258 228 | Phoas.Abs t1 _ e1 => wf (t1 :: ts) (e1 (length ts))
adamc@258 229 end.
adamc@258 230
adamc@258 231 Fixpoint makeG (ts : list type) : list { t : type & nat * nat }%type :=
adamc@258 232 match ts with
adamc@258 233 | nil => nil
adamc@258 234 | t :: ts' => existT _ t (length ts', length ts') :: makeG ts'
adamc@258 235 end.
adamc@258 236
adamc@258 237 Opaque eq_nat_dec.
adamc@258 238 Hint Extern 1 (_ >= _) => omega.
adamc@258 239
adamc@258 240 Lemma lookup_contra' : forall t ts n,
adamc@258 241 ts ## n = Some t
adamc@258 242 -> n >= length ts
adamc@258 243 -> False.
adamc@258 244 induction ts; crush;
adamc@258 245 match goal with
adamc@258 246 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E; crush
adamc@258 247 end; eauto.
adamc@258 248 Qed.
adamc@258 249
adamc@258 250 Lemma lookup_contra : forall t ts,
adamc@258 251 ts ## (length ts) = Some t
adamc@258 252 -> False.
adamc@258 253 intros; eapply lookup_contra'; eauto.
adamc@258 254 Qed.
adamc@258 255
adamc@258 256 Hint Resolve lookup_contra.
adamc@258 257
adamc@258 258 Lemma lookup_In : forall t v1 v2 ts,
adamc@258 259 In (existT (fun _ : type => (nat * nat)%type) t (v1, v2)) (makeG ts)
adamc@258 260 -> ts ## v1 = Some t.
adamc@258 261 induction ts; crush;
adamc@258 262 match goal with
adamc@258 263 | [ |- context[if ?E then _ else _] ] => destruct E; crush
adamc@258 264 end; elimtype False; eauto.
adamc@258 265 Qed.
adamc@258 266
adamc@258 267 Hint Resolve lookup_In.
adamc@258 268
adamc@258 269 Hint Extern 1 (_ :: _ = makeG (_ :: _)) => reflexivity.
adamc@258 270
adamc@258 271 Lemma Wf_wf' : forall G t e1 (e2 : Phoas.exp (fun _ => nat) t),
adamc@258 272 exp_equiv G e1 e2
adamc@258 273 -> forall ts, G = makeG ts
adamc@258 274 -> wf ts e1.
adamc@258 275 induction 1; crush; eauto.
adamc@258 276 Qed.
adamc@258 277
adamc@258 278 Lemma Wf_wf : forall t (E : Exp t),
adamc@258 279 Wf E
adamc@258 280 -> wf nil (E (fun _ => nat)).
adamc@258 281 intros; eapply Wf_wf'; eauto.
adamc@258 282 Qed.
adamc@259 283
adamc@259 284 Theorem None_Some : forall T (x : T),
adamc@259 285 None = Some x
adamc@259 286 -> False.
adamc@259 287 congruence.
adamc@259 288 Qed.
adamc@259 289
adamc@259 290 Theorem Some_Some : forall T (x y : T),
adamc@259 291 Some x = Some y
adamc@259 292 -> x = y.
adamc@259 293 congruence.
adamc@259 294 Qed.
adamc@259 295
adamc@259 296 Fixpoint makeVar {ts n t} : ts ## n = Some t -> member t ts :=
adamc@259 297 match ts return ts ## n = Some t -> member t ts with
adamc@259 298 | nil => fun Heq => match None_Some Heq with end
adamc@259 299 | t' :: ts' => if eq_nat_dec n (length ts') as b
adamc@259 300 return (if b then Some t' else lookup ts' n) = Some t -> member t (t' :: ts')
adamc@259 301 then fun Heq => match Some_Some Heq in _ = t0 return member t0 (t' :: ts') with
adamc@259 302 | refl_equal => HFirst
adamc@259 303 end
adamc@259 304 else fun Heq => HNext (makeVar Heq)
adamc@259 305 end.
adamc@259 306
adamc@259 307 Axiom cheat : forall T, T.
adamc@259 308
adamc@259 309 Fixpoint dbify {ts} t (e : Phoas.exp (fun _ => nat) t) : wf ts e -> DeBruijn.exp ts t :=
adamc@259 310 match e in Phoas.exp _ t return wf ts e -> DeBruijn.exp ts t with
adamc@259 311 | Phoas.Var _ n => fun wf => DeBruijn.Var (makeVar wf)
adamc@259 312
adamc@259 313 | Phoas.Const n => fun _ => DeBruijn.Const n
adamc@259 314 | Phoas.Plus e1 e2 => fun wf => DeBruijn.Plus (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
adamc@259 315
adamc@259 316 | Phoas.App _ _ e1 e2 => fun wf => DeBruijn.App (dbify e1 (proj1 wf)) (dbify e2 (proj2 wf))
adamc@259 317 | Phoas.Abs _ _ e1 => fun wf => DeBruijn.Abs (dbify (e1 (length ts)) wf)
adamc@259 318 end.
adamc@259 319
adamc@259 320 Definition Dbify t (E : Phoas.Exp t) (W : Wf E) : DeBruijn.exp nil t :=
adamc@259 321 dbify (E _) (Wf_wf W).
adamc@259 322
adamc@259 323 Fixpoint makeG' ts (s : hlist typeDenote ts) : list { t : type & nat * typeDenote t }%type :=
adamc@259 324 match s with
adamc@259 325 | HNil => nil
adamc@259 326 | HCons _ ts' v s' => existT _ _ (length ts', v) :: makeG' s'
adamc@259 327 end.
adamc@259 328
adamc@259 329 Lemma In_makeG'_contra' : forall t v2 ts (s : hlist _ ts) n,
adamc@259 330 In (existT _ t (n, v2)) (makeG' s)
adamc@259 331 -> n >= length ts
adamc@259 332 -> False.
adamc@259 333 induction s; crush; eauto.
adamc@259 334 Qed.
adamc@259 335
adamc@259 336 Lemma In_makeG'_contra : forall t v2 ts (s : hlist _ ts),
adamc@259 337 In (existT _ t (length ts, v2)) (makeG' s)
adamc@259 338 -> False.
adamc@259 339 intros; eapply In_makeG'_contra'; eauto.
adamc@259 340 Qed.
adamc@259 341
adamc@259 342 Hint Resolve In_makeG'_contra.
adamc@259 343
adamc@259 344 Lemma In_makeG' : forall t v1 v2 ts s (w : ts ## v1 = Some t),
adamc@259 345 In (existT _ t (v1, v2)) (makeG' s)
adamc@259 346 -> hget s (makeVar w) = v2.
adamc@259 347 induction s; crush;
adamc@259 348 match goal with
adamc@259 349 | [ |- context[if ?E then _ else _] ] => destruct E; crush
adamc@259 350 end;
adamc@259 351 repeat match goal with
adamc@259 352 | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf)
adamc@259 353 end; crush; elimtype False; eauto.
adamc@259 354 Qed.
adamc@259 355
adamc@259 356 Hint Resolve In_makeG'.
adamc@259 357
adamc@259 358 Lemma dbify_sound : forall G t (e1 : Phoas.exp _ t) (e2 : Phoas.exp _ t),
adamc@259 359 exp_equiv G e1 e2
adamc@259 360 -> forall ts (w : wf ts e1) s,
adamc@259 361 G = makeG' s
adamc@259 362 -> DeBruijn.expDenote (dbify e1 w) s = Phoas.expDenote e2.
adamc@259 363 induction 1; crush; ext_eq; crush.
adamc@259 364 Qed.
adamc@259 365
adamc@259 366 Theorem Dbify_sound : forall t (E : Exp t) (W : Wf E),
adamc@259 367 DeBruijn.expDenote (Dbify W) HNil = Phoas.ExpDenote E.
adamc@259 368 unfold Dbify, Phoas.ExpDenote; intros; eapply dbify_sound; eauto.
adamc@259 369 Qed.