Mercurial > cpdt > repo

annotate src/Intensional.v @ 188:aec05464fedd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Automated ccExp_correct
author Adam Chlipala <adamc@hcoop.net>
date Mon, 17 Nov 2008 10:31:22 -0500
parents 71c076dd5f31
children 0198181d1b64
rev   line source
adamc@182 1 (* Copyright (c) 2008, 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@182 10 (* begin hide *)
adamc@184 11 Require Import Arith Bool String List Eqdep JMeq.
adamc@182 12
adamc@182 13 Require Import Axioms Tactics DepList.
adamc@182 14
adamc@182 15 Set Implicit Arguments.
adamc@184 16
adamc@184 17 Infix "==" := JMeq (at level 70, no associativity).
adamc@182 18 (* end hide *)
adamc@182 19
adamc@182 20
adamc@184 21
adamc@184 22
adamc@182 23 (** %\chapter{Intensional Transformations}% *)
adamc@182 24
adamc@182 25 (** TODO: Prose for this chapter *)
adamc@182 26
adamc@182 27
adamc@182 28 (** * Closure Conversion *)
adamc@182 29
adamc@182 30 Module Source.
adamc@182 31 Inductive type : Type :=
adamc@182 32 | TNat : type
adamc@182 33 | Arrow : type -> type -> type.
adamc@182 34
adamc@182 35 Notation "'Nat'" := TNat : source_scope.
adamc@182 36 Infix "-->" := Arrow (right associativity, at level 60) : source_scope.
adamc@182 37
adamc@182 38 Open Scope source_scope.
adamc@182 39 Bind Scope source_scope with type.
adamc@182 40 Delimit Scope source_scope with source.
adamc@182 41
adamc@182 42 Section vars.
adamc@182 43 Variable var : type -> Type.
adamc@182 44
adamc@182 45 Inductive exp : type -> Type :=
adamc@182 46 | Var : forall t,
adamc@182 47 var t
adamc@182 48 -> exp t
adamc@182 49
adamc@182 50 | Const : nat -> exp Nat
adamc@182 51 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@182 52
adamc@182 53 | App : forall t1 t2,
adamc@182 54 exp (t1 --> t2)
adamc@182 55 -> exp t1
adamc@182 56 -> exp t2
adamc@182 57 | Abs : forall t1 t2,
adamc@182 58 (var t1 -> exp t2)
adamc@182 59 -> exp (t1 --> t2).
adamc@182 60 End vars.
adamc@182 61
adamc@182 62 Definition Exp t := forall var, exp var t.
adamc@182 63
adamc@182 64 Implicit Arguments Var [var t].
adamc@182 65 Implicit Arguments Const [var].
adamc@182 66 Implicit Arguments Plus [var].
adamc@182 67 Implicit Arguments App [var t1 t2].
adamc@182 68 Implicit Arguments Abs [var t1 t2].
adamc@182 69
adamc@182 70 Notation "# v" := (Var v) (at level 70) : source_scope.
adamc@182 71
adamc@182 72 Notation "^ n" := (Const n) (at level 70) : source_scope.
adamc@182 73 Infix "+^" := Plus (left associativity, at level 79) : source_scope.
adamc@182 74
adamc@182 75 Infix "@" := App (left associativity, at level 77) : source_scope.
adamc@182 76 Notation "\ x , e" := (Abs (fun x => e)) (at level 78) : source_scope.
adamc@182 77 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78) : source_scope.
adamc@182 78
adamc@182 79 Bind Scope source_scope with exp.
adamc@182 80
adamc@182 81 Definition zero : Exp Nat := fun _ => ^0.
adamc@182 82 Definition one : Exp Nat := fun _ => ^1.
adamc@182 83 Definition zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@182 84 Definition ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@182 85 Definition app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@182 86 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@182 87 \f, \x, #f @ #x.
adamc@182 88 Definition app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@182 89
adamc@182 90 Fixpoint typeDenote (t : type) : Set :=
adamc@182 91 match t with
adamc@182 92 | Nat => nat
adamc@182 93 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@182 94 end.
adamc@182 95
adamc@182 96 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@182 97 match e in (exp _ t) return (typeDenote t) with
adamc@182 98 | Var _ v => v
adamc@182 99
adamc@182 100 | Const n => n
adamc@182 101 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@182 102
adamc@182 103 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@182 104 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@182 105 end.
adamc@182 106
adamc@182 107 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@182 108
adamc@182 109 Section exp_equiv.
adamc@182 110 Variables var1 var2 : type -> Type.
adamc@182 111
adamc@182 112 Inductive exp_equiv : list { t : type & var1 t * var2 t }%type -> forall t, exp var1 t -> exp var2 t -> Prop :=
adamc@182 113 | EqVar : forall G t (v1 : var1 t) v2,
adamc@182 114 In (existT _ t (v1, v2)) G
adamc@182 115 -> exp_equiv G (#v1) (#v2)
adamc@182 116
adamc@182 117 | EqConst : forall G n,
adamc@182 118 exp_equiv G (^n) (^n)
adamc@182 119 | EqPlus : forall G x1 y1 x2 y2,
adamc@182 120 exp_equiv G x1 x2
adamc@182 121 -> exp_equiv G y1 y2
adamc@182 122 -> exp_equiv G (x1 +^ y1) (x2 +^ y2)
adamc@182 123
adamc@182 124 | EqApp : forall G t1 t2 (f1 : exp _ (t1 --> t2)) (x1 : exp _ t1) f2 x2,
adamc@182 125 exp_equiv G f1 f2
adamc@182 126 -> exp_equiv G x1 x2
adamc@182 127 -> exp_equiv G (f1 @ x1) (f2 @ x2)
adamc@182 128 | EqAbs : forall G t1 t2 (f1 : var1 t1 -> exp var1 t2) f2,
adamc@182 129 (forall v1 v2, exp_equiv (existT _ t1 (v1, v2) :: G) (f1 v1) (f2 v2))
adamc@182 130 -> exp_equiv G (Abs f1) (Abs f2).
adamc@182 131 End exp_equiv.
adamc@182 132
adamc@182 133 Axiom Exp_equiv : forall t (E : Exp t) var1 var2,
adamc@182 134 exp_equiv nil (E var1) (E var2).
adamc@182 135 End Source.
adamc@182 136
adamc@183 137 Module Closed.
adamc@182 138 Inductive type : Type :=
adamc@182 139 | TNat : type
adamc@182 140 | Arrow : type -> type -> type
adamc@182 141 | Code : type -> type -> type -> type
adamc@182 142 | Prod : type -> type -> type
adamc@182 143 | TUnit : type.
adamc@182 144
adamc@182 145 Notation "'Nat'" := TNat : cc_scope.
adamc@182 146 Notation "'Unit'" := TUnit : cc_scope.
adamc@182 147 Infix "-->" := Arrow (right associativity, at level 60) : cc_scope.
adamc@182 148 Infix "**" := Prod (right associativity, at level 59) : cc_scope.
adamc@182 149 Notation "env @@ dom ---> ran" := (Code env dom ran) (no associativity, at level 62, dom at next level) : cc_scope.
adamc@182 150
adamc@182 151 Bind Scope cc_scope with type.
adamc@182 152 Delimit Scope cc_scope with cc.
adamc@182 153
adamc@182 154 Open Local Scope cc_scope.
adamc@182 155
adamc@182 156 Section vars.
adamc@182 157 Variable var : type -> Set.
adamc@182 158
adamc@182 159 Inductive exp : type -> Type :=
adamc@182 160 | Var : forall t,
adamc@182 161 var t
adamc@182 162 -> exp t
adamc@182 163
adamc@182 164 | Const : nat -> exp Nat
adamc@182 165 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@182 166
adamc@182 167 | App : forall dom ran,
adamc@182 168 exp (dom --> ran)
adamc@182 169 -> exp dom
adamc@182 170 -> exp ran
adamc@182 171
adamc@182 172 | Pack : forall env dom ran,
adamc@182 173 exp (env @@ dom ---> ran)
adamc@182 174 -> exp env
adamc@182 175 -> exp (dom --> ran)
adamc@182 176
adamc@182 177 | EUnit : exp Unit
adamc@182 178
adamc@182 179 | Pair : forall t1 t2,
adamc@182 180 exp t1
adamc@182 181 -> exp t2
adamc@182 182 -> exp (t1 ** t2)
adamc@182 183 | Fst : forall t1 t2,
adamc@182 184 exp (t1 ** t2)
adamc@182 185 -> exp t1
adamc@182 186 | Snd : forall t1 t2,
adamc@182 187 exp (t1 ** t2)
adamc@183 188 -> exp t2
adamc@183 189
adamc@183 190 | Let : forall t1 t2,
adamc@183 191 exp t1
adamc@183 192 -> (var t1 -> exp t2)
adamc@182 193 -> exp t2.
adamc@182 194
adamc@182 195 Section funcs.
adamc@182 196 Variable T : Type.
adamc@182 197
adamc@182 198 Inductive funcs : Type :=
adamc@182 199 | Main : T -> funcs
adamc@182 200 | Abs : forall env dom ran,
adamc@182 201 (var env -> var dom -> exp ran)
adamc@182 202 -> (var (env @@ dom ---> ran) -> funcs)
adamc@182 203 -> funcs.
adamc@182 204 End funcs.
adamc@182 205
adamc@182 206 Definition prog t := funcs (exp t).
adamc@182 207 End vars.
adamc@182 208
adamc@182 209 Implicit Arguments Var [var t].
adamc@182 210 Implicit Arguments Const [var].
adamc@182 211 Implicit Arguments EUnit [var].
adamc@182 212 Implicit Arguments Fst [var t1 t2].
adamc@182 213 Implicit Arguments Snd [var t1 t2].
adamc@182 214
adamc@182 215 Implicit Arguments Main [var T].
adamc@182 216 Implicit Arguments Abs [var T env dom ran].
adamc@182 217
adamc@182 218 Notation "# v" := (Var v) (at level 70) : cc_scope.
adamc@182 219
adamc@182 220 Notation "^ n" := (Const n) (at level 70) : cc_scope.
adamc@182 221 Infix "+^" := Plus (left associativity, at level 79) : cc_scope.
adamc@182 222
adamc@183 223 Infix "@" := App (left associativity, at level 77) : cc_scope.
adamc@182 224 Infix "##" := Pack (no associativity, at level 71) : cc_scope.
adamc@182 225
adamc@182 226 Notation "()" := EUnit : cc_scope.
adamc@182 227
adamc@182 228 Notation "[ x1 , x2 ]" := (Pair x1 x2) (at level 73) : cc_scope.
adamc@182 229 Notation "#1 x" := (Fst x) (at level 72) : cc_scope.
adamc@182 230 Notation "#2 x" := (Snd x) (at level 72) : cc_scope.
adamc@182 231
adamc@183 232 Notation "f <== \\ x , y , e ; fs" :=
adamc@182 233 (Abs (fun x y => e) (fun f => fs))
adamc@182 234 (right associativity, at level 80, e at next level) : cc_scope.
adamc@187 235 Notation "f <== \\ ! , y , e ; fs" :=
adamc@187 236 (Abs (fun _ y => e) (fun f => fs))
adamc@187 237 (right associativity, at level 80, e at next level) : cc_scope.
adamc@187 238 Notation "f <== \\ x , ! , e ; fs" :=
adamc@187 239 (Abs (fun x _ => e) (fun f => fs))
adamc@187 240 (right associativity, at level 80, e at next level) : cc_scope.
adamc@187 241 Notation "f <== \\ ! , ! , e ; fs" :=
adamc@187 242 (Abs (fun _ _ => e) (fun f => fs))
adamc@187 243 (right associativity, at level 80, e at next level) : cc_scope.
adamc@182 244
adamc@183 245 Notation "x <- e1 ; e2" := (Let e1 (fun x => e2))
adamc@183 246 (right associativity, at level 80, e1 at next level) : cc_scope.
adamc@183 247
adamc@182 248 Bind Scope cc_scope with exp funcs prog.
adamc@182 249
adamc@182 250 Fixpoint typeDenote (t : type) : Set :=
adamc@182 251 match t with
adamc@182 252 | Nat => nat
adamc@182 253 | Unit => unit
adamc@182 254 | dom --> ran => typeDenote dom -> typeDenote ran
adamc@182 255 | t1 ** t2 => typeDenote t1 * typeDenote t2
adamc@182 256 | env @@ dom ---> ran => typeDenote env -> typeDenote dom -> typeDenote ran
adamc@182 257 end%type.
adamc@182 258
adamc@182 259 Fixpoint expDenote t (e : exp typeDenote t) {struct e} : typeDenote t :=
adamc@182 260 match e in (exp _ t) return (typeDenote t) with
adamc@182 261 | Var _ v => v
adamc@182 262
adamc@182 263 | Const n => n
adamc@182 264 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@182 265
adamc@182 266 | App _ _ f x => (expDenote f) (expDenote x)
adamc@182 267 | Pack _ _ _ f env => (expDenote f) (expDenote env)
adamc@182 268
adamc@182 269 | EUnit => tt
adamc@182 270
adamc@182 271 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@182 272 | Fst _ _ e' => fst (expDenote e')
adamc@182 273 | Snd _ _ e' => snd (expDenote e')
adamc@183 274
adamc@183 275 | Let _ _ e1 e2 => expDenote (e2 (expDenote e1))
adamc@182 276 end.
adamc@182 277
adamc@182 278 Fixpoint funcsDenote T (fs : funcs typeDenote T) : T :=
adamc@182 279 match fs with
adamc@182 280 | Main v => v
adamc@182 281 | Abs _ _ _ e fs =>
adamc@182 282 funcsDenote (fs (fun env arg => expDenote (e env arg)))
adamc@182 283 end.
adamc@182 284
adamc@182 285 Definition progDenote t (p : prog typeDenote t) : typeDenote t :=
adamc@182 286 expDenote (funcsDenote p).
adamc@182 287
adamc@182 288 Definition Exp t := forall var, exp var t.
adamc@182 289 Definition Prog t := forall var, prog var t.
adamc@182 290
adamc@182 291 Definition ExpDenote t (E : Exp t) := expDenote (E _).
adamc@182 292 Definition ProgDenote t (P : Prog t) := progDenote (P _).
adamc@182 293 End Closed.
adamc@182 294
adamc@183 295 Import Source Closed.
adamc@183 296
adamc@183 297 Section splice.
adamc@183 298 Open Local Scope cc_scope.
adamc@183 299
adamc@183 300 Fixpoint spliceFuncs var T1 (fs : funcs var T1)
adamc@183 301 T2 (f : T1 -> funcs var T2) {struct fs} : funcs var T2 :=
adamc@183 302 match fs with
adamc@183 303 | Main v => f v
adamc@183 304 | Abs _ _ _ e fs' => Abs e (fun x => spliceFuncs (fs' x) f)
adamc@183 305 end.
adamc@183 306 End splice.
adamc@183 307
adamc@183 308 Notation "x <-- e1 ; e2" := (spliceFuncs e1 (fun x => e2))
adamc@183 309 (right associativity, at level 80, e1 at next level) : cc_scope.
adamc@183 310
adamc@183 311 Definition natvar (_ : Source.type) := nat.
adamc@183 312 Definition isfree := hlist (fun (_ : Source.type) => bool).
adamc@183 313
adamc@183 314 Ltac maybe_destruct E :=
adamc@183 315 match goal with
adamc@183 316 | [ x : _ |- _ ] =>
adamc@183 317 match E with
adamc@183 318 | x => idtac
adamc@183 319 end
adamc@183 320 | _ =>
adamc@183 321 match E with
adamc@183 322 | eq_nat_dec _ _ => idtac
adamc@183 323 end
adamc@183 324 end; destruct E.
adamc@183 325
adamc@183 326 Ltac my_crush :=
adamc@183 327 crush; repeat (match goal with
adamc@183 328 | [ x : (_ * _)%type |- _ ] => destruct x
adamc@183 329 | [ |- context[if ?B then _ else _] ] => maybe_destruct B
adamc@183 330 | [ _ : context[if ?B then _ else _] |- _ ] => maybe_destruct B
adamc@183 331 end; crush).
adamc@183 332
adamc@183 333 Section isfree.
adamc@183 334 Import Source.
adamc@183 335 Open Local Scope source_scope.
adamc@183 336
adamc@183 337 Fixpoint lookup_type (envT : list Source.type) (n : nat) {struct envT}
adamc@183 338 : isfree envT -> option Source.type :=
adamc@183 339 match envT return (isfree envT -> _) with
adamc@183 340 | nil => fun _ => None
adamc@183 341 | first :: rest => fun fvs =>
adamc@183 342 if eq_nat_dec n (length rest)
adamc@183 343 then match fvs with
adamc@183 344 | (true, _) => Some first
adamc@183 345 | (false, _) => None
adamc@183 346 end
adamc@183 347 else lookup_type rest n (snd fvs)
adamc@183 348 end.
adamc@183 349
adamc@183 350 Implicit Arguments lookup_type [envT].
adamc@183 351
adamc@183 352 Notation ok := (fun (envT : list Source.type) (fvs : isfree envT)
adamc@183 353 (n : nat) (t : Source.type)
adamc@183 354 => lookup_type n fvs = Some t).
adamc@183 355
adamc@183 356 Fixpoint wfExp (envT : list Source.type) (fvs : isfree envT)
adamc@183 357 t (e : Source.exp natvar t) {struct e} : Prop :=
adamc@183 358 match e with
adamc@183 359 | Var t v => ok envT fvs v t
adamc@183 360
adamc@183 361 | Const _ => True
adamc@183 362 | Plus e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
adamc@183 363
adamc@183 364 | App _ _ e1 e2 => wfExp envT fvs e1 /\ wfExp envT fvs e2
adamc@183 365 | Abs dom _ e' => wfExp (dom :: envT) (true ::: fvs) (e' (length envT))
adamc@183 366 end.
adamc@183 367
adamc@183 368 Implicit Arguments wfExp [envT t].
adamc@183 369
adamc@183 370 Theorem wfExp_weaken : forall t (e : exp natvar t) envT (fvs fvs' : isfree envT),
adamc@183 371 wfExp fvs e
adamc@183 372 -> (forall n t, ok _ fvs n t -> ok _ fvs' n t)
adamc@183 373 -> wfExp fvs' e.
adamc@183 374 Hint Extern 1 (lookup_type (envT := _ :: _) _ _ = Some _) =>
adamc@183 375 simpl in *; my_crush.
adamc@183 376
adamc@183 377 induction e; my_crush; eauto.
adamc@183 378 Defined.
adamc@183 379
adamc@183 380 Fixpoint isfree_none (envT : list Source.type) : isfree envT :=
adamc@183 381 match envT return (isfree envT) with
adamc@183 382 | nil => tt
adamc@183 383 | _ :: _ => (false, isfree_none _)
adamc@183 384 end.
adamc@183 385
adamc@183 386 Implicit Arguments isfree_none [envT].
adamc@183 387
adamc@183 388 Fixpoint isfree_one (envT : list Source.type) (n : nat) {struct envT} : isfree envT :=
adamc@183 389 match envT return (isfree envT) with
adamc@183 390 | nil => tt
adamc@183 391 | _ :: rest =>
adamc@183 392 if eq_nat_dec n (length rest)
adamc@183 393 then (true, isfree_none)
adamc@183 394 else (false, isfree_one _ n)
adamc@183 395 end.
adamc@183 396
adamc@183 397 Implicit Arguments isfree_one [envT].
adamc@183 398
adamc@183 399 Fixpoint isfree_merge (envT : list Source.type) : isfree envT -> isfree envT -> isfree envT :=
adamc@183 400 match envT return (isfree envT -> isfree envT -> isfree envT) with
adamc@183 401 | nil => fun _ _ => tt
adamc@183 402 | _ :: _ => fun fv1 fv2 => (fst fv1 || fst fv2, isfree_merge _ (snd fv1) (snd fv2))
adamc@183 403 end.
adamc@183 404
adamc@183 405 Implicit Arguments isfree_merge [envT].
adamc@183 406
adamc@183 407 Fixpoint fvsExp t (e : exp natvar t)
adamc@183 408 (envT : list Source.type) {struct e} : isfree envT :=
adamc@183 409 match e with
adamc@183 410 | Var _ n => isfree_one n
adamc@183 411
adamc@183 412 | Const _ => isfree_none
adamc@183 413 | Plus e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
adamc@183 414
adamc@183 415 | App _ _ e1 e2 => isfree_merge (fvsExp e1 envT) (fvsExp e2 envT)
adamc@183 416 | Abs dom _ e' => snd (fvsExp (e' (length envT)) (dom :: envT))
adamc@183 417 end.
adamc@183 418
adamc@183 419 Lemma isfree_one_correct : forall t (v : natvar t) envT fvs,
adamc@183 420 ok envT fvs v t
adamc@183 421 -> ok envT (isfree_one (envT:=envT) v) v t.
adamc@183 422 induction envT; my_crush; eauto.
adamc@183 423 Defined.
adamc@183 424
adamc@183 425 Lemma isfree_merge_correct1 : forall t (v : natvar t) envT fvs1 fvs2,
adamc@183 426 ok envT fvs1 v t
adamc@183 427 -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
adamc@183 428 induction envT; my_crush; eauto.
adamc@183 429 Defined.
adamc@183 430
adamc@183 431 Hint Rewrite orb_true_r : cpdt.
adamc@183 432
adamc@183 433 Lemma isfree_merge_correct2 : forall t (v : natvar t) envT fvs1 fvs2,
adamc@183 434 ok envT fvs2 v t
adamc@183 435 -> ok envT (isfree_merge (envT:=envT) fvs1 fvs2) v t.
adamc@183 436 induction envT; my_crush; eauto.
adamc@183 437 Defined.
adamc@183 438
adamc@183 439 Hint Resolve isfree_one_correct isfree_merge_correct1 isfree_merge_correct2.
adamc@183 440
adamc@183 441 Lemma fvsExp_correct : forall t (e : exp natvar t)
adamc@183 442 envT (fvs : isfree envT), wfExp fvs e
adamc@183 443 -> forall (fvs' : isfree envT),
adamc@183 444 (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs' v t)
adamc@183 445 -> wfExp fvs' e.
adamc@183 446 Hint Extern 1 (_ = _) =>
adamc@183 447 match goal with
adamc@183 448 | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
adamc@183 449 destruct (fvsExp X Y); my_crush
adamc@183 450 end.
adamc@183 451
adamc@183 452 induction e; my_crush; eauto.
adamc@183 453 Defined.
adamc@183 454
adamc@183 455 Lemma lookup_type_unique : forall v t1 t2 envT (fvs1 fvs2 : isfree envT),
adamc@183 456 lookup_type v fvs1 = Some t1
adamc@183 457 -> lookup_type v fvs2 = Some t2
adamc@183 458 -> t1 = t2.
adamc@183 459 induction envT; my_crush; eauto.
adamc@183 460 Defined.
adamc@183 461
adamc@183 462 Implicit Arguments lookup_type_unique [v t1 t2 envT fvs1 fvs2].
adamc@183 463
adamc@183 464 Hint Extern 2 (lookup_type _ _ = Some _) =>
adamc@183 465 match goal with
adamc@183 466 | [ H1 : lookup_type ?v _ = Some _,
adamc@183 467 H2 : lookup_type ?v _ = Some _ |- _ ] =>
adamc@183 468 (generalize (lookup_type_unique H1 H2); intro; subst)
adamc@183 469 || rewrite <- (lookup_type_unique H1 H2)
adamc@183 470 end.
adamc@183 471
adamc@183 472 Lemma lookup_none : forall v t envT,
adamc@183 473 lookup_type (envT:=envT) v (isfree_none (envT:=envT)) = Some t
adamc@183 474 -> False.
adamc@183 475 induction envT; my_crush.
adamc@183 476 Defined.
adamc@183 477
adamc@183 478 Hint Extern 2 (_ = _) => elimtype False; eapply lookup_none; eassumption.
adamc@183 479
adamc@183 480 Lemma lookup_one : forall v' v t envT,
adamc@183 481 lookup_type (envT:=envT) v' (isfree_one (envT:=envT) v) = Some t
adamc@183 482 -> v' = v.
adamc@183 483 induction envT; my_crush.
adamc@183 484 Defined.
adamc@183 485
adamc@183 486 Implicit Arguments lookup_one [v' v t envT].
adamc@183 487
adamc@183 488 Hint Extern 2 (lookup_type _ _ = Some _) =>
adamc@183 489 match goal with
adamc@183 490 | [ H : lookup_type _ _ = Some _ |- _ ] =>
adamc@183 491 generalize (lookup_one H); intro; subst
adamc@183 492 end.
adamc@183 493
adamc@183 494 Lemma lookup_merge : forall v t envT (fvs1 fvs2 : isfree envT),
adamc@183 495 lookup_type v (isfree_merge fvs1 fvs2) = Some t
adamc@183 496 -> lookup_type v fvs1 = Some t
adamc@183 497 \/ lookup_type v fvs2 = Some t.
adamc@183 498 induction envT; my_crush.
adamc@183 499 Defined.
adamc@183 500
adamc@183 501 Implicit Arguments lookup_merge [v t envT fvs1 fvs2].
adamc@183 502
adamc@183 503 Lemma lookup_bound : forall v t envT (fvs : isfree envT),
adamc@183 504 lookup_type v fvs = Some t
adamc@183 505 -> v < length envT.
adamc@183 506 Hint Resolve lt_S.
adamc@183 507 induction envT; my_crush; eauto.
adamc@183 508 Defined.
adamc@183 509
adamc@183 510 Hint Resolve lookup_bound.
adamc@183 511
adamc@183 512 Lemma lookup_bound_contra : forall t envT (fvs : isfree envT),
adamc@183 513 lookup_type (length envT) fvs = Some t
adamc@183 514 -> False.
adamc@187 515 intros; assert (length envT < length envT); eauto; crush.
adamc@183 516 Defined.
adamc@183 517
adamc@183 518 Hint Resolve lookup_bound_contra.
adamc@183 519
adamc@183 520 Lemma lookup_push_drop : forall v t t' envT fvs,
adamc@183 521 v < length envT
adamc@183 522 -> lookup_type (envT := t :: envT) v (true, fvs) = Some t'
adamc@183 523 -> lookup_type (envT := envT) v fvs = Some t'.
adamc@183 524 my_crush.
adamc@183 525 Defined.
adamc@183 526
adamc@183 527 Lemma lookup_push_add : forall v t t' envT fvs,
adamc@183 528 lookup_type (envT := envT) v (snd fvs) = Some t'
adamc@183 529 -> lookup_type (envT := t :: envT) v fvs = Some t'.
adamc@183 530 my_crush; elimtype False; eauto.
adamc@183 531 Defined.
adamc@183 532
adamc@183 533 Hint Resolve lookup_bound lookup_push_drop lookup_push_add.
adamc@183 534
adamc@183 535 Theorem fvsExp_minimal : forall t (e : exp natvar t)
adamc@183 536 envT (fvs : isfree envT), wfExp fvs e
adamc@183 537 -> (forall v t, ok envT (fvsExp e envT) v t -> ok envT fvs v t).
adamc@183 538 Hint Extern 1 (_ = _) =>
adamc@183 539 match goal with
adamc@183 540 | [ H : lookup_type _ (isfree_merge _ _) = Some _ |- _ ] =>
adamc@183 541 destruct (lookup_merge H); clear H; eauto
adamc@183 542 end.
adamc@183 543
adamc@183 544 induction e; my_crush; eauto.
adamc@183 545 Defined.
adamc@183 546
adamc@183 547 Fixpoint ccType (t : Source.type) : Closed.type :=
adamc@183 548 match t with
adamc@183 549 | Nat%source => Nat
adamc@183 550 | (dom --> ran)%source => ccType dom --> ccType ran
adamc@183 551 end%cc.
adamc@183 552
adamc@183 553 Open Local Scope cc_scope.
adamc@183 554
adamc@183 555 Fixpoint envType (envT : list Source.type) : isfree envT -> Closed.type :=
adamc@183 556 match envT return (isfree envT -> _) with
adamc@183 557 | nil => fun _ => Unit
adamc@183 558 | t :: _ => fun tup =>
adamc@183 559 if fst tup
adamc@183 560 then ccType t ** envType _ (snd tup)
adamc@183 561 else envType _ (snd tup)
adamc@183 562 end.
adamc@183 563
adamc@183 564 Implicit Arguments envType [envT].
adamc@183 565
adamc@183 566 Fixpoint envOf (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
adamc@183 567 : isfree envT -> Set :=
adamc@183 568 match envT return (isfree envT -> _) with
adamc@183 569 | nil => fun _ => unit
adamc@183 570 | first :: rest => fun fvs =>
adamc@183 571 match fvs with
adamc@183 572 | (true, fvs') => (var (ccType first) * envOf var rest fvs')%type
adamc@183 573 | (false, fvs') => envOf var rest fvs'
adamc@183 574 end
adamc@183 575 end.
adamc@183 576
adamc@183 577 Implicit Arguments envOf [envT].
adamc@183 578
adamc@183 579 Notation "var <| to" := (match to with
adamc@183 580 | None => unit
adamc@183 581 | Some t => var (ccType t)
adamc@183 582 end) (no associativity, at level 70).
adamc@183 583
adamc@183 584 Fixpoint lookup (var : Closed.type -> Set) (envT : list Source.type) :
adamc@183 585 forall (n : nat) (fvs : isfree envT), envOf var fvs -> var <| lookup_type n fvs :=
adamc@183 586 match envT return (forall (n : nat) (fvs : isfree envT), envOf var fvs
adamc@183 587 -> var <| lookup_type n fvs) with
adamc@183 588 | nil => fun _ _ _ => tt
adamc@183 589 | first :: rest => fun n fvs =>
adamc@183 590 match (eq_nat_dec n (length rest)) as Heq return
adamc@183 591 (envOf var (envT := first :: rest) fvs
adamc@183 592 -> var <| (if Heq
adamc@183 593 then match fvs with
adamc@183 594 | (true, _) => Some first
adamc@183 595 | (false, _) => None
adamc@183 596 end
adamc@183 597 else lookup_type n (snd fvs))) with
adamc@183 598 | left _ =>
adamc@183 599 match fvs return (envOf var (envT := first :: rest) fvs
adamc@183 600 -> var <| (match fvs with
adamc@183 601 | (true, _) => Some first
adamc@183 602 | (false, _) => None
adamc@183 603 end)) with
adamc@183 604 | (true, _) => fun env => fst env
adamc@183 605 | (false, _) => fun _ => tt
adamc@183 606 end
adamc@183 607 | right _ =>
adamc@183 608 match fvs return (envOf var (envT := first :: rest) fvs
adamc@183 609 -> var <| (lookup_type n (snd fvs))) with
adamc@183 610 | (true, fvs') => fun env => lookup var rest n fvs' (snd env)
adamc@183 611 | (false, fvs') => fun env => lookup var rest n fvs' env
adamc@183 612 end
adamc@183 613 end
adamc@183 614 end.
adamc@183 615
adamc@183 616 Theorem lok : forall var n t envT (fvs : isfree envT),
adamc@183 617 lookup_type n fvs = Some t
adamc@183 618 -> var <| lookup_type n fvs = var (ccType t).
adamc@183 619 crush.
adamc@183 620 Defined.
adamc@183 621 End isfree.
adamc@183 622
adamc@183 623 Implicit Arguments lookup_type [envT].
adamc@183 624 Implicit Arguments lookup [envT fvs].
adamc@183 625 Implicit Arguments wfExp [t envT].
adamc@183 626 Implicit Arguments envType [envT].
adamc@183 627 Implicit Arguments envOf [envT].
adamc@183 628 Implicit Arguments lok [var n t envT fvs].
adamc@183 629
adamc@183 630 Section lookup_hints.
adamc@183 631 Hint Resolve lookup_bound_contra.
adamc@183 632
adamc@183 633 Hint Resolve lookup_bound_contra.
adamc@183 634
adamc@183 635 Lemma lookup_type_push : forall t' envT (fvs1 fvs2 : isfree envT) b1 b2,
adamc@183 636 (forall (n : nat) (t : Source.type),
adamc@183 637 lookup_type (envT := t' :: envT) n (b1, fvs1) = Some t ->
adamc@183 638 lookup_type (envT := t' :: envT) n (b2, fvs2) = Some t)
adamc@183 639 -> (forall (n : nat) (t : Source.type),
adamc@183 640 lookup_type n fvs1 = Some t ->
adamc@183 641 lookup_type n fvs2 = Some t).
adamc@183 642 intros until b2; intro H; intros n t;
adamc@183 643 generalize (H n t); my_crush; elimtype False; eauto.
adamc@183 644 Defined.
adamc@183 645
adamc@183 646 Lemma lookup_type_push_contra : forall t' envT (fvs1 fvs2 : isfree envT),
adamc@183 647 (forall (n : nat) (t : Source.type),
adamc@183 648 lookup_type (envT := t' :: envT) n (true, fvs1) = Some t ->
adamc@183 649 lookup_type (envT := t' :: envT) n (false, fvs2) = Some t)
adamc@183 650 -> False.
adamc@183 651 intros until fvs2; intro H; generalize (H (length envT) t'); my_crush.
adamc@183 652 Defined.
adamc@183 653 End lookup_hints.
adamc@183 654
adamc@183 655 Section packing.
adamc@183 656 Open Local Scope cc_scope.
adamc@183 657
adamc@183 658 Hint Resolve lookup_type_push lookup_type_push_contra.
adamc@183 659
adamc@183 660 Definition packExp (var : Closed.type -> Set) (envT : list Source.type)
adamc@183 661 (fvs1 fvs2 : isfree envT)
adamc@183 662 : (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
adamc@183 663 -> envOf var fvs2 -> exp var (envType fvs1).
adamc@183 664 refine (fix packExp (var : Closed.type -> Set) (envT : list Source.type) {struct envT}
adamc@183 665 : forall fvs1 fvs2 : isfree envT,
adamc@183 666 (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
adamc@183 667 -> envOf var fvs2 -> exp var (envType fvs1) :=
adamc@183 668 match envT return (forall fvs1 fvs2 : isfree envT,
adamc@183 669 (forall n t, lookup_type n fvs1 = Some t -> lookup_type n fvs2 = Some t)
adamc@183 670 -> envOf var fvs2
adamc@183 671 -> exp var (envType fvs1)) with
adamc@183 672 | nil => fun _ _ _ _ => ()
adamc@183 673 | first :: rest => fun fvs1 =>
adamc@183 674 match fvs1 return (forall fvs2 : isfree (first :: rest),
adamc@183 675 (forall n t, lookup_type (envT := first :: rest) n fvs1 = Some t
adamc@183 676 -> lookup_type n fvs2 = Some t)
adamc@183 677 -> envOf var fvs2
adamc@183 678 -> exp var (envType (envT := first :: rest) fvs1)) with
adamc@183 679 | (false, fvs1') => fun fvs2 =>
adamc@183 680 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (false, fvs1') = Some t
adamc@183 681 -> lookup_type (envT := first :: rest) n fvs2 = Some t)
adamc@183 682 -> envOf (envT := first :: rest) var fvs2
adamc@183 683 -> exp var (envType (envT := first :: rest) (false, fvs1'))) with
adamc@183 684 | (false, fvs2') => fun Hmin env =>
adamc@183 685 packExp var _ fvs1' fvs2' _ env
adamc@183 686 | (true, fvs2') => fun Hmin env =>
adamc@183 687 packExp var _ fvs1' fvs2' _ (snd env)
adamc@183 688 end
adamc@183 689 | (true, fvs1') => fun fvs2 =>
adamc@183 690 match fvs2 return ((forall n t, lookup_type (envT := first :: rest) n (true, fvs1') = Some t
adamc@183 691 -> lookup_type (envT := first :: rest) n fvs2 = Some t)
adamc@183 692 -> envOf (envT := first :: rest) var fvs2
adamc@183 693 -> exp var (envType (envT := first :: rest) (true, fvs1'))) with
adamc@183 694 | (false, fvs2') => fun Hmin env =>
adamc@183 695 False_rect _ _
adamc@183 696 | (true, fvs2') => fun Hmin env =>
adamc@183 697 [#(fst env), packExp var _ fvs1' fvs2' _ (snd env)]
adamc@183 698 end
adamc@183 699 end
adamc@183 700 end); eauto.
adamc@183 701 Defined.
adamc@183 702
adamc@183 703 Hint Resolve fvsExp_correct fvsExp_minimal.
adamc@183 704 Hint Resolve lookup_push_drop lookup_bound lookup_push_add.
adamc@183 705
adamc@183 706 Implicit Arguments packExp [var envT].
adamc@183 707
adamc@183 708 Fixpoint unpackExp (var : Closed.type -> Set) t (envT : list Source.type) {struct envT}
adamc@183 709 : forall fvs : isfree envT,
adamc@183 710 exp var (envType fvs)
adamc@183 711 -> (envOf var fvs -> exp var t) -> exp var t :=
adamc@183 712 match envT return (forall fvs : isfree envT,
adamc@183 713 exp var (envType fvs)
adamc@183 714 -> (envOf var fvs -> exp var t) -> exp var t) with
adamc@183 715 | nil => fun _ _ f => f tt
adamc@183 716 | first :: rest => fun fvs =>
adamc@183 717 match fvs return (exp var (envType (envT := first :: rest) fvs)
adamc@183 718 -> (envOf var (envT := first :: rest) fvs -> exp var t)
adamc@183 719 -> exp var t) with
adamc@183 720 | (false, fvs') => fun p f =>
adamc@183 721 unpackExp rest fvs' p f
adamc@183 722 | (true, fvs') => fun p f =>
adamc@183 723 x <- #1 p;
adamc@183 724 unpackExp rest fvs' (#2 p)
adamc@183 725 (fun env => f (x, env))
adamc@183 726 end
adamc@183 727 end.
adamc@183 728
adamc@183 729 Implicit Arguments unpackExp [var t envT fvs].
adamc@183 730
adamc@183 731 Theorem wfExp_lax : forall t t' envT (fvs : isfree envT) (e : Source.exp natvar t),
adamc@183 732 wfExp (envT := t' :: envT) (true, fvs) e
adamc@183 733 -> wfExp (envT := t' :: envT) (true, snd (fvsExp e (t' :: envT))) e.
adamc@183 734 Hint Extern 1 (_ = _) =>
adamc@183 735 match goal with
adamc@183 736 | [ H : lookup_type _ (fvsExp ?X ?Y) = _ |- _ ] =>
adamc@183 737 destruct (fvsExp X Y); my_crush
adamc@183 738 end.
adamc@183 739 eauto.
adamc@183 740 Defined.
adamc@183 741
adamc@183 742 Implicit Arguments wfExp_lax [t t' envT fvs e].
adamc@183 743
adamc@183 744 Lemma inclusion : forall t t' envT fvs (e : Source.exp natvar t),
adamc@183 745 wfExp (envT := t' :: envT) (true, fvs) e
adamc@183 746 -> (forall n t, lookup_type n (snd (fvsExp e (t' :: envT))) = Some t
adamc@183 747 -> lookup_type n fvs = Some t).
adamc@183 748 eauto.
adamc@183 749 Defined.
adamc@183 750
adamc@183 751 Implicit Arguments inclusion [t t' envT fvs e].
adamc@183 752
adamc@183 753 Definition env_prog var t envT (fvs : isfree envT) :=
adamc@183 754 funcs var (envOf var fvs -> Closed.exp var t).
adamc@183 755
adamc@183 756 Implicit Arguments env_prog [envT].
adamc@183 757
adamc@183 758 Import Source.
adamc@183 759 Open Local Scope cc_scope.
adamc@183 760
adamc@187 761 Definition proj1 A B (pf : A /\ B) : A :=
adamc@187 762 let (x, _) := pf in x.
adamc@187 763 Definition proj2 A B (pf : A /\ B) : B :=
adamc@187 764 let (_, y) := pf in y.
adamc@187 765
adamc@183 766 Fixpoint ccExp var t (e : Source.exp natvar t)
adamc@183 767 (envT : list Source.type) (fvs : isfree envT)
adamc@183 768 {struct e} : wfExp fvs e -> env_prog var (ccType t) fvs :=
adamc@183 769 match e in (Source.exp _ t) return (wfExp fvs e -> env_prog var (ccType t) fvs) with
adamc@183 770 | Const n => fun _ => Main (fun _ => ^n)
adamc@183 771 | Plus e1 e2 => fun wf =>
adamc@183 772 n1 <-- ccExp var e1 _ fvs (proj1 wf);
adamc@183 773 n2 <-- ccExp var e2 _ fvs (proj2 wf);
adamc@183 774 Main (fun env => n1 env +^ n2 env)
adamc@183 775
adamc@183 776 | Var _ n => fun wf =>
adamc@183 777 Main (fun env => #(match lok wf in _ = T return T with
adamc@183 778 | refl_equal => lookup var n env
adamc@183 779 end))
adamc@183 780
adamc@183 781 | App _ _ f x => fun wf =>
adamc@183 782 f' <-- ccExp var f _ fvs (proj1 wf);
adamc@183 783 x' <-- ccExp var x _ fvs (proj2 wf);
adamc@183 784 Main (fun env => f' env @ x' env)
adamc@183 785
adamc@183 786 | Abs dom _ b => fun wf =>
adamc@183 787 b' <-- ccExp var (b (length envT)) (dom :: envT) _ (wfExp_lax wf);
adamc@183 788 f <== \\env, arg, unpackExp (#env) (fun env => b' (arg, env));
adamc@183 789 Main (fun env => #f ##
adamc@183 790 packExp
adamc@183 791 (snd (fvsExp (b (length envT)) (dom :: envT)))
adamc@183 792 fvs (inclusion wf) env)
adamc@183 793 end.
adamc@183 794 End packing.
adamc@183 795
adamc@183 796 Implicit Arguments packExp [var envT].
adamc@183 797 Implicit Arguments unpackExp [var t envT fvs].
adamc@183 798
adamc@183 799 Implicit Arguments ccExp [var t envT].
adamc@183 800
adamc@184 801 Fixpoint map_funcs var T1 T2 (f : T1 -> T2) (fs : funcs var T1) {struct fs}
adamc@184 802 : funcs var T2 :=
adamc@183 803 match fs with
adamc@184 804 | Main v => Main (f v)
adamc@184 805 | Abs _ _ _ e fs' => Abs e (fun x => map_funcs f (fs' x))
adamc@183 806 end.
adamc@183 807
adamc@186 808 Definition CcExp' t (E : Source.Exp t) (Hwf : wfExp (envT := nil) tt (E _)) : Prog (ccType t) :=
adamc@184 809 fun _ => map_funcs (fun f => f tt) (ccExp (E _) (envT := nil) tt Hwf).
adamc@183 810
adamc@183 811
adamc@187 812 (** ** Examples *)
adamc@187 813
adamc@187 814 Open Local Scope source_scope.
adamc@187 815
adamc@187 816 Definition ident : Source.Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@187 817 Theorem ident_ok : wfExp (envT := nil) tt (ident _).
adamc@187 818 crush.
adamc@187 819 Defined.
adamc@187 820 Eval compute in CcExp' ident ident_ok.
adamc@187 821 Eval compute in ProgDenote (CcExp' ident ident_ok).
adamc@187 822
adamc@187 823 Definition app_ident : Source.Exp Nat := fun _ => ident _ @ ^0.
adamc@187 824 Theorem app_ident_ok : wfExp (envT := nil) tt (app_ident _).
adamc@187 825 crush.
adamc@187 826 Defined.
adamc@187 827 Eval compute in CcExp' app_ident app_ident_ok.
adamc@187 828 Eval compute in ProgDenote (CcExp' app_ident app_ident_ok).
adamc@187 829
adamc@187 830 Definition first : Source.Exp (Nat --> Nat --> Nat) := fun _ =>
adamc@187 831 \x, \y, #x.
adamc@187 832 Theorem first_ok : wfExp (envT := nil) tt (first _).
adamc@187 833 crush.
adamc@187 834 Defined.
adamc@187 835 Eval compute in CcExp' first first_ok.
adamc@187 836 Eval compute in ProgDenote (CcExp' first first_ok).
adamc@187 837
adamc@187 838 Definition app_first : Source.Exp Nat := fun _ => first _ @ ^1 @ ^0.
adamc@187 839 Theorem app_first_ok : wfExp (envT := nil) tt (app_first _).
adamc@187 840 crush.
adamc@187 841 Defined.
adamc@187 842 Eval compute in CcExp' app_first app_first_ok.
adamc@187 843 Eval compute in ProgDenote (CcExp' app_first app_first_ok).
adamc@187 844
adamc@187 845
adamc@187 846 (** ** Correctness *)
adamc@183 847
adamc@184 848 Section spliceFuncs_correct.
adamc@184 849 Variables T1 T2 : Type.
adamc@184 850 Variable f : T1 -> funcs typeDenote T2.
adamc@183 851
adamc@184 852 Theorem spliceFuncs_correct : forall fs,
adamc@184 853 funcsDenote (spliceFuncs fs f)
adamc@184 854 = funcsDenote (f (funcsDenote fs)).
adamc@184 855 induction fs; crush.
adamc@183 856 Qed.
adamc@183 857 End spliceFuncs_correct.
adamc@183 858
adamc@183 859
adamc@185 860 Notation "var <| to" := (match to return Set with
adamc@183 861 | None => unit
adamc@184 862 | Some t => var (ccType t)
adamc@183 863 end) (no associativity, at level 70).
adamc@183 864
adamc@183 865 Section packing_correct.
adamc@184 866 Fixpoint makeEnv (envT : list Source.type) : forall (fvs : isfree envT),
adamc@184 867 Closed.typeDenote (envType fvs)
adamc@184 868 -> envOf Closed.typeDenote fvs :=
adamc@183 869 match envT return (forall (fvs : isfree envT),
adamc@184 870 Closed.typeDenote (envType fvs)
adamc@184 871 -> envOf Closed.typeDenote fvs) with
adamc@183 872 | nil => fun _ _ => tt
adamc@183 873 | first :: rest => fun fvs =>
adamc@184 874 match fvs return (Closed.typeDenote (envType (envT := first :: rest) fvs)
adamc@184 875 -> envOf (envT := first :: rest) Closed.typeDenote fvs) with
adamc@183 876 | (false, fvs') => fun env => makeEnv rest fvs' env
adamc@183 877 | (true, fvs') => fun env => (fst env, makeEnv rest fvs' (snd env))
adamc@183 878 end
adamc@183 879 end.
adamc@183 880
adamc@184 881 Implicit Arguments makeEnv [envT fvs].
adamc@184 882
adamc@184 883 Theorem unpackExp_correct : forall t (envT : list Source.type) (fvs : isfree envT)
adamc@184 884 (e1 : Closed.exp Closed.typeDenote (envType fvs))
adamc@184 885 (e2 : envOf Closed.typeDenote fvs -> Closed.exp Closed.typeDenote t),
adamc@184 886 Closed.expDenote (unpackExp e1 e2)
adamc@184 887 = Closed.expDenote (e2 (makeEnv (Closed.expDenote e1))).
adamc@184 888 induction envT; my_crush.
adamc@183 889 Qed.
adamc@183 890
adamc@183 891 Lemma lookup_type_more : forall v2 envT (fvs : isfree envT) t b v,
adamc@183 892 (v2 = length envT -> False)
adamc@183 893 -> lookup_type v2 (envT := t :: envT) (b, fvs) = v
adamc@183 894 -> lookup_type v2 fvs = v.
adamc@184 895 my_crush.
adamc@183 896 Qed.
adamc@183 897
adamc@183 898 Lemma lookup_type_less : forall v2 t envT (fvs : isfree (t :: envT)) v,
adamc@183 899 (v2 = length envT -> False)
adamc@183 900 -> lookup_type v2 (snd fvs) = v
adamc@183 901 -> lookup_type v2 (envT := t :: envT) fvs = v.
adamc@184 902 my_crush.
adamc@183 903 Qed.
adamc@183 904
adamc@184 905 Hint Resolve lookup_bound_contra.
adamc@184 906
adamc@183 907 Lemma lookup_bound_contra_eq : forall t envT (fvs : isfree envT) v,
adamc@183 908 lookup_type v fvs = Some t
adamc@183 909 -> v = length envT
adamc@183 910 -> False.
adamc@184 911 my_crush; elimtype False; eauto.
adamc@184 912 Qed.
adamc@183 913
adamc@184 914 Lemma lookup_type_inner : forall t t' envT v t'' (fvs : isfree envT) e,
adamc@184 915 wfExp (envT := t' :: envT) (true, fvs) e
adamc@184 916 -> lookup_type v (snd (fvsExp (t := t) e (t' :: envT))) = Some t''
adamc@184 917 -> lookup_type v fvs = Some t''.
adamc@184 918 Hint Resolve lookup_bound_contra_eq fvsExp_minimal
adamc@183 919 lookup_type_more lookup_type_less.
adamc@184 920 Hint Extern 2 (Some _ = Some _) => elimtype False.
adamc@183 921
adamc@183 922 eauto 6.
adamc@183 923 Qed.
adamc@183 924
adamc@183 925 Lemma cast_irrel : forall T1 T2 x (H1 H2 : T1 = T2),
adamc@184 926 match H1 in _ = T return T with
adamc@184 927 | refl_equal => x
adamc@184 928 end
adamc@184 929 = match H2 in _ = T return T with
adamc@184 930 | refl_equal => x
adamc@184 931 end.
adamc@184 932 intros; generalize H1; crush;
adamc@184 933 repeat match goal with
adamc@184 934 | [ |- context[match ?pf with refl_equal => _ end] ] =>
adamc@184 935 rewrite (UIP_refl _ _ pf)
adamc@184 936 end;
adamc@184 937 reflexivity.
adamc@183 938 Qed.
adamc@183 939
adamc@183 940 Hint Immediate cast_irrel.
adamc@183 941
adamc@184 942 Hint Extern 3 (_ == _) =>
adamc@183 943 match goal with
adamc@183 944 | [ |- context[False_rect _ ?H] ] =>
adamc@183 945 apply False_rect; exact H
adamc@183 946 end.
adamc@183 947
adamc@187 948 Theorem packExp_correct : forall v t envT (fvs1 fvs2 : isfree envT)
adamc@183 949 Hincl env,
adamc@187 950 lookup_type v fvs1 = Some t
adamc@184 951 -> lookup Closed.typeDenote v env
adamc@184 952 == lookup Closed.typeDenote v
adamc@184 953 (makeEnv (Closed.expDenote
adamc@184 954 (packExp fvs1 fvs2 Hincl env))).
adamc@184 955 induction envT; my_crush.
adamc@183 956 Qed.
adamc@183 957 End packing_correct.
adamc@183 958
adamc@185 959 Implicit Arguments packExp_correct [v envT fvs1].
adamc@187 960 Implicit Arguments lookup_type_inner [t t' envT v t'' fvs e].
adamc@187 961 Implicit Arguments inclusion [t t' envT fvs e].
adamc@184 962
adamc@184 963 Lemma typeDenote_same : forall t,
adamc@184 964 Source.typeDenote t = Closed.typeDenote (ccType t).
adamc@184 965 induction t; crush.
adamc@184 966 Qed.
adamc@184 967
adamc@184 968 Hint Resolve typeDenote_same.
adamc@184 969
adamc@185 970 Fixpoint lr (t : Source.type) : Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop :=
adamc@185 971 match t return Source.typeDenote t -> Closed.typeDenote (ccType t) -> Prop with
adamc@185 972 | Nat => @eq nat
adamc@185 973 | dom --> ran => fun f1 f2 =>
adamc@185 974 forall x1 x2, lr dom x1 x2
adamc@185 975 -> lr ran (f1 x1) (f2 x2)
adamc@185 976 end.
adamc@184 977
adamc@186 978 Theorem ccExp_correct : forall t G
adamc@184 979 (e1 : Source.exp Source.typeDenote t)
adamc@184 980 (e2 : Source.exp natvar t),
adamc@184 981 exp_equiv G e1 e2
adamc@184 982 -> forall (envT : list Source.type) (fvs : isfree envT)
adamc@184 983 (env : envOf Closed.typeDenote fvs) (wf : wfExp fvs e2),
adamc@184 984 (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
adamc@184 985 In (existT _ _ (v1, v2)) G
adamc@183 986 -> v2 < length envT)
adamc@184 987 -> (forall t (v1 : Source.typeDenote t) (v2 : natvar t),
adamc@184 988 In (existT _ _ (v1, v2)) G
adamc@185 989 -> forall pf,
adamc@185 990 lr t v1 (match lok pf in _ = T return T with
adamc@185 991 | refl_equal => lookup Closed.typeDenote v2 env
adamc@185 992 end))
adamc@185 993 -> lr t (Source.expDenote e1) (Closed.expDenote (funcsDenote (ccExp e2 fvs wf) env)).
adamc@183 994
adamc@184 995 Hint Rewrite spliceFuncs_correct unpackExp_correct : cpdt.
adamc@183 996 Hint Resolve packExp_correct lookup_type_inner.
adamc@183 997
adamc@188 998 induction 1; crush;
adamc@188 999 match goal with
adamc@188 1000 | [ IH : _, Hlr : lr ?T ?X1 ?X2, ENV : list Source.type, F2 : natvar _ -> _ |- _ ] =>
adamc@188 1001 apply (IH X1 (length ENV) (T :: ENV) (true, snd (fvsExp (F2 (length ENV)) (T :: ENV))))
adamc@188 1002 end; crush;
adamc@188 1003 match goal with
adamc@188 1004 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In _ _ |- _ ] =>
adamc@188 1005 solve [ generalize (Hlt _ _ _ Hin); crush ]
adamc@188 1006 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
adamc@188 1007 end; simpl;
adamc@188 1008 match goal with
adamc@188 1009 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@188 1010 end; intuition; subst;
adamc@188 1011 match goal with
adamc@188 1012 | [ |- context[match ?pf with refl_equal => _ end] ] => rewrite (UIP_refl _ _ pf); assumption
adamc@188 1013 | [ Hlt : forall t v1 v2, _ -> _ < _, Hin : In (existT _ _ (_, length _)) _ |- _ ] =>
adamc@188 1014 generalize (Hlt _ _ _ Hin); crush
adamc@188 1015 | [ HG : _, Hin : In _ _, wf : wfExp _ _, pf : _ = Some _,
adamc@188 1016 fvs : isfree _, env : envOf _ _ |- _ ] =>
adamc@188 1017 generalize (HG _ _ _ Hin (lookup_type_inner wf pf)); clear_all;
adamc@188 1018 repeat match goal with
adamc@188 1019 | [ |- context[match ?pf with refl_equal => _ end] ] => generalize pf
adamc@188 1020 end; simpl;
adamc@188 1021 generalize (packExp_correct _ fvs (inclusion wf) env pf); simpl;
adamc@188 1022 match goal with
adamc@188 1023 | [ |- ?X == ?Y -> _ ] =>
adamc@188 1024 generalize X Y
adamc@188 1025 end;
adamc@188 1026 rewrite pf; rewrite (lookup_type_inner wf pf);
adamc@188 1027 intros lhs rhs Heq; intros;
adamc@188 1028 repeat match goal with
adamc@188 1029 | [ H : _ = _ |- _ ] => rewrite (UIP_refl _ _ H) in *
adamc@188 1030 end;
adamc@188 1031 rewrite <- Heq; assumption
adamc@188 1032 end.
adamc@183 1033 Qed.
adamc@183 1034
adamc@183 1035
adamc@183 1036 (** * Parametric version *)
adamc@183 1037
adamc@183 1038 Section wf.
adamc@186 1039 Lemma Exp_wf' : forall G t (e1 e2 : Source.exp natvar t),
adamc@186 1040 exp_equiv G e1 e2
adamc@186 1041 -> forall envT (fvs : isfree envT),
adamc@186 1042 (forall t (v1 v2 : natvar t), In (existT _ _ (v1, v2)) G
adamc@186 1043 -> lookup_type v1 fvs = Some t)
adamc@186 1044 -> wfExp fvs e1.
adamc@186 1045 Hint Extern 3 (Some _ = Some _) => elimtype False; eapply lookup_bound_contra; eauto.
adamc@183 1046
adamc@186 1047 induction 1; crush.
adamc@186 1048 eapply H0.
adamc@186 1049 eauto.
adamc@183 1050
adamc@186 1051 apply H0 with (length envT).
adamc@186 1052 my_crush.
adamc@186 1053 eauto.
adamc@183 1054 Qed.
adamc@183 1055
adamc@186 1056 Theorem Exp_wf : forall t (E : Source.Exp t),
adamc@186 1057 wfExp (envT := nil) tt (E _).
adamc@186 1058 intros; eapply Exp_wf';
adamc@186 1059 [apply Exp_equiv
adamc@186 1060 | crush].
adamc@183 1061 Qed.
adamc@183 1062 End wf.
adamc@183 1063
adamc@186 1064 Definition CcExp t (E : Source.Exp t) : Prog (ccType t) :=
adamc@186 1065 CcExp' E (Exp_wf E).
adamc@183 1066
adamc@186 1067 Lemma map_funcs_correct : forall T1 T2 (f : T1 -> T2) (fs : funcs Closed.typeDenote T1),
adamc@186 1068 funcsDenote (map_funcs f fs) = f (funcsDenote fs).
adamc@186 1069 induction fs; crush.
adamc@183 1070 Qed.
adamc@183 1071
adamc@186 1072 Theorem CcExp_correct : forall (E : Source.Exp Nat),
adamc@186 1073 Source.ExpDenote E
adamc@186 1074 = ProgDenote (CcExp E).
adamc@186 1075 Hint Rewrite map_funcs_correct : cpdt.
adamc@183 1076
adamc@186 1077 unfold Source.ExpDenote, ProgDenote, CcExp, CcExp', progDenote; crush;
adamc@186 1078 apply (ccExp_correct
adamc@183 1079 (G := nil)
adamc@183 1080 (e1 := E _)
adamc@183 1081 (e2 := E _)
adamc@186 1082 (Exp_equiv _ _ _)
adamc@183 1083 nil
adamc@183 1084 tt
adamc@186 1085 tt); crush.
adamc@183 1086 Qed.