Mercurial > cpdt > repo

annotate src/Firstorder.v @ 228:0be1a42b3035

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proof-reading pass through first bit of Universes
author Adam Chlipala <adamc@hcoop.net>
date Fri, 20 Nov 2009 10:18:35 -0500
parents 13620dfd5f97
children 4b001a611e79
rev   line source
adamc@222 1 (* Copyright (c) 2008-2009, 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@155 81 Lemma weaken_lookup : forall x t G' G1,
adamc@155 82 G1 |-v x : t
adamc@155 83 -> G1 ++ G' |-v x : t.
adamc@152 84 induction G1 as [ | [x' t'] tl ]; crush;
adamc@152 85 match goal with
adamc@152 86 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
adamc@152 87 end.
adamc@152 88 Qed.
adamc@152 89
adamc@152 90 Hint Resolve weaken_lookup.
adamc@152 91
adamc@152 92 Theorem weaken_hasType' : forall G' G e t,
adamc@152 93 G |-e e : t
adamc@155 94 -> G ++ G' |-e e : t.
adamc@152 95 induction 1; crush; eauto.
adamc@152 96 Qed.
adamc@152 97
adamc@155 98 Theorem weaken_hasType : forall e t,
adamc@155 99 nil |-e e : t
adamc@155 100 -> forall G', G' |-e e : t.
adamc@155 101 intros; change G' with (nil ++ G');
adamc@152 102 eapply weaken_hasType'; eauto.
adamc@152 103 Qed.
adamc@152 104
adamc@161 105 Hint Resolve weaken_hasType.
adamc@152 106
adamc@152 107 Section subst.
adamc@152 108 Variable x : var.
adamc@152 109 Variable e1 : exp.
adamc@152 110
adamc@152 111 Fixpoint subst (e2 : exp) : exp :=
adamc@152 112 match e2 with
adamc@152 113 | Const b => Const b
adamc@152 114 | Var x' =>
adamc@152 115 if var_eq x' x
adamc@152 116 then e1
adamc@152 117 else Var x'
adamc@152 118 | App e1 e2 => App (subst e1) (subst e2)
adamc@152 119 | Abs x' e' =>
adamc@152 120 Abs x' (if var_eq x' x
adamc@152 121 then e'
adamc@152 122 else subst e')
adamc@152 123 end.
adamc@152 124
adamc@152 125 Variable xt : type.
adamc@152 126 Hypothesis Ht' : nil |-e e1 : xt.
adamc@152 127
adamc@157 128 Notation "x # G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
adamc@152 129
adamc@157 130 Lemma subst_lookup' : forall x' t,
adamc@152 131 x <> x'
adamc@155 132 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 133 -> G1 |-v x' : t.
adamc@152 134 induction G1 as [ | [x'' t'] tl ]; crush;
adamc@152 135 match goal with
adamc@152 136 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@152 137 end; crush.
adamc@152 138 Qed.
adamc@152 139
adamc@157 140 Hint Resolve subst_lookup'.
adamc@152 141
adamc@157 142 Lemma subst_lookup : forall x' t G1,
adamc@157 143 x' # G1
adamc@155 144 -> G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 145 -> t = xt.
adamc@152 146 induction G1 as [ | [x'' t'] tl ]; crush; eauto;
adamc@152 147 match goal with
adamc@152 148 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@183 149 end; crush; (elimtype False; eauto;
adamc@183 150 match goal with
adamc@183 151 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@183 152 end)
adamc@183 153 || match goal with
adamc@183 154 | [ H : _ |- _ ] => apply H; crush; eauto
adamc@183 155 end.
adamc@152 156 Qed.
adamc@152 157
adamc@157 158 Implicit Arguments subst_lookup [x' t G1].
adamc@152 159
adamc@155 160 Lemma shadow_lookup : forall v t t' G1,
adamc@152 161 G1 |-v x : t'
adamc@155 162 -> G1 ++ (x, xt) :: nil |-v v : t
adamc@155 163 -> G1 |-v v : t.
adamc@152 164 induction G1 as [ | [x'' t''] tl ]; crush;
adamc@152 165 match goal with
adamc@152 166 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@152 167 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
adamc@152 168 inversion H1; crush; inversion H2; crush
adamc@152 169 end.
adamc@152 170 Qed.
adamc@152 171
adamc@155 172 Lemma shadow_hasType' : forall G e t,
adamc@152 173 G |-e e : t
adamc@155 174 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@152 175 -> forall t'', G1 |-v x : t''
adamc@155 176 -> G1 |-e e : t.
adamc@152 177 Hint Resolve shadow_lookup.
adamc@152 178
adamc@152 179 induction 1; crush; eauto;
adamc@152 180 match goal with
adamc@152 181 | [ H : (?x0, _) :: _ ++ (x, _) :: _ |-e _ : _ |- _ ] =>
adamc@152 182 destruct (var_eq x0 x); subst; eauto
adamc@152 183 end.
adamc@155 184 Qed.
adamc@152 185
adamc@155 186 Lemma shadow_hasType : forall G1 e t t'',
adamc@155 187 G1 ++ (x, xt) :: nil |-e e : t
adamc@152 188 -> G1 |-v x : t''
adamc@155 189 -> G1 |-e e : t.
adamc@152 190 intros; eapply shadow_hasType'; eauto.
adamc@152 191 Qed.
adamc@152 192
adamc@152 193 Hint Resolve shadow_hasType.
adamc@152 194
adamc@157 195 Lemma disjoint_cons : forall x x' t (G : ctx),
adamc@157 196 x # G
adamc@157 197 -> x' <> x
adamc@157 198 -> x # (x', t) :: G.
adamc@157 199 firstorder;
adamc@157 200 match goal with
adamc@157 201 | [ H : (_, _) = (_, _) |- _ ] => injection H
adamc@157 202 end; crush.
adamc@157 203 Qed.
adamc@157 204
adamc@157 205 Hint Resolve disjoint_cons.
adamc@157 206
adamc@152 207 Theorem subst_hasType : forall G e2 t,
adamc@152 208 G |-e e2 : t
adamc@155 209 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@157 210 -> x # G1
adamc@155 211 -> G1 |-e subst e2 : t.
adamc@152 212 induction 1; crush;
adamc@152 213 try match goal with
adamc@152 214 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@152 215 end; crush; eauto 6;
adamc@152 216 match goal with
adamc@157 217 | [ H1 : x # _, H2 : _ |-v x : _ |- _ ] =>
adamc@157 218 rewrite (subst_lookup H1 H2)
adamc@152 219 end; crush.
adamc@152 220 Qed.
adamc@152 221
adamc@152 222 Theorem subst_hasType_closed : forall e2 t,
adamc@152 223 (x, xt) :: nil |-e e2 : t
adamc@152 224 -> nil |-e subst e2 : t.
adamc@155 225 intros; eapply subst_hasType; eauto.
adamc@152 226 Qed.
adamc@152 227 End subst.
adamc@152 228
adamc@154 229 Hint Resolve subst_hasType_closed.
adamc@154 230
adamc@154 231 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
adamc@154 232
adamc@154 233 Inductive val : exp -> Prop :=
adamc@154 234 | VConst : forall b, val (Const b)
adamc@154 235 | VAbs : forall x e, val (Abs x e).
adamc@154 236
adamc@154 237 Hint Constructors val.
adamc@154 238
adamc@154 239 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@154 240
adamc@154 241 Inductive step : exp -> exp -> Prop :=
adamc@154 242 | Beta : forall x e1 e2,
adamc@161 243 val e2
adamc@161 244 -> App (Abs x e1) e2 ==> [x ~> e2] e1
adamc@154 245 | Cong1 : forall e1 e2 e1',
adamc@154 246 e1 ==> e1'
adamc@154 247 -> App e1 e2 ==> App e1' e2
adamc@154 248 | Cong2 : forall e1 e2 e2',
adamc@154 249 val e1
adamc@154 250 -> e2 ==> e2'
adamc@154 251 -> App e1 e2 ==> App e1 e2'
adamc@154 252
adamc@154 253 where "e1 ==> e2" := (step e1 e2).
adamc@154 254
adamc@154 255 Hint Constructors step.
adamc@154 256
adamc@155 257 Lemma progress' : forall G e t, G |-e e : t
adamc@154 258 -> G = nil
adamc@154 259 -> val e \/ exists e', e ==> e'.
adamc@154 260 induction 1; crush; eauto;
adamc@154 261 try match goal with
adamc@154 262 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@154 263 end;
adamc@154 264 repeat match goal with
adamc@154 265 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@154 266 end.
adamc@154 267 Qed.
adamc@154 268
adamc@155 269 Theorem progress : forall e t, nil |-e e : t
adamc@155 270 -> val e \/ exists e', e ==> e'.
adamc@155 271 intros; eapply progress'; eauto.
adamc@155 272 Qed.
adamc@155 273
adamc@155 274 Lemma preservation' : forall G e t, G |-e e : t
adamc@154 275 -> G = nil
adamc@154 276 -> forall e', e ==> e'
adamc@155 277 -> nil |-e e' : t.
adamc@154 278 induction 1; inversion 2; crush; eauto;
adamc@154 279 match goal with
adamc@154 280 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
adamc@154 281 end; eauto.
adamc@154 282 Qed.
adamc@154 283
adamc@155 284 Theorem preservation : forall e t, nil |-e e : t
adamc@155 285 -> forall e', e ==> e'
adamc@155 286 -> nil |-e e' : t.
adamc@155 287 intros; eapply preservation'; eauto.
adamc@155 288 Qed.
adamc@155 289
adamc@152 290 End Concrete.
adamc@156 291
adamc@156 292
adamc@156 293 (** * De Bruijn Indices *)
adamc@156 294
adamc@156 295 Module DeBruijn.
adamc@156 296
adamc@156 297 Definition var := nat.
adamc@156 298 Definition var_eq := eq_nat_dec.
adamc@156 299
adamc@156 300 Inductive exp : Set :=
adamc@156 301 | Const : bool -> exp
adamc@156 302 | Var : var -> exp
adamc@156 303 | App : exp -> exp -> exp
adamc@156 304 | Abs : exp -> exp.
adamc@156 305
adamc@156 306 Inductive type : Set :=
adamc@156 307 | Bool : type
adamc@156 308 | Arrow : type -> type -> type.
adamc@156 309
adamc@156 310 Infix "-->" := Arrow (right associativity, at level 60).
adamc@156 311
adamc@156 312 Definition ctx := list type.
adamc@156 313
adamc@156 314 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@156 315
adamc@156 316 Inductive lookup : ctx -> var -> type -> Prop :=
adamc@156 317 | First : forall t G,
adamc@156 318 t :: G |-v O : t
adamc@156 319 | Next : forall x t t' G,
adamc@156 320 G |-v x : t
adamc@156 321 -> t' :: G |-v S x : t
adamc@156 322
adamc@156 323 where "G |-v x : t" := (lookup G x t).
adamc@156 324
adamc@156 325 Hint Constructors lookup.
adamc@156 326
adamc@156 327 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@156 328
adamc@156 329 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@156 330 | TConst : forall G b,
adamc@156 331 G |-e Const b : Bool
adamc@156 332 | TVar : forall G v t,
adamc@156 333 G |-v v : t
adamc@156 334 -> G |-e Var v : t
adamc@156 335 | TApp : forall G e1 e2 dom ran,
adamc@156 336 G |-e e1 : dom --> ran
adamc@156 337 -> G |-e e2 : dom
adamc@156 338 -> G |-e App e1 e2 : ran
adamc@156 339 | TAbs : forall G e' dom ran,
adamc@156 340 dom :: G |-e e' : ran
adamc@156 341 -> G |-e Abs e' : dom --> ran
adamc@156 342
adamc@156 343 where "G |-e e : t" := (hasType G e t).
adamc@156 344
adamc@156 345 Hint Constructors hasType.
adamc@156 346
adamc@156 347 Lemma weaken_lookup : forall G' v t G,
adamc@156 348 G |-v v : t
adamc@156 349 -> G ++ G' |-v v : t.
adamc@156 350 induction 1; crush.
adamc@156 351 Qed.
adamc@156 352
adamc@156 353 Hint Resolve weaken_lookup.
adamc@156 354
adamc@156 355 Theorem weaken_hasType' : forall G' G e t,
adamc@156 356 G |-e e : t
adamc@156 357 -> G ++ G' |-e e : t.
adamc@156 358 induction 1; crush; eauto.
adamc@156 359 Qed.
adamc@156 360
adamc@156 361 Theorem weaken_hasType : forall e t,
adamc@156 362 nil |-e e : t
adamc@156 363 -> forall G', G' |-e e : t.
adamc@156 364 intros; change G' with (nil ++ G');
adamc@156 365 eapply weaken_hasType'; eauto.
adamc@156 366 Qed.
adamc@156 367
adamc@161 368 Hint Resolve weaken_hasType.
adamc@156 369
adamc@156 370 Section subst.
adamc@156 371 Variable e1 : exp.
adamc@156 372
adamc@156 373 Fixpoint subst (x : var) (e2 : exp) : exp :=
adamc@156 374 match e2 with
adamc@156 375 | Const b => Const b
adamc@156 376 | Var x' =>
adamc@156 377 if var_eq x' x
adamc@156 378 then e1
adamc@156 379 else Var x'
adamc@156 380 | App e1 e2 => App (subst x e1) (subst x e2)
adamc@156 381 | Abs e' => Abs (subst (S x) e')
adamc@156 382 end.
adamc@156 383
adamc@156 384 Variable xt : type.
adamc@156 385
adamc@156 386 Lemma subst_eq : forall t G1,
adamc@156 387 G1 ++ xt :: nil |-v length G1 : t
adamc@156 388 -> t = xt.
adamc@156 389 induction G1; inversion 1; crush.
adamc@156 390 Qed.
adamc@156 391
adamc@156 392 Implicit Arguments subst_eq [t G1].
adamc@156 393
adamc@156 394 Lemma subst_eq' : forall t G1 x,
adamc@156 395 G1 ++ xt :: nil |-v x : t
adamc@156 396 -> x <> length G1
adamc@156 397 -> G1 |-v x : t.
adamc@156 398 induction G1; inversion 1; crush;
adamc@156 399 match goal with
adamc@156 400 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@156 401 end.
adamc@156 402 Qed.
adamc@156 403
adamc@156 404 Hint Resolve subst_eq'.
adamc@156 405
adamc@156 406 Lemma subst_neq : forall v t G1,
adamc@156 407 G1 ++ xt :: nil |-v v : t
adamc@156 408 -> v <> length G1
adamc@156 409 -> G1 |-e Var v : t.
adamc@156 410 induction G1; inversion 1; crush.
adamc@156 411 Qed.
adamc@156 412
adamc@156 413 Hint Resolve subst_neq.
adamc@156 414
adamc@156 415 Hypothesis Ht' : nil |-e e1 : xt.
adamc@156 416
adamc@156 417 Lemma hasType_push : forall dom G1 e' ran,
adamc@156 418 dom :: G1 |-e subst (length (dom :: G1)) e' : ran
adamc@156 419 -> dom :: G1 |-e subst (S (length G1)) e' : ran.
adamc@156 420 trivial.
adamc@156 421 Qed.
adamc@156 422
adamc@156 423 Hint Resolve hasType_push.
adamc@156 424
adamc@156 425 Theorem subst_hasType : forall G e2 t,
adamc@156 426 G |-e e2 : t
adamc@156 427 -> forall G1, G = G1 ++ xt :: nil
adamc@156 428 -> G1 |-e subst (length G1) e2 : t.
adamc@156 429 induction 1; crush;
adamc@156 430 try match goal with
adamc@156 431 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@156 432 end; crush; eauto 6;
adamc@156 433 try match goal with
adamc@156 434 | [ H : _ |-v _ : _ |- _ ] =>
adamc@156 435 rewrite (subst_eq H)
adamc@156 436 end; crush.
adamc@156 437 Qed.
adamc@156 438
adamc@156 439 Theorem subst_hasType_closed : forall e2 t,
adamc@156 440 xt :: nil |-e e2 : t
adamc@156 441 -> nil |-e subst O e2 : t.
adamc@156 442 intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
adamc@156 443 Qed.
adamc@156 444 End subst.
adamc@156 445
adamc@156 446 Hint Resolve subst_hasType_closed.
adamc@156 447
adamc@156 448 Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
adamc@156 449
adamc@156 450 Inductive val : exp -> Prop :=
adamc@156 451 | VConst : forall b, val (Const b)
adamc@156 452 | VAbs : forall e, val (Abs e).
adamc@156 453
adamc@156 454 Hint Constructors val.
adamc@156 455
adamc@156 456 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@156 457
adamc@156 458 Inductive step : exp -> exp -> Prop :=
adamc@156 459 | Beta : forall e1 e2,
adamc@161 460 val e2
adamc@161 461 -> App (Abs e1) e2 ==> [O ~> e2] e1
adamc@156 462 | Cong1 : forall e1 e2 e1',
adamc@156 463 e1 ==> e1'
adamc@156 464 -> App e1 e2 ==> App e1' e2
adamc@156 465 | Cong2 : forall e1 e2 e2',
adamc@156 466 val e1
adamc@156 467 -> e2 ==> e2'
adamc@156 468 -> App e1 e2 ==> App e1 e2'
adamc@156 469
adamc@156 470 where "e1 ==> e2" := (step e1 e2).
adamc@156 471
adamc@156 472 Hint Constructors step.
adamc@156 473
adamc@156 474 Lemma progress' : forall G e t, G |-e e : t
adamc@156 475 -> G = nil
adamc@156 476 -> val e \/ exists e', e ==> e'.
adamc@156 477 induction 1; crush; eauto;
adamc@156 478 try match goal with
adamc@156 479 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@156 480 end;
adamc@156 481 repeat match goal with
adamc@156 482 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@156 483 end.
adamc@156 484 Qed.
adamc@156 485
adamc@156 486 Theorem progress : forall e t, nil |-e e : t
adamc@156 487 -> val e \/ exists e', e ==> e'.
adamc@156 488 intros; eapply progress'; eauto.
adamc@156 489 Qed.
adamc@156 490
adamc@156 491 Lemma preservation' : forall G e t, G |-e e : t
adamc@156 492 -> G = nil
adamc@156 493 -> forall e', e ==> e'
adamc@156 494 -> nil |-e e' : t.
adamc@156 495 induction 1; inversion 2; crush; eauto;
adamc@156 496 match goal with
adamc@156 497 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
adamc@156 498 end; eauto.
adamc@156 499 Qed.
adamc@156 500
adamc@156 501 Theorem preservation : forall e t, nil |-e e : t
adamc@156 502 -> forall e', e ==> e'
adamc@156 503 -> nil |-e e' : t.
adamc@156 504 intros; eapply preservation'; eauto.
adamc@156 505 Qed.
adamc@156 506
adamc@156 507 End DeBruijn.