Mercurial > cpdt > repo

annotate src/Hoas.v @ 163:ba306bf9ec80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Feeling stuck with Hoas
author Adam Chlipala <adamc@hcoop.net>
date Tue, 04 Nov 2008 16:45:50 -0500
parents df02642f93b8
children 391ccedd0568
rev   line source
adamc@158 1 (* Copyright (c) 2008, Adam Chlipala
adamc@158 2 *
adamc@158 3 * This work is licensed under a
adamc@158 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@158 5 * Unported License.
adamc@158 6 * The license text is available at:
adamc@158 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@158 8 *)
adamc@158 9
adamc@158 10 (* begin hide *)
adamc@158 11 Require Import Arith Eqdep String List.
adamc@158 12
adamc@160 13 Require Import Axioms DepList Tactics.
adamc@158 14
adamc@158 15 Set Implicit Arguments.
adamc@158 16 (* end hide *)
adamc@158 17
adamc@158 18
adamc@158 19 (** %\chapter{Higher-Order Abstract Syntax}% *)
adamc@158 20
adamc@158 21 (** TODO: Prose for this chapter *)
adamc@158 22
adamc@158 23
adamc@158 24 (** * Parametric Higher-Order Abstract Syntax *)
adamc@158 25
adamc@158 26 Inductive type : Type :=
adamc@159 27 | Nat : type
adamc@158 28 | Arrow : type -> type -> type.
adamc@158 29
adamc@158 30 Infix "-->" := Arrow (right associativity, at level 60).
adamc@158 31
adamc@158 32 Section exp.
adamc@158 33 Variable var : type -> Type.
adamc@158 34
adamc@158 35 Inductive exp : type -> Type :=
adamc@159 36 | Const' : nat -> exp Nat
adamc@159 37 | Plus' : exp Nat -> exp Nat -> exp Nat
adamc@159 38
adamc@158 39 | Var : forall t, var t -> exp t
adamc@158 40 | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran
adamc@158 41 | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran).
adamc@158 42 End exp.
adamc@158 43
adamc@158 44 Implicit Arguments Const' [var].
adamc@158 45 Implicit Arguments Var [var t].
adamc@158 46 Implicit Arguments Abs' [var dom ran].
adamc@158 47
adamc@158 48 Definition Exp t := forall var, exp var t.
adamc@158 49 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
adamc@158 50
adamc@159 51 Definition Const (n : nat) : Exp Nat :=
adamc@159 52 fun _ => Const' n.
adamc@159 53 Definition Plus (E1 E2 : Exp Nat) : Exp Nat :=
adamc@159 54 fun _ => Plus' (E1 _) (E2 _).
adamc@158 55 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
adamc@158 56 fun _ => App' (F _) (X _).
adamc@158 57 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
adamc@158 58 fun _ => Abs' (B _).
adamc@158 59
adamc@158 60 Section flatten.
adamc@158 61 Variable var : type -> Type.
adamc@158 62
adamc@158 63 Fixpoint flatten t (e : exp (exp var) t) {struct e} : exp var t :=
adamc@158 64 match e in exp _ t return exp _ t with
adamc@159 65 | Const' n => Const' n
adamc@159 66 | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
adamc@158 67 | Var _ e' => e'
adamc@158 68 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
adamc@158 69 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
adamc@158 70 end.
adamc@158 71 End flatten.
adamc@158 72
adamc@158 73 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
adamc@158 74 flatten (E2 _ (E1 _)).
adamc@158 75
adamc@158 76
adamc@158 77 (** * A Type Soundness Proof *)
adamc@158 78
adamc@158 79 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
adamc@158 80
adamc@158 81 Inductive Val : forall t, Exp t -> Prop :=
adamc@159 82 | VConst : forall n, Val (Const n)
adamc@158 83 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
adamc@158 84
adamc@158 85 Hint Constructors Val.
adamc@158 86
adamc@162 87 Inductive Ctx : type -> type -> Type :=
adamc@162 88 | AppCong1 : forall (dom ran : type),
adamc@162 89 Exp dom -> Ctx (dom --> ran) ran
adamc@162 90 | AppCong2 : forall (dom ran : type),
adamc@162 91 Exp (dom --> ran) -> Ctx dom ran
adamc@162 92 | PlusCong1 : Exp Nat -> Ctx Nat Nat
adamc@162 93 | PlusCong2 : Exp Nat -> Ctx Nat Nat.
adamc@162 94
adamc@162 95 Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop :=
adamc@162 96 | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X)
adamc@162 97 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F)
adamc@162 98 | IsPlus1 : forall E2, isCtx (PlusCong1 E2)
adamc@162 99 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).
adamc@162 100
adamc@162 101 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
adamc@162 102 match C in Ctx t1 t2 return Exp t1 -> Exp t2 with
adamc@162 103 | AppCong1 _ _ X => fun F => App F X
adamc@162 104 | AppCong2 _ _ F => fun X => App F X
adamc@162 105 | PlusCong1 E2 => fun E1 => Plus E1 E2
adamc@162 106 | PlusCong2 E1 => fun E2 => Plus E1 E2
adamc@162 107 end.
adamc@162 108
adamc@162 109 Infix "@" := plug (no associativity, at level 60).
adamc@162 110
adamc@158 111 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
adamc@158 112 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
adamc@160 113 Val X
adamc@160 114 -> App (Abs B) X ==> Subst X B
adamc@159 115 | Sum : forall n1 n2,
adamc@159 116 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
adamc@162 117 | Cong : forall t t' (C : Ctx t t') E E' E1,
adamc@162 118 isCtx C
adamc@162 119 -> E1 = C @ E
adamc@162 120 -> E ==> E'
adamc@162 121 -> E1 ==> C @ E'
adamc@159 122
adamc@158 123 where "E1 ==> E2" := (Step E1 E2).
adamc@158 124
adamc@162 125 Hint Constructors isCtx Step.
adamc@158 126
adamc@158 127 Inductive Closed : forall t, Exp t -> Prop :=
adamc@158 128 | CConst : forall b,
adamc@158 129 Closed (Const b)
adamc@159 130 | CPlus : forall E1 E2,
adamc@159 131 Closed E1
adamc@159 132 -> Closed E2
adamc@159 133 -> Closed (Plus E1 E2)
adamc@158 134 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
adamc@158 135 Closed E1
adamc@158 136 -> Closed E2
adamc@158 137 -> Closed (App E1 E2)
adamc@158 138 | CAbs : forall dom ran (E1 : Exp1 dom ran),
adamc@158 139 Closed (Abs E1).
adamc@158 140
adamc@158 141 Axiom closed : forall t (E : Exp t), Closed E.
adamc@158 142
adamc@163 143 Ltac my_subst :=
adamc@163 144 repeat match goal with
adamc@163 145 | [ x : type |- _ ] => subst x
adamc@163 146 end.
adamc@163 147
adamc@160 148 Ltac my_crush' :=
adamc@163 149 crush; my_subst;
adamc@158 150 repeat (match goal with
adamc@158 151 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
adamc@163 152 end; crush; my_subst).
adamc@163 153
adamc@163 154 Ltac equate_conj F G :=
adamc@163 155 match constr:(F, G) with
adamc@163 156 | (_ ?x1, _ ?x2) => constr:(x1 = x2)
adamc@163 157 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
adamc@163 158 | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
adamc@163 159 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
adamc@163 160 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
adamc@163 161 end.
adamc@158 162
adamc@160 163 Ltac my_crush :=
adamc@160 164 my_crush';
adamc@163 165 repeat (match goal with
adamc@163 166 | [ H : ?F = ?G |- _ ] =>
adamc@163 167 (let H' := fresh "H'" in
adamc@163 168 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
adamc@163 169 | discriminate || injection H'; clear H' ];
adamc@163 170 my_crush';
adamc@163 171 repeat match goal with
adamc@163 172 | [ H : context[fun _ => unit] |- _ ] => clear H
adamc@163 173 end;
adamc@163 174 match type of H with
adamc@163 175 | ?F = ?G =>
adamc@163 176 let ec := equate_conj F G in
adamc@163 177 let var := fresh "var" in
adamc@163 178 assert ec; [ intuition; unfold Exp; apply ext_eq; intro var;
adamc@163 179 assert (H' : F var = G var); try congruence;
adamc@163 180 match type of H' with
adamc@163 181 | ?X = ?Y =>
adamc@163 182 let X := eval hnf in X in
adamc@163 183 let Y := eval hnf in Y in
adamc@163 184 change (X = Y) in H'
adamc@163 185 end; injection H'; my_crush'; tauto
adamc@163 186 | intuition; subst ]
adamc@163 187 end);
adamc@163 188 clear H
adamc@163 189 end; my_crush');
adamc@163 190 my_crush'.
adamc@160 191
adamc@162 192 Hint Extern 1 (_ = _ @ _) => simpl.
adamc@162 193
adamc@158 194 Lemma progress' : forall t (E : Exp t),
adamc@158 195 Closed E
adamc@158 196 -> Val E \/ exists E', E ==> E'.
adamc@158 197 induction 1; crush;
adamc@159 198 repeat match goal with
adamc@159 199 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush
adamc@162 200 end; eauto 6.
adamc@158 201 Qed.
adamc@158 202
adamc@158 203 Theorem progress : forall t (E : Exp t),
adamc@158 204 Val E \/ exists E', E ==> E'.
adamc@158 205 intros; apply progress'; apply closed.
adamc@158 206 Qed.
adamc@158 207
adamc@160 208
adamc@160 209 (** * Big-Step Semantics *)
adamc@160 210
adamc@160 211 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
adamc@160 212
adamc@160 213 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 214 | SConst : forall n,
adamc@160 215 Const n ===> Const n
adamc@160 216 | SPlus : forall E1 E2 n1 n2,
adamc@160 217 E1 ===> Const n1
adamc@160 218 -> E2 ===> Const n2
adamc@160 219 -> Plus E1 E2 ===> Const (n1 + n2)
adamc@160 220
adamc@160 221 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
adamc@160 222 E1 ===> Abs B
adamc@160 223 -> E2 ===> V2
adamc@160 224 -> Subst V2 B ===> V
adamc@160 225 -> App E1 E2 ===> V
adamc@160 226 | SAbs : forall dom ran (B : Exp1 dom ran),
adamc@160 227 Abs B ===> Abs B
adamc@160 228
adamc@160 229 where "E1 ===> E2" := (BigStep E1 E2).
adamc@160 230
adamc@160 231 Hint Constructors BigStep.
adamc@160 232
adamc@160 233 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
adamc@160 234
adamc@160 235 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 236 | Done : forall t (E : Exp t), E ==>* E
adamc@160 237 | OneStep : forall t (E E' E'' : Exp t),
adamc@160 238 E ==> E'
adamc@160 239 -> E' ==>* E''
adamc@160 240 -> E ==>* E''
adamc@160 241
adamc@160 242 where "E1 ==>* E2" := (MultiStep E1 E2).
adamc@160 243
adamc@160 244 Hint Constructors MultiStep.
adamc@160 245
adamc@160 246 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
adamc@160 247 E1 ==>* E2
adamc@160 248 -> E2 ==>* E3
adamc@160 249 -> E1 ==>* E3.
adamc@160 250 induction 1; eauto.
adamc@160 251 Qed.
adamc@160 252
adamc@160 253 Theorem Big_Val : forall t (E V : Exp t),
adamc@160 254 E ===> V
adamc@160 255 -> Val V.
adamc@160 256 induction 1; crush.
adamc@160 257 Qed.
adamc@160 258
adamc@160 259 Theorem Val_Big : forall t (V : Exp t),
adamc@160 260 Val V
adamc@160 261 -> V ===> V.
adamc@160 262 destruct 1; crush.
adamc@160 263 Qed.
adamc@160 264
adamc@160 265 Hint Resolve Big_Val Val_Big.
adamc@160 266
adamc@162 267 Lemma Multi_Cong : forall t t' (C : Ctx t t'),
adamc@162 268 isCtx C
adamc@162 269 -> forall E E', E ==>* E'
adamc@162 270 -> C @ E ==>* C @ E'.
adamc@160 271 induction 2; crush; eauto.
adamc@160 272 Qed.
adamc@160 273
adamc@162 274 Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
adamc@162 275 isCtx C
adamc@162 276 -> E1 = C @ E
adamc@162 277 -> E2 = C @ E'
adamc@162 278 -> E ==>* E'
adamc@162 279 -> E1 ==>* E2.
adamc@162 280 crush; apply Multi_Cong; auto.
adamc@162 281 Qed.
adamc@162 282
adamc@162 283 Hint Resolve Multi_Cong'.
adamc@162 284
adamc@162 285 Ltac mtrans E :=
adamc@162 286 match goal with
adamc@162 287 | [ |- E ==>* _ ] => fail 1
adamc@162 288 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
adamc@162 289 end.
adamc@160 290
adamc@160 291 Theorem Big_Multi : forall t (E V : Exp t),
adamc@160 292 E ===> V
adamc@160 293 -> E ==>* V.
adamc@162 294 induction 1; crush; eauto;
adamc@162 295 repeat match goal with
adamc@162 296 | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
adamc@162 297 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
adamc@162 298 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
adamc@162 299 end.
adamc@160 300 Qed.
adamc@160 301
adamc@160 302 Lemma Big_Val' : forall t (V1 V2 : Exp t),
adamc@160 303 Val V2
adamc@160 304 -> V1 = V2
adamc@160 305 -> V1 ===> V2.
adamc@160 306 crush.
adamc@160 307 Qed.
adamc@160 308
adamc@160 309 Hint Resolve Big_Val'.
adamc@160 310
adamc@160 311 Lemma Multi_Big' : forall t (E E' : Exp t),
adamc@160 312 E ==> E'
adamc@160 313 -> forall E'', E' ===> E''
adamc@160 314 -> E ===> E''.
adamc@160 315 induction 1; crush; eauto;
adamc@160 316 match goal with
adamc@160 317 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
adamc@162 318 end;
adamc@162 319 match goal with
adamc@162 320 | [ H : isCtx _ |- _ ] => inversion H; my_crush; eauto
adamc@160 321 end.
adamc@160 322 Qed.
adamc@160 323
adamc@160 324 Hint Resolve Multi_Big'.
adamc@160 325
adamc@160 326 Theorem Multi_Big : forall t (E V : Exp t),
adamc@160 327 E ==>* V
adamc@160 328 -> Val V
adamc@160 329 -> E ===> V.
adamc@160 330 induction 1; crush; eauto.
adamc@160 331 Qed.
adamc@160 332
adamc@160 333
adamc@160 334 (** * Constant folding *)
adamc@160 335
adamc@160 336 Section cfold.
adamc@160 337 Variable var : type -> Type.
adamc@160 338
adamc@160 339 Fixpoint cfold t (e : exp var t) {struct e} : exp var t :=
adamc@160 340 match e in exp _ t return exp _ t with
adamc@160 341 | Const' n => Const' n
adamc@160 342 | Plus' e1 e2 =>
adamc@160 343 let e1' := cfold e1 in
adamc@160 344 let e2' := cfold e2 in
adamc@160 345 match e1', e2' with
adamc@160 346 | Const' n1, Const' n2 => Const' (n1 + n2)
adamc@160 347 | _, _ => Plus' e1' e2'
adamc@160 348 end
adamc@160 349
adamc@160 350 | Var _ x => Var x
adamc@160 351 | App' _ _ e1 e2 => App' (cfold e1) (cfold e2)
adamc@160 352 | Abs' _ _ e' => Abs' (fun x => cfold (e' x))
adamc@160 353 end.
adamc@160 354 End cfold.
adamc@160 355
adamc@160 356 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@163 357 Definition Cfold1 t1 t2 (E : Exp1 t1 t2) : Exp1 t1 t2 := fun _ x => cfold (E _ x).
adamc@163 358
adamc@163 359 Lemma fold_Cfold : forall t (E : Exp t),
adamc@163 360 (fun _ => cfold (E _)) = Cfold E.
adamc@163 361 reflexivity.
adamc@163 362 Qed.
adamc@163 363
adamc@163 364 Hint Rewrite fold_Cfold : fold.
adamc@163 365
adamc@163 366 Lemma fold_Cfold1 : forall t1 t2 (E : Exp1 t1 t2),
adamc@163 367 (fun _ x => cfold (E _ x)) = Cfold1 E.
adamc@163 368 reflexivity.
adamc@163 369 Qed.
adamc@163 370
adamc@163 371 Lemma fold_Subst_Cfold1 : forall t1 t2 (E : Exp1 t1 t2) (V : Exp t1),
adamc@163 372 (fun _ => flatten (cfold (E _ (V _))))
adamc@163 373 = Subst V (Cfold1 E).
adamc@163 374 reflexivity.
adamc@163 375 Qed.
adamc@163 376
adamc@163 377 Axiom cheat : forall T, T.
adamc@163 378
adamc@163 379
adamc@163 380 Lemma fold_Const : forall n, (fun _ => Const' n) = Const n.
adamc@163 381 reflexivity.
adamc@163 382 Qed.
adamc@163 383 Lemma fold_Plus : forall (E1 E2 : Exp _), (fun _ => Plus' (E1 _) (E2 _)) = Plus E1 E2.
adamc@163 384 reflexivity.
adamc@163 385 Qed.
adamc@163 386 Lemma fold_App : forall dom ran (F : Exp (dom --> ran)) (X : Exp dom),
adamc@163 387 (fun _ => App' (F _) (X _)) = App F X.
adamc@163 388 reflexivity.
adamc@163 389 Qed.
adamc@163 390 Lemma fold_Abs : forall dom ran (B : Exp1 dom ran),
adamc@163 391 (fun _ => Abs' (B _)) = Abs B.
adamc@163 392 reflexivity.
adamc@163 393 Qed.
adamc@163 394
adamc@163 395 Hint Rewrite fold_Const fold_Plus fold_App fold_Abs : fold.
adamc@163 396
adamc@163 397 Lemma fold_Subst : forall t1 t2 (E1 : Exp1 t1 t2) (V : Exp t1),
adamc@163 398 (fun _ => flatten (E1 _ (V _))) = Subst V E1.
adamc@163 399 reflexivity.
adamc@163 400 Qed.
adamc@163 401
adamc@163 402 Hint Rewrite fold_Subst : fold.
adamc@163 403
adamc@163 404 Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t.
adamc@163 405
adamc@163 406 Definition ConstN G (n : nat) : ExpN G Nat :=
adamc@163 407 fun _ _ => Const' n.
adamc@163 408 Definition VarN G t (m : member t G) : ExpN G t := fun _ s => Var (hget s m).
adamc@163 409 Definition PlusN G (E1 E2 : ExpN G Nat) : ExpN G Nat :=
adamc@163 410 fun _ s => Plus' (E1 _ s) (E2 _ s).
adamc@163 411 Definition AppN G dom ran (F : ExpN G (dom --> ran)) (X : ExpN G dom) : ExpN G ran :=
adamc@163 412 fun _ s => App' (F _ s) (X _ s).
adamc@163 413 Definition AbsN G dom ran (B : ExpN (dom :: G) ran) : ExpN G (dom --> ran) :=
adamc@163 414 fun _ s => Abs' (fun x => B _ (x ::: s)).
adamc@163 415
adamc@163 416 Inductive ClosedN : forall G t, ExpN G t -> Prop :=
adamc@163 417 | CConstN : forall G b,
adamc@163 418 ClosedN (ConstN G b)
adamc@163 419 | CPlusN : forall G (E1 E2 : ExpN G _),
adamc@163 420 ClosedN E1
adamc@163 421 -> ClosedN E2
adamc@163 422 -> ClosedN (PlusN E1 E2)
adamc@163 423 | CAppN : forall G dom ran (E1 : ExpN G (dom --> ran)) E2,
adamc@163 424 ClosedN E1
adamc@163 425 -> ClosedN E2
adamc@163 426 -> ClosedN (AppN E1 E2)
adamc@163 427 | CAbsN : forall G dom ran (E1 : ExpN (dom :: G) ran),
adamc@163 428 ClosedN E1
adamc@163 429 -> ClosedN (AbsN E1).
adamc@163 430
adamc@163 431 Axiom closedN : forall G t (E : ExpN G t), ClosedN E.
adamc@163 432
adamc@163 433 Hint Resolve closedN.
adamc@163 434
adamc@163 435 Section Closed1.
adamc@163 436 Variable xt : type.
adamc@163 437
adamc@163 438 Definition Const1 (n : nat) : Exp1 xt Nat :=
adamc@163 439 fun _ _ => Const' n.
adamc@163 440 Definition Var1 : Exp1 xt xt := fun _ x => Var x.
adamc@163 441 Definition Plus1 (E1 E2 : Exp1 xt Nat) : Exp1 xt Nat :=
adamc@163 442 fun _ s => Plus' (E1 _ s) (E2 _ s).
adamc@163 443 Definition App1 dom ran (F : Exp1 xt (dom --> ran)) (X : Exp1 xt dom) : Exp1 xt ran :=
adamc@163 444 fun _ s => App' (F _ s) (X _ s).
adamc@163 445 Definition Abs1 dom ran (B : forall var, var dom -> Exp1 xt ran) : Exp1 xt (dom --> ran) :=
adamc@163 446 fun _ s => Abs' (fun x => B _ x _ s).
adamc@163 447
adamc@163 448 Inductive Closed1 : forall t, Exp1 xt t -> Prop :=
adamc@163 449 | CConst1 : forall b,
adamc@163 450 Closed1 (Const1 b)
adamc@163 451 | CPlus1 : forall E1 E2,
adamc@163 452 Closed1 E1
adamc@163 453 -> Closed1 E2
adamc@163 454 -> Closed1 (Plus1 E1 E2)
adamc@163 455 | CApp1 : forall dom ran (E1 : Exp1 _ (dom --> ran)) E2,
adamc@163 456 Closed1 E1
adamc@163 457 -> Closed1 E2
adamc@163 458 -> Closed1 (App1 E1 E2)
adamc@163 459 | CAbs1 : forall dom ran (E1 : forall var, var dom -> Exp1 _ ran),
adamc@163 460 Closed1 (Abs1 E1).
adamc@163 461
adamc@163 462 Axiom closed1 : forall t (E : Exp1 xt t), Closed1 E.
adamc@163 463 End Closed1.
adamc@163 464
adamc@163 465 Hint Resolve closed1.
adamc@163 466
adamc@163 467 Definition CfoldN G t (E : ExpN G t) : ExpN G t := fun _ s => cfold (E _ s).
adamc@163 468
adamc@163 469 Theorem fold_CfoldN : forall G t (E : ExpN G t),
adamc@163 470 (fun _ s => cfold (E _ s)) = CfoldN E.
adamc@163 471 reflexivity.
adamc@163 472 Qed.
adamc@163 473
adamc@163 474 Definition SubstN t1 G t2 (E1 : ExpN G t1) (E2 : ExpN (G ++ t1 :: nil) t2) : ExpN G t2 :=
adamc@163 475 fun _ s => flatten (E2 _ (hmap (@Var _) s +++ E1 _ s ::: hnil)).
adamc@163 476
adamc@163 477 Lemma fold_SubstN : forall t1 G t2 (E1 : ExpN G t1) (E2 : ExpN (G ++ t1 :: nil) t2),
adamc@163 478 (fun _ s => flatten (E2 _ (hmap (@Var _) s +++ E1 _ s ::: hnil))) = SubstN E1 E2.
adamc@163 479 reflexivity.
adamc@163 480 Qed.
adamc@163 481
adamc@163 482 Hint Rewrite fold_CfoldN fold_SubstN : fold.
adamc@163 483
adamc@163 484 Ltac ssimp := unfold Subst, Cfold, CfoldN, SubstN in *; simpl in *; autorewrite with fold in *;
adamc@163 485 repeat match goal with
adamc@163 486 | [ xt : type |- _ ] =>
adamc@163 487 rewrite (@fold_Subst xt) in *
adamc@163 488 end;
adamc@163 489 autorewrite with fold in *.
adamc@163 490
adamc@163 491 Ltac uiper :=
adamc@163 492 repeat match goal with
adamc@163 493 | [ H : _ = _ |- _ ] =>
adamc@163 494 generalize H; subst; intro H; rewrite (UIP_refl _ _ H)
adamc@163 495 end.
adamc@163 496
adamc@163 497 Section eq_arg.
adamc@163 498 Variable A : Type.
adamc@163 499 Variable B : A -> Type.
adamc@163 500
adamc@163 501 Variable x : A.
adamc@163 502
adamc@163 503 Variables f g : forall x, B x.
adamc@163 504 Hypothesis Heq : f = g.
adamc@163 505
adamc@163 506 Theorem eq_arg : f x = g x.
adamc@163 507 congruence.
adamc@163 508 Qed.
adamc@163 509 End eq_arg.
adamc@163 510
adamc@163 511 Implicit Arguments eq_arg [A B f g].
adamc@163 512
adamc@163 513 (*Lemma Cfold_Subst_comm : forall G t (E : ExpN G t),
adamc@163 514 ClosedN E
adamc@163 515 -> forall t1 G' (pf : G = G' ++ t1 :: nil) V,
adamc@163 516 CfoldN (SubstN V (match pf in _ = G return ExpN G _ with refl_equal => E end))
adamc@163 517 = SubstN (CfoldN V) (CfoldN (match pf in _ = G return ExpN G _ with refl_equal => E end)).
adamc@163 518 induction 1; my_crush; uiper; ssimp; crush;
adamc@163 519 unfold ExpN; do 2 ext_eq.
adamc@163 520
adamc@163 521 generalize (eq_arg x0 (eq_arg x (IHClosedN1 _ _ (refl_equal _) V))).
adamc@163 522 generalize (eq_arg x0 (eq_arg x (IHClosedN2 _ _ (refl_equal _) V))).
adamc@163 523 crush.
adamc@163 524
adamc@163 525 match goal with
adamc@163 526 | [ |- _ = flatten (match ?E with
adamc@163 527 | Const' _ => _
adamc@163 528 | Plus' _ _ => _
adamc@163 529 | Var _ _ => _
adamc@163 530 | App' _ _ _ _ => _
adamc@163 531 | Abs' _ _ _ => _
adamc@163 532 end) ] => dep_destruct E
adamc@163 533 end; crush.
adamc@163 534
adamc@163 535 match goal with
adamc@163 536 | [ |- _ = flatten (match ?E with
adamc@163 537 | Const' _ => _
adamc@163 538 | Plus' _ _ => _
adamc@163 539 | Var _ _ => _
adamc@163 540 | App' _ _ _ _ => _
adamc@163 541 | Abs' _ _ _ => _
adamc@163 542 end) ] => dep_destruct E
adamc@163 543 end; crush.
adamc@163 544
adamc@163 545 match goal with
adamc@163 546 | [ |- match ?E with
adamc@163 547 | Const' _ => _
adamc@163 548 | Plus' _ _ => _
adamc@163 549 | Var _ _ => _
adamc@163 550 | App' _ _ _ _ => _
adamc@163 551 | Abs' _ _ _ => _
adamc@163 552 end = _ ] => dep_destruct E
adamc@163 553 end; crush.
adamc@163 554 rewrite <- H2.
adamc@163 555
adamc@163 556 dep_destruct e.
adamc@163 557 intro
adamc@163 558
adamc@163 559
adamc@163 560 apply cheat.
adamc@163 561
adamc@163 562 unfold ExpN; do 2 ext_eq.
adamc@163 563 generalize (eq_arg x0 (eq_arg x (IHClosedN1 _ _ (refl_equal _) V))).
adamc@163 564 generalize (eq_arg x0 (eq_arg x (IHClosedN2 _ _ (refl_equal _) V))).
adamc@163 565 congruence.
adamc@163 566
adamc@163 567 unfold ExpN; do 2 ext_eq.
adamc@163 568 f_equal.
adamc@163 569 ext_eq.
adamc@163 570 exact (eq_arg (x1 ::: x0) (eq_arg x (IHClosedN _ (dom :: G') (refl_equal _) (fun _ s => V _ (snd s))))).
adamc@163 571 Qed.*)
adamc@163 572
adamc@163 573 Lemma Cfold_Subst' : forall t (E V' : Exp t),
adamc@163 574 E ===> V'
adamc@163 575 -> forall G xt (V : ExpN G xt) B, E = SubstN V B
adamc@163 576 -> ClosedN B
adamc@163 577 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'.
adamc@163 578 induction 1; inversion 2; my_crush; ssimp.
adamc@163 579
adamc@163 580 auto.
adamc@163 581
adamc@163 582 apply cheat.
adamc@163 583
adamc@163 584 my_crush.
adamc@163 585 econstructor.
adamc@163 586 instantiate (1 := Cfold1 B).
adamc@163 587 unfold Subst, Cfold1 in *; eauto.
adamc@163 588 unfold Subst, Cfold1 in *; eauto.
adamc@163 589 unfold Subst, Cfold; eauto.
adamc@163 590
adamc@163 591 my_crush; ssimp.
adamc@163 592
adamc@163 593
adamc@163 594
adamc@163 595
adamc@163 596 Lemma Cfold_Subst' : forall t (B : Exp1 xt t),
adamc@163 597 Closed1 B
adamc@163 598 -> forall V', Subst V B ===> V'
adamc@163 599 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'.
adamc@163 600 induction 1; my_crush; ssimp.
adamc@163 601
adamc@163 602 inversion H; my_crush.
adamc@163 603
adamc@163 604 apply cheat.
adamc@163 605
adamc@163 606 inversion H1; my_crush.
adamc@163 607 econstructor.
adamc@163 608 instantiate (1 := Cfold1 B).
adamc@163 609 eauto.
adamc@163 610 change (Abs (Cfold1 B)) with (Cfold (Abs B)).
adamc@163 611 auto.
adamc@163 612 eauto.
adamc@163 613 eauto.
adamc@163 614
adamc@163 615 apply IHClosed1_1.
adamc@163 616 eauto.
adamc@163 617
adamc@163 618 match goal with
adamc@163 619 | [ (*H : ?F = ?G,*) H2 : ?X (fun _ => unit) = ?Y _ _ _ _ (fun _ => unit) |- _ ] =>
adamc@163 620 idtac(*match X with
adamc@163 621 | Y => fail 1
adamc@163 622 | _ =>
adamc@163 623 idtac(*assert (X = Y); [ unfold Exp; apply ext_eq; intro var;
adamc@163 624 let H' := fresh "H'" in
adamc@163 625 assert (H' : F var = G var); [ congruence
adamc@163 626 | match type of H' with
adamc@163 627 | ?X = ?Y =>
adamc@163 628 let X := eval hnf in X in
adamc@163 629 let Y := eval hnf in Y in
adamc@163 630 change (X = Y) in H'
adamc@163 631 end; injection H'; clear H'; my_crush' ]
adamc@163 632 | my_crush'; clear H2 ]*)
adamc@163 633 end*)
adamc@163 634 end.
adamc@163 635
adamc@163 636 clear H5 H3.
adamc@163 637 my_crush.
adamc@163 638
adamc@163 639
adamc@163 640 unfold Subst in *; simpl in *; autorewrite with fold in *.
adamc@163 641
adamc@163 642
adamc@163 643 Check fold_Subst.
adamc@163 644
adamc@163 645 repeat rewrite (@fold_Subst t1) in *.
adamc@163 646
adamc@163 647 simp (Subst (t2 := Nat) V).
adamc@163 648
adamc@163 649
adamc@163 650 induction 1; my_crush.
adamc@163 651 End Exp1.
adamc@163 652
adamc@163 653 Axiom closed1 : forall t1 t2 (E : Exp1 t1 t2), Closed1 E.
adamc@163 654
adamc@163 655
adamc@163 656
adamc@163 657 Lemma Cfold_Subst' : forall t1 (V : Exp t1) t2 (B : Exp1 t1 t2),
adamc@163 658 Closed1 B
adamc@163 659 -> forall V', Subst V B ===> V'
adamc@163 660 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'.
adamc@163 661 induction 1; my_crush.
adamc@163 662
adamc@163 663 unfold Subst in *; simpl in *; autorewrite with fold in *.
adamc@163 664 inversion H; my_crush.
adamc@163 665
adamc@163 666 unfold Subst in *; simpl in *; autorewrite with fold in *.
adamc@163 667 Check fold_Subst.
adamc@163 668
adamc@163 669 repeat rewrite (@fold_Subst t1) in *.
adamc@163 670
adamc@163 671 simp (Subst (t2 := Nat) V).
adamc@163 672
adamc@163 673
adamc@163 674 induction 1; my_crush.
adamc@163 675
adamc@163 676 Theorem Cfold_Subst : forall t1 t2 (V : Exp t1) B (V' : Exp t2),
adamc@163 677 Subst V B ===> V'
adamc@163 678 -> Subst (Cfold V) (Cfold1 B) ===> Cfold V'.
adamc@163 679
adamc@163 680 Theorem Cfold_correct : forall t (E V : Exp t),
adamc@163 681 E ===> V
adamc@163 682 -> Cfold E ===> Cfold V.
adamc@163 683 induction 1; unfold Cfold in *; crush; simp; auto.
adamc@163 684
adamc@163 685 simp.
adamc@163 686 simp.
adamc@163 687 apply cheat.
adamc@163 688
adamc@163 689 simp.
adamc@163 690 econstructor; eauto.
adamc@163 691
adamc@163 692
adamc@163 693
adamc@163 694 match goal with
adamc@163 695 | [ |- ?E ===> ?V ] =>
adamc@163 696 try simp1 ltac:(fun E' => change (E' ===> V));
adamc@163 697 try match goal with
adamc@163 698 | [ |- ?E' ===> _ ] =>
adamc@163 699 simp1 ltac:(fun V' => change (E' ===> V'))
adamc@163 700 end
adamc@163 701 | [ H : ?E ===> ?V |- _ ] =>
adamc@163 702 try simp1 ltac:(fun E' => change (E' ===> V) in H);
adamc@163 703 try match type of H with
adamc@163 704 | ?E' ===> _ =>
adamc@163 705 simp1 ltac:(fun V' => change (E' ===> V') in H)
adamc@163 706 end
adamc@163 707 end.
adamc@163 708 simp.
adamc@163 709
adamc@163 710 let H := IHBigStep1 in
adamc@163 711 match type of H with
adamc@163 712 | ?E ===> ?V =>
adamc@163 713 try simp1 ltac:(fun E' => change (E' ===> V) in H);
adamc@163 714 try match type of H with
adamc@163 715 | ?E' ===> _ =>
adamc@163 716 simp1 ltac:(fun V' => change (E' ===> V') in H)
adamc@163 717 end
adamc@163 718 end.
adamc@163 719
adamc@163 720 try simp1 ltac:(fun E' => change (E' ===> V) in H)
adamc@163 721 end.
adamc@163 722
adamc@163 723 simp.
adamc@163 724
adamc@163 725 try simp1 ltac:(fun E' => change (fun H : type -> Type => cfold (E1 H)) with E' in IHBigStep1).
adamc@163 726 try simp1 ltac:(fun V' => change (fun H : type -> Type =>
adamc@163 727 Abs' (dom:=dom) (fun x : H dom => cfold (B H x))) with V' in IHBigStep1).
adamc@163 728
adamc@163 729 simp1 ltac:(fun E => change ((fun H : type -> Type => cfold (E1 H)) ===> E) in IHBigStep1).
adamc@163 730
adamc@163 731 change ((fun H : type -> Type => cfold (E1 H)) ===> Abs (fun _ x => cfold (B _ x))) in IHBigStep1.
adamc@163 732 (fun H : type -> Type =>
adamc@163 733 Abs' (dom:=dom) (fun x : H dom => cfold (B H x)))
adamc@163 734
adamc@163 735 fold Cfold.
adamc@163 736
adamc@160 737
adamc@160 738
adamc@160 739 Definition ExpN (G : list type) (t : type) := forall var, hlist var G -> exp var t.
adamc@160 740
adamc@160 741 Definition ConstN G (n : nat) : ExpN G Nat :=
adamc@160 742 fun _ _ => Const' n.
adamc@160 743 Definition PlusN G (E1 E2 : ExpN G Nat) : ExpN G Nat :=
adamc@160 744 fun _ s => Plus' (E1 _ s) (E2 _ s).
adamc@160 745 Definition AppN G dom ran (F : ExpN G (dom --> ran)) (X : ExpN G dom) : ExpN G ran :=
adamc@160 746 fun _ s => App' (F _ s) (X _ s).
adamc@160 747 Definition AbsN G dom ran (B : ExpN (dom :: G) ran) : ExpN G (dom --> ran) :=
adamc@162 748 fun _ s => Abs' (fun x => B _ (x ::: s)).