Mercurial > cpdt > repo

annotate src/Firstorder.v @ 156:be15ed0a8bae

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
De Bruijn
author Adam Chlipala <adamc@hcoop.net>
date Sun, 02 Nov 2008 13:51:51 -0500
parents b31ca896f211
children 2022e3f2aa26
rev   line source
adamc@152 1 (* Copyright (c) 2008, Adam Chlipala
adamc@152 2 *
adamc@152 3 * This work is licensed under a
adamc@152 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@152 5 * Unported License.
adamc@152 6 * The license text is available at:
adamc@152 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@152 8 *)
adamc@152 9
adamc@152 10 (* begin hide *)
adamc@156 11 Require Import Arith String List.
adamc@152 12
adamc@152 13 Require Import Tactics.
adamc@152 14
adamc@152 15 Set Implicit Arguments.
adamc@152 16 (* end hide *)
adamc@152 17
adamc@152 18
adamc@153 19 (** %\part{Formalizing Programming Languages and Compilers}
adamc@152 20
adamc@153 21 \chapter{First-Order Abstract Syntax}% *)
adamc@152 22
adamc@152 23 (** TODO: Prose for this chapter *)
adamc@152 24
adamc@152 25
adamc@152 26 (** * Concrete Binding *)
adamc@152 27
adamc@152 28 Module Concrete.
adamc@152 29
adamc@152 30 Definition var := string.
adamc@152 31 Definition var_eq := string_dec.
adamc@152 32
adamc@152 33 Inductive exp : Set :=
adamc@152 34 | Const : bool -> exp
adamc@152 35 | Var : var -> exp
adamc@152 36 | App : exp -> exp -> exp
adamc@152 37 | Abs : var -> exp -> exp.
adamc@152 38
adamc@152 39 Inductive type : Set :=
adamc@152 40 | Bool : type
adamc@152 41 | Arrow : type -> type -> type.
adamc@152 42
adamc@152 43 Infix "-->" := Arrow (right associativity, at level 60).
adamc@152 44
adamc@152 45 Definition ctx := list (var * type).
adamc@152 46
adamc@152 47 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@152 48
adamc@152 49 Inductive lookup : ctx -> var -> type -> Prop :=
adamc@152 50 | First : forall x t G,
adamc@152 51 (x, t) :: G |-v x : t
adamc@152 52 | Next : forall x t x' t' G,
adamc@152 53 x <> x'
adamc@152 54 -> G |-v x : t
adamc@152 55 -> (x', t') :: G |-v x : t
adamc@152 56
adamc@152 57 where "G |-v x : t" := (lookup G x t).
adamc@152 58
adamc@152 59 Hint Constructors lookup.
adamc@152 60
adamc@152 61 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@152 62
adamc@152 63 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@152 64 | TConst : forall G b,
adamc@152 65 G |-e Const b : Bool
adamc@152 66 | TVar : forall G v t,
adamc@152 67 G |-v v : t
adamc@152 68 -> G |-e Var v : t
adamc@152 69 | TApp : forall G e1 e2 dom ran,
adamc@152 70 G |-e e1 : dom --> ran
adamc@152 71 -> G |-e e2 : dom
adamc@152 72 -> G |-e App e1 e2 : ran
adamc@152 73 | TAbs : forall G x e' dom ran,
adamc@152 74 (x, dom) :: G |-e e' : ran
adamc@152 75 -> G |-e Abs x e' : dom --> ran
adamc@152 76
adamc@152 77 where "G |-e e : t" := (hasType G e t).
adamc@152 78
adamc@152 79 Hint Constructors hasType.
adamc@152 80
adamc@152 81 Notation "x ## G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
adamc@152 82
adamc@152 83 Notation "G' # G" := (forall (x : var) (t : type), In (x, t) G -> x ## G') (no associativity, at level 90).
adamc@152 84
adamc@152 85 Lemma lookup_In : forall G x t,
adamc@152 86 G |-v x : t
adamc@152 87 -> In (x, t) G.
adamc@152 88 induction 1; crush.
adamc@152 89 Qed.
adamc@152 90
adamc@152 91 Hint Resolve lookup_In.
adamc@152 92
adamc@152 93 Lemma disjoint_invert1 : forall G x t G' x' t',
adamc@152 94 G |-v x : t
adamc@152 95 -> (x', t') :: G' # G
adamc@152 96 -> x <> x'.
adamc@152 97 crush; eauto.
adamc@152 98 Qed.
adamc@152 99
adamc@152 100 Lemma disjoint_invert2 : forall G' G p,
adamc@152 101 p :: G' # G
adamc@152 102 -> G' # G.
adamc@152 103 firstorder.
adamc@152 104 Qed.
adamc@152 105
adamc@152 106 Hint Resolve disjoint_invert1 disjoint_invert2.
adamc@152 107 Hint Extern 1 (_ <> _) => (intro; subst).
adamc@152 108
adamc@152 109 Lemma weaken_lookup' : forall G x t,
adamc@152 110 G |-v x : t
adamc@152 111 -> forall G', G' # G
adamc@152 112 -> G' ++ G |-v x : t.
adamc@152 113 induction G' as [ | [x' t'] tl ]; crush; eauto 9.
adamc@152 114 Qed.
adamc@152 115
adamc@155 116 Lemma weaken_lookup : forall x t G' G1,
adamc@155 117 G1 |-v x : t
adamc@155 118 -> G1 ++ G' |-v x : t.
adamc@152 119 Hint Resolve weaken_lookup'.
adamc@152 120
adamc@152 121 induction G1 as [ | [x' t'] tl ]; crush;
adamc@152 122 match goal with
adamc@152 123 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
adamc@152 124 end.
adamc@152 125 Qed.
adamc@152 126
adamc@152 127 Hint Resolve weaken_lookup.
adamc@152 128
adamc@152 129 Theorem weaken_hasType' : forall G' G e t,
adamc@152 130 G |-e e : t
adamc@155 131 -> G ++ G' |-e e : t.
adamc@152 132 induction 1; crush; eauto.
adamc@152 133 Qed.
adamc@152 134
adamc@155 135 Theorem weaken_hasType : forall e t,
adamc@155 136 nil |-e e : t
adamc@155 137 -> forall G', G' |-e e : t.
adamc@155 138 intros; change G' with (nil ++ G');
adamc@152 139 eapply weaken_hasType'; eauto.
adamc@152 140 Qed.
adamc@152 141
adamc@152 142 Theorem weaken_hasType_closed : forall e t,
adamc@152 143 nil |-e e : t
adamc@152 144 -> forall G, G |-e e : t.
adamc@152 145 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
adamc@152 146 Qed.
adamc@152 147
adamc@155 148 Theorem weaken_hasType1 : forall e t,
adamc@155 149 nil |-e e : t
adamc@155 150 -> forall x t', (x, t') :: nil |-e e : t.
adamc@155 151 intros; change ((x, t') :: nil) with (((x, t') :: nil) ++ nil);
adamc@155 152 apply weaken_hasType; crush.
adamc@152 153 Qed.
adamc@152 154
adamc@152 155 Hint Resolve weaken_hasType_closed weaken_hasType1.
adamc@152 156
adamc@152 157 Section subst.
adamc@152 158 Variable x : var.
adamc@152 159 Variable e1 : exp.
adamc@152 160
adamc@152 161 Fixpoint subst (e2 : exp) : exp :=
adamc@152 162 match e2 with
adamc@152 163 | Const b => Const b
adamc@152 164 | Var x' =>
adamc@152 165 if var_eq x' x
adamc@152 166 then e1
adamc@152 167 else Var x'
adamc@152 168 | App e1 e2 => App (subst e1) (subst e2)
adamc@152 169 | Abs x' e' =>
adamc@152 170 Abs x' (if var_eq x' x
adamc@152 171 then e'
adamc@152 172 else subst e')
adamc@152 173 end.
adamc@152 174
adamc@152 175 Variable xt : type.
adamc@152 176 Hypothesis Ht' : nil |-e e1 : xt.
adamc@152 177
adamc@152 178 Lemma subst_lookup' : forall G2 x' t,
adamc@152 179 x' ## G2
adamc@152 180 -> (x, xt) :: G2 |-v x' : t
adamc@152 181 -> t = xt.
adamc@152 182 inversion 2; crush; elimtype False; eauto.
adamc@152 183 Qed.
adamc@152 184
adamc@155 185 Lemma subst_lookup : forall x' t,
adamc@152 186 x <> x'
adamc@155 187 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 188 -> G1 |-v x' : t.
adamc@152 189 induction G1 as [ | [x'' t'] tl ]; crush;
adamc@152 190 match goal with
adamc@152 191 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@152 192 end; crush.
adamc@152 193 Qed.
adamc@152 194
adamc@152 195 Hint Resolve subst_lookup.
adamc@152 196
adamc@155 197 Lemma subst_lookup'' : forall x' t G1,
adamc@155 198 x' ## G1
adamc@155 199 -> G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 200 -> t = xt.
adamc@152 201 Hint Resolve subst_lookup'.
adamc@152 202
adamc@152 203 induction G1 as [ | [x'' t'] tl ]; crush; eauto;
adamc@152 204 match goal with
adamc@152 205 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@155 206 end; crush; elimtype False; eauto;
adamc@155 207 match goal with
adamc@155 208 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@155 209 end.
adamc@152 210 Qed.
adamc@152 211
adamc@155 212 Implicit Arguments subst_lookup'' [x' t G1].
adamc@152 213
adamc@152 214 Lemma disjoint_cons : forall x x' t (G : ctx),
adamc@152 215 x ## G
adamc@152 216 -> x' <> x
adamc@152 217 -> x ## (x', t) :: G.
adamc@152 218 firstorder;
adamc@152 219 match goal with
adamc@152 220 | [ H : (_, _) = (_, _) |- _ ] => injection H
adamc@152 221 end; crush.
adamc@152 222 Qed.
adamc@152 223
adamc@152 224 Hint Resolve disjoint_cons.
adamc@152 225
adamc@155 226 Lemma shadow_lookup : forall v t t' G1,
adamc@152 227 G1 |-v x : t'
adamc@155 228 -> G1 ++ (x, xt) :: nil |-v v : t
adamc@155 229 -> G1 |-v v : t.
adamc@152 230 induction G1 as [ | [x'' t''] tl ]; crush;
adamc@152 231 match goal with
adamc@152 232 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@152 233 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
adamc@152 234 inversion H1; crush; inversion H2; crush
adamc@152 235 end.
adamc@152 236 Qed.
adamc@152 237
adamc@155 238 Lemma shadow_hasType' : forall G e t,
adamc@152 239 G |-e e : t
adamc@155 240 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@152 241 -> forall t'', G1 |-v x : t''
adamc@155 242 -> G1 |-e e : t.
adamc@152 243 Hint Resolve shadow_lookup.
adamc@152 244
adamc@152 245 induction 1; crush; eauto;
adamc@152 246 match goal with
adamc@152 247 | [ H : (?x0, _) :: _ ++ (x, _) :: _ |-e _ : _ |- _ ] =>
adamc@152 248 destruct (var_eq x0 x); subst; eauto
adamc@152 249 end.
adamc@155 250 Qed.
adamc@152 251
adamc@155 252 Lemma shadow_hasType : forall G1 e t t'',
adamc@155 253 G1 ++ (x, xt) :: nil |-e e : t
adamc@152 254 -> G1 |-v x : t''
adamc@155 255 -> G1 |-e e : t.
adamc@152 256 intros; eapply shadow_hasType'; eauto.
adamc@152 257 Qed.
adamc@152 258
adamc@152 259 Hint Resolve shadow_hasType.
adamc@152 260
adamc@152 261 Theorem subst_hasType : forall G e2 t,
adamc@152 262 G |-e e2 : t
adamc@155 263 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@152 264 -> x ## G1
adamc@155 265 -> G1 |-e subst e2 : t.
adamc@152 266 induction 1; crush;
adamc@152 267 try match goal with
adamc@152 268 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@152 269 end; crush; eauto 6;
adamc@152 270 match goal with
adamc@155 271 | [ H1 : x ## _, H2 : _ |-v x : _ |- _ ] =>
adamc@155 272 rewrite (subst_lookup'' H1 H2)
adamc@152 273 end; crush.
adamc@152 274 Qed.
adamc@152 275
adamc@152 276 Theorem subst_hasType_closed : forall e2 t,
adamc@152 277 (x, xt) :: nil |-e e2 : t
adamc@152 278 -> nil |-e subst e2 : t.
adamc@155 279 intros; eapply subst_hasType; eauto.
adamc@152 280 Qed.
adamc@152 281 End subst.
adamc@152 282
adamc@154 283 Hint Resolve subst_hasType_closed.
adamc@154 284
adamc@154 285 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
adamc@154 286
adamc@154 287 Inductive val : exp -> Prop :=
adamc@154 288 | VConst : forall b, val (Const b)
adamc@154 289 | VAbs : forall x e, val (Abs x e).
adamc@154 290
adamc@154 291 Hint Constructors val.
adamc@154 292
adamc@154 293 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@154 294
adamc@154 295 Inductive step : exp -> exp -> Prop :=
adamc@154 296 | Beta : forall x e1 e2,
adamc@154 297 App (Abs x e1) e2 ==> [x ~> e2] e1
adamc@154 298 | Cong1 : forall e1 e2 e1',
adamc@154 299 e1 ==> e1'
adamc@154 300 -> App e1 e2 ==> App e1' e2
adamc@154 301 | Cong2 : forall e1 e2 e2',
adamc@154 302 val e1
adamc@154 303 -> e2 ==> e2'
adamc@154 304 -> App e1 e2 ==> App e1 e2'
adamc@154 305
adamc@154 306 where "e1 ==> e2" := (step e1 e2).
adamc@154 307
adamc@154 308 Hint Constructors step.
adamc@154 309
adamc@155 310 Lemma progress' : forall G e t, G |-e e : t
adamc@154 311 -> G = nil
adamc@154 312 -> val e \/ exists e', e ==> e'.
adamc@154 313 induction 1; crush; eauto;
adamc@154 314 try match goal with
adamc@154 315 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@154 316 end;
adamc@154 317 repeat match goal with
adamc@154 318 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@154 319 end.
adamc@154 320 Qed.
adamc@154 321
adamc@155 322 Theorem progress : forall e t, nil |-e e : t
adamc@155 323 -> val e \/ exists e', e ==> e'.
adamc@155 324 intros; eapply progress'; eauto.
adamc@155 325 Qed.
adamc@155 326
adamc@155 327 Lemma preservation' : forall G e t, G |-e e : t
adamc@154 328 -> G = nil
adamc@154 329 -> forall e', e ==> e'
adamc@155 330 -> nil |-e e' : t.
adamc@154 331 induction 1; inversion 2; crush; eauto;
adamc@154 332 match goal with
adamc@154 333 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
adamc@154 334 end; eauto.
adamc@154 335 Qed.
adamc@154 336
adamc@155 337 Theorem preservation : forall e t, nil |-e e : t
adamc@155 338 -> forall e', e ==> e'
adamc@155 339 -> nil |-e e' : t.
adamc@155 340 intros; eapply preservation'; eauto.
adamc@155 341 Qed.
adamc@155 342
adamc@152 343 End Concrete.
adamc@156 344
adamc@156 345
adamc@156 346 (** * De Bruijn Indices *)
adamc@156 347
adamc@156 348 Module DeBruijn.
adamc@156 349
adamc@156 350 Definition var := nat.
adamc@156 351 Definition var_eq := eq_nat_dec.
adamc@156 352
adamc@156 353 Inductive exp : Set :=
adamc@156 354 | Const : bool -> exp
adamc@156 355 | Var : var -> exp
adamc@156 356 | App : exp -> exp -> exp
adamc@156 357 | Abs : exp -> exp.
adamc@156 358
adamc@156 359 Inductive type : Set :=
adamc@156 360 | Bool : type
adamc@156 361 | Arrow : type -> type -> type.
adamc@156 362
adamc@156 363 Infix "-->" := Arrow (right associativity, at level 60).
adamc@156 364
adamc@156 365 Definition ctx := list type.
adamc@156 366
adamc@156 367 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@156 368
adamc@156 369 Inductive lookup : ctx -> var -> type -> Prop :=
adamc@156 370 | First : forall t G,
adamc@156 371 t :: G |-v O : t
adamc@156 372 | Next : forall x t t' G,
adamc@156 373 G |-v x : t
adamc@156 374 -> t' :: G |-v S x : t
adamc@156 375
adamc@156 376 where "G |-v x : t" := (lookup G x t).
adamc@156 377
adamc@156 378 Hint Constructors lookup.
adamc@156 379
adamc@156 380 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@156 381
adamc@156 382 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@156 383 | TConst : forall G b,
adamc@156 384 G |-e Const b : Bool
adamc@156 385 | TVar : forall G v t,
adamc@156 386 G |-v v : t
adamc@156 387 -> G |-e Var v : t
adamc@156 388 | TApp : forall G e1 e2 dom ran,
adamc@156 389 G |-e e1 : dom --> ran
adamc@156 390 -> G |-e e2 : dom
adamc@156 391 -> G |-e App e1 e2 : ran
adamc@156 392 | TAbs : forall G e' dom ran,
adamc@156 393 dom :: G |-e e' : ran
adamc@156 394 -> G |-e Abs e' : dom --> ran
adamc@156 395
adamc@156 396 where "G |-e e : t" := (hasType G e t).
adamc@156 397
adamc@156 398 Hint Constructors hasType.
adamc@156 399
adamc@156 400 Lemma weaken_lookup : forall G' v t G,
adamc@156 401 G |-v v : t
adamc@156 402 -> G ++ G' |-v v : t.
adamc@156 403 induction 1; crush.
adamc@156 404 Qed.
adamc@156 405
adamc@156 406 Hint Resolve weaken_lookup.
adamc@156 407
adamc@156 408 Theorem weaken_hasType' : forall G' G e t,
adamc@156 409 G |-e e : t
adamc@156 410 -> G ++ G' |-e e : t.
adamc@156 411 induction 1; crush; eauto.
adamc@156 412 Qed.
adamc@156 413
adamc@156 414 Theorem weaken_hasType : forall e t,
adamc@156 415 nil |-e e : t
adamc@156 416 -> forall G', G' |-e e : t.
adamc@156 417 intros; change G' with (nil ++ G');
adamc@156 418 eapply weaken_hasType'; eauto.
adamc@156 419 Qed.
adamc@156 420
adamc@156 421 Theorem weaken_hasType_closed : forall e t,
adamc@156 422 nil |-e e : t
adamc@156 423 -> forall G, G |-e e : t.
adamc@156 424 intros; rewrite (app_nil_end G); apply weaken_hasType; auto.
adamc@156 425 Qed.
adamc@156 426
adamc@156 427 Theorem weaken_hasType1 : forall e t,
adamc@156 428 nil |-e e : t
adamc@156 429 -> forall t', t' :: nil |-e e : t.
adamc@156 430 intros; change (t' :: nil) with ((t' :: nil) ++ nil);
adamc@156 431 apply weaken_hasType; crush.
adamc@156 432 Qed.
adamc@156 433
adamc@156 434 Hint Resolve weaken_hasType_closed weaken_hasType1.
adamc@156 435
adamc@156 436 Section subst.
adamc@156 437 Variable e1 : exp.
adamc@156 438
adamc@156 439 Fixpoint subst (x : var) (e2 : exp) : exp :=
adamc@156 440 match e2 with
adamc@156 441 | Const b => Const b
adamc@156 442 | Var x' =>
adamc@156 443 if var_eq x' x
adamc@156 444 then e1
adamc@156 445 else Var x'
adamc@156 446 | App e1 e2 => App (subst x e1) (subst x e2)
adamc@156 447 | Abs e' => Abs (subst (S x) e')
adamc@156 448 end.
adamc@156 449
adamc@156 450 Variable xt : type.
adamc@156 451
adamc@156 452 Lemma subst_eq : forall t G1,
adamc@156 453 G1 ++ xt :: nil |-v length G1 : t
adamc@156 454 -> t = xt.
adamc@156 455 induction G1; inversion 1; crush.
adamc@156 456 Qed.
adamc@156 457
adamc@156 458 Implicit Arguments subst_eq [t G1].
adamc@156 459
adamc@156 460 Lemma subst_eq' : forall t G1 x,
adamc@156 461 G1 ++ xt :: nil |-v x : t
adamc@156 462 -> x <> length G1
adamc@156 463 -> G1 |-v x : t.
adamc@156 464 induction G1; inversion 1; crush;
adamc@156 465 match goal with
adamc@156 466 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@156 467 end.
adamc@156 468 Qed.
adamc@156 469
adamc@156 470 Hint Resolve subst_eq'.
adamc@156 471
adamc@156 472 Lemma subst_neq : forall v t G1,
adamc@156 473 G1 ++ xt :: nil |-v v : t
adamc@156 474 -> v <> length G1
adamc@156 475 -> G1 |-e Var v : t.
adamc@156 476 induction G1; inversion 1; crush.
adamc@156 477 Qed.
adamc@156 478
adamc@156 479 Hint Resolve subst_neq.
adamc@156 480
adamc@156 481 Hypothesis Ht' : nil |-e e1 : xt.
adamc@156 482
adamc@156 483 Lemma hasType_push : forall dom G1 e' ran,
adamc@156 484 dom :: G1 |-e subst (length (dom :: G1)) e' : ran
adamc@156 485 -> dom :: G1 |-e subst (S (length G1)) e' : ran.
adamc@156 486 trivial.
adamc@156 487 Qed.
adamc@156 488
adamc@156 489 Hint Resolve hasType_push.
adamc@156 490
adamc@156 491 Theorem subst_hasType : forall G e2 t,
adamc@156 492 G |-e e2 : t
adamc@156 493 -> forall G1, G = G1 ++ xt :: nil
adamc@156 494 -> G1 |-e subst (length G1) e2 : t.
adamc@156 495 induction 1; crush;
adamc@156 496 try match goal with
adamc@156 497 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@156 498 end; crush; eauto 6;
adamc@156 499 try match goal with
adamc@156 500 | [ H : _ |-v _ : _ |- _ ] =>
adamc@156 501 rewrite (subst_eq H)
adamc@156 502 end; crush.
adamc@156 503 Qed.
adamc@156 504
adamc@156 505 Theorem subst_hasType_closed : forall e2 t,
adamc@156 506 xt :: nil |-e e2 : t
adamc@156 507 -> nil |-e subst O e2 : t.
adamc@156 508 intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
adamc@156 509 Qed.
adamc@156 510 End subst.
adamc@156 511
adamc@156 512 Hint Resolve subst_hasType_closed.
adamc@156 513
adamc@156 514 Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
adamc@156 515
adamc@156 516 Inductive val : exp -> Prop :=
adamc@156 517 | VConst : forall b, val (Const b)
adamc@156 518 | VAbs : forall e, val (Abs e).
adamc@156 519
adamc@156 520 Hint Constructors val.
adamc@156 521
adamc@156 522 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@156 523
adamc@156 524 Inductive step : exp -> exp -> Prop :=
adamc@156 525 | Beta : forall e1 e2,
adamc@156 526 App (Abs e1) e2 ==> [O ~> e2] e1
adamc@156 527 | Cong1 : forall e1 e2 e1',
adamc@156 528 e1 ==> e1'
adamc@156 529 -> App e1 e2 ==> App e1' e2
adamc@156 530 | Cong2 : forall e1 e2 e2',
adamc@156 531 val e1
adamc@156 532 -> e2 ==> e2'
adamc@156 533 -> App e1 e2 ==> App e1 e2'
adamc@156 534
adamc@156 535 where "e1 ==> e2" := (step e1 e2).
adamc@156 536
adamc@156 537 Hint Constructors step.
adamc@156 538
adamc@156 539 Lemma progress' : forall G e t, G |-e e : t
adamc@156 540 -> G = nil
adamc@156 541 -> val e \/ exists e', e ==> e'.
adamc@156 542 induction 1; crush; eauto;
adamc@156 543 try match goal with
adamc@156 544 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@156 545 end;
adamc@156 546 repeat match goal with
adamc@156 547 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@156 548 end.
adamc@156 549 Qed.
adamc@156 550
adamc@156 551 Theorem progress : forall e t, nil |-e e : t
adamc@156 552 -> val e \/ exists e', e ==> e'.
adamc@156 553 intros; eapply progress'; eauto.
adamc@156 554 Qed.
adamc@156 555
adamc@156 556 Lemma preservation' : forall G e t, G |-e e : t
adamc@156 557 -> G = nil
adamc@156 558 -> forall e', e ==> e'
adamc@156 559 -> nil |-e e' : t.
adamc@156 560 induction 1; inversion 2; crush; eauto;
adamc@156 561 match goal with
adamc@156 562 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
adamc@156 563 end; eauto.
adamc@156 564 Qed.
adamc@156 565
adamc@156 566 Theorem preservation : forall e t, nil |-e e : t
adamc@156 567 -> forall e', e ==> e'
adamc@156 568 -> nil |-e e' : t.
adamc@156 569 intros; eapply preservation'; eauto.
adamc@156 570 Qed.
adamc@156 571
adamc@156 572 End DeBruijn.