Mercurial > cpdt > repo

annotate src/Firstorder.v @ 248:8bd90fe41acd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Automated LocallyNameless
author Adam Chlipala <adamc@hcoop.net>
date Fri, 11 Dec 2009 15:00:42 -0500
parents ecfa8eec3852
children 0f45421cae21
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@245 23 (** Many people interested in interactive theorem-proving want to prove theorems about programming languages. That domain also provides a good setting for demonstrating how to apply the ideas from the earlier parts of this book. This part introduces some techniques for encoding the syntax and semantics of programming languages, along with some example proofs designed to be as practical as possible, rather than to illustrate basic Coq technique.
adamc@245 24
adamc@245 25 To prove anything about a language, we must first formalize the language's syntax. We have a broad design space to choose from, and it makes sense to start with the simplest options, so-called %\textit{%#<i>#first-order#</i>#%}% syntax encodings that do not use dependent types. These encodings are first-order because they do not use Coq function types in a critical way. In this chapter, we consider the most popular first-order encodings, using each to prove a basic type soundness theorem. *)
adamc@152 26
adamc@152 27
adamc@152 28 (** * Concrete Binding *)
adamc@152 29
adamc@245 30 (** The most obvious encoding of the syntax of programming languages follows usual context-free grammars literally. We represent variables as strings and include a variable in our AST definition wherever a variable appears in the informal grammar. Concrete binding turns out to involve a surprisingly large amount of menial bookkeeping, especially when we encode higher-order languages with nested binder scopes. This section's example should give a flavor of what is required. *)
adamc@245 31
adamc@152 32 Module Concrete.
adamc@152 33
adamc@245 34 (** We need our variable type and its decidable equality operation. *)
adamc@245 35
adamc@152 36 Definition var := string.
adamc@152 37 Definition var_eq := string_dec.
adamc@152 38
adamc@245 39 (** We will formalize basic simply-typed lambda calculus. The syntax of expressions and types follows what we would write in a context-free grammar. *)
adamc@245 40
adamc@152 41 Inductive exp : Set :=
adamc@152 42 | Const : bool -> exp
adamc@152 43 | Var : var -> exp
adamc@152 44 | App : exp -> exp -> exp
adamc@152 45 | Abs : var -> exp -> exp.
adamc@152 46
adamc@152 47 Inductive type : Set :=
adamc@152 48 | Bool : type
adamc@152 49 | Arrow : type -> type -> type.
adamc@152 50
adamc@245 51 (** It is useful to define a syntax extension that lets us write function types in more standard notation. *)
adamc@245 52
adamc@152 53 Infix "-->" := Arrow (right associativity, at level 60).
adamc@152 54
adamc@245 55 (** Now we turn to a typing judgment. We will need to define it in terms of typing contexts, which we represent as lists of pairs of variables and types. *)
adamc@245 56
adamc@152 57 Definition ctx := list (var * type).
adamc@152 58
adamc@245 59 (** The definitions of our judgments will be prettier if we write them using mixfix syntax. To define a judgment for looking up the type of a variable in a context, we first %\textit{%#</i>#reserve#</i>#%}% a notation for the judgment. Reserved notations enable mutually-recursive definition of a judgment and its notation; in this sense, the reservation is like a forward declaration in C. *)
adamc@245 60
adamc@152 61 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@152 62
adamc@245 63 (** Now we define the judgment itself, using a [where] clause to associate a notation definition. *)
adamc@245 64
adamc@152 65 Inductive lookup : ctx -> var -> type -> Prop :=
adamc@152 66 | First : forall x t G,
adamc@152 67 (x, t) :: G |-v x : t
adamc@152 68 | Next : forall x t x' t' G,
adamc@152 69 x <> x'
adamc@152 70 -> G |-v x : t
adamc@152 71 -> (x', t') :: G |-v x : t
adamc@152 72
adamc@152 73 where "G |-v x : t" := (lookup G x t).
adamc@152 74
adamc@152 75 Hint Constructors lookup.
adamc@152 76
adamc@245 77 (** The same technique applies to defining the main typing judgment. We use an [at next level] clause to cause the argument [e] of the notation to be parsed at a low enough precedence level. *)
adamc@245 78
adamc@152 79 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@152 80
adamc@152 81 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@152 82 | TConst : forall G b,
adamc@152 83 G |-e Const b : Bool
adamc@152 84 | TVar : forall G v t,
adamc@152 85 G |-v v : t
adamc@152 86 -> G |-e Var v : t
adamc@152 87 | TApp : forall G e1 e2 dom ran,
adamc@152 88 G |-e e1 : dom --> ran
adamc@152 89 -> G |-e e2 : dom
adamc@152 90 -> G |-e App e1 e2 : ran
adamc@152 91 | TAbs : forall G x e' dom ran,
adamc@152 92 (x, dom) :: G |-e e' : ran
adamc@152 93 -> G |-e Abs x e' : dom --> ran
adamc@152 94
adamc@152 95 where "G |-e e : t" := (hasType G e t).
adamc@152 96
adamc@152 97 Hint Constructors hasType.
adamc@152 98
adamc@245 99 (** It is useful to know that variable lookup results are unchanged by adding extra bindings to the end of a context. *)
adamc@245 100
adamc@155 101 Lemma weaken_lookup : forall x t G' G1,
adamc@155 102 G1 |-v x : t
adamc@155 103 -> G1 ++ G' |-v x : t.
adamc@245 104 induction G1 as [ | [? ?] ? ]; crush;
adamc@152 105 match goal with
adamc@152 106 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
adamc@152 107 end.
adamc@152 108 Qed.
adamc@152 109
adamc@152 110 Hint Resolve weaken_lookup.
adamc@152 111
adamc@245 112 (** The same property extends to the full typing judgment. *)
adamc@245 113
adamc@152 114 Theorem weaken_hasType' : forall G' G e t,
adamc@152 115 G |-e e : t
adamc@155 116 -> G ++ G' |-e e : t.
adamc@152 117 induction 1; crush; eauto.
adamc@152 118 Qed.
adamc@152 119
adamc@155 120 Theorem weaken_hasType : forall e t,
adamc@155 121 nil |-e e : t
adamc@155 122 -> forall G', G' |-e e : t.
adamc@155 123 intros; change G' with (nil ++ G');
adamc@152 124 eapply weaken_hasType'; eauto.
adamc@152 125 Qed.
adamc@152 126
adamc@161 127 Hint Resolve weaken_hasType.
adamc@152 128
adamc@245 129 (** Much of the inconvenience of first-order encodings comes from the need to treat capture-avoiding substitution explicitly. We must start by defining a substitution function. *)
adamc@245 130
adamc@152 131 Section subst.
adamc@152 132 Variable x : var.
adamc@152 133 Variable e1 : exp.
adamc@152 134
adamc@245 135 (** We are substituting expression [e1] for every free occurrence of [x]. Note that this definition is specialized to the case where [e1] is closed; substitution is substantially more complicated otherwise, potentially involving explicit alpha-variation. Luckily, our example of type safety for a call-by-value semantics only requires this restricted variety of substitution. *)
adamc@245 136
adamc@152 137 Fixpoint subst (e2 : exp) : exp :=
adamc@152 138 match e2 with
adamc@246 139 | Const _ => e2
adamc@246 140 | Var x' => if var_eq x' x then e1 else e2
adamc@152 141 | App e1 e2 => App (subst e1) (subst e2)
adamc@246 142 | Abs x' e' => Abs x' (if var_eq x' x then e' else subst e')
adamc@152 143 end.
adamc@152 144
adamc@245 145 (** We can prove a few theorems about substitution in well-typed terms, where we assume that [e1] is closed and has type [xt]. *)
adamc@245 146
adamc@152 147 Variable xt : type.
adamc@152 148 Hypothesis Ht' : nil |-e e1 : xt.
adamc@152 149
adamc@245 150 (** It is helpful to establish a notation asserting the freshness of a particular variable in a context. *)
adamc@245 151
adamc@157 152 Notation "x # G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
adamc@152 153
adamc@245 154 (** To prove type preservation, we will need lemmas proving consequences of variable lookup proofs. *)
adamc@245 155
adamc@157 156 Lemma subst_lookup' : forall x' t,
adamc@152 157 x <> x'
adamc@155 158 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 159 -> G1 |-v x' : t.
adamc@245 160 induction G1 as [ | [? ?] ? ]; crush;
adamc@152 161 match goal with
adamc@152 162 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@152 163 end; crush.
adamc@152 164 Qed.
adamc@152 165
adamc@157 166 Hint Resolve subst_lookup'.
adamc@152 167
adamc@157 168 Lemma subst_lookup : forall x' t G1,
adamc@157 169 x' # G1
adamc@155 170 -> G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 171 -> t = xt.
adamc@245 172 induction G1 as [ | [? ?] ? ]; crush; eauto;
adamc@152 173 match goal with
adamc@152 174 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@183 175 end; crush; (elimtype False; eauto;
adamc@183 176 match goal with
adamc@183 177 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@183 178 end)
adamc@183 179 || match goal with
adamc@183 180 | [ H : _ |- _ ] => apply H; crush; eauto
adamc@183 181 end.
adamc@152 182 Qed.
adamc@152 183
adamc@157 184 Implicit Arguments subst_lookup [x' t G1].
adamc@152 185
adamc@245 186 (** Another set of lemmas allows us to remove provably unused variables from the ends of typing contexts. *)
adamc@245 187
adamc@155 188 Lemma shadow_lookup : forall v t t' G1,
adamc@152 189 G1 |-v x : t'
adamc@155 190 -> G1 ++ (x, xt) :: nil |-v v : t
adamc@155 191 -> G1 |-v v : t.
adamc@245 192 induction G1 as [ | [? ?] ? ]; crush;
adamc@152 193 match goal with
adamc@152 194 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@152 195 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
adamc@152 196 inversion H1; crush; inversion H2; crush
adamc@152 197 end.
adamc@152 198 Qed.
adamc@152 199
adamc@155 200 Lemma shadow_hasType' : forall G e t,
adamc@152 201 G |-e e : t
adamc@155 202 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@152 203 -> forall t'', G1 |-v x : t''
adamc@155 204 -> G1 |-e e : t.
adamc@152 205 Hint Resolve shadow_lookup.
adamc@152 206
adamc@152 207 induction 1; crush; eauto;
adamc@152 208 match goal with
adamc@245 209 | [ H : (?x0, _) :: _ ++ (?x, _) :: _ |-e _ : _ |- _ ] =>
adamc@152 210 destruct (var_eq x0 x); subst; eauto
adamc@152 211 end.
adamc@155 212 Qed.
adamc@152 213
adamc@155 214 Lemma shadow_hasType : forall G1 e t t'',
adamc@155 215 G1 ++ (x, xt) :: nil |-e e : t
adamc@152 216 -> G1 |-v x : t''
adamc@155 217 -> G1 |-e e : t.
adamc@152 218 intros; eapply shadow_hasType'; eauto.
adamc@152 219 Qed.
adamc@152 220
adamc@152 221 Hint Resolve shadow_hasType.
adamc@152 222
adamc@245 223 (** Disjointness facts may be extended to larger contexts when the appropriate obligations are met. *)
adamc@245 224
adamc@157 225 Lemma disjoint_cons : forall x x' t (G : ctx),
adamc@157 226 x # G
adamc@157 227 -> x' <> x
adamc@157 228 -> x # (x', t) :: G.
adamc@157 229 firstorder;
adamc@157 230 match goal with
adamc@157 231 | [ H : (_, _) = (_, _) |- _ ] => injection H
adamc@157 232 end; crush.
adamc@157 233 Qed.
adamc@157 234
adamc@157 235 Hint Resolve disjoint_cons.
adamc@157 236
adamc@245 237 (** Finally, we arrive at the main theorem about substitution: it preserves typing. *)
adamc@245 238
adamc@152 239 Theorem subst_hasType : forall G e2 t,
adamc@152 240 G |-e e2 : t
adamc@155 241 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@157 242 -> x # G1
adamc@155 243 -> G1 |-e subst e2 : t.
adamc@152 244 induction 1; crush;
adamc@152 245 try match goal with
adamc@152 246 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@152 247 end; crush; eauto 6;
adamc@152 248 match goal with
adamc@157 249 | [ H1 : x # _, H2 : _ |-v x : _ |- _ ] =>
adamc@157 250 rewrite (subst_lookup H1 H2)
adamc@152 251 end; crush.
adamc@152 252 Qed.
adamc@152 253
adamc@245 254 (** We wrap the last theorem into an easier-to-apply form specialized to closed expressions. *)
adamc@245 255
adamc@152 256 Theorem subst_hasType_closed : forall e2 t,
adamc@152 257 (x, xt) :: nil |-e e2 : t
adamc@152 258 -> nil |-e subst e2 : t.
adamc@155 259 intros; eapply subst_hasType; eauto.
adamc@152 260 Qed.
adamc@152 261 End subst.
adamc@152 262
adamc@154 263 Hint Resolve subst_hasType_closed.
adamc@154 264
adamc@245 265 (** A notation for substitution will make the operational semantics easier to read. *)
adamc@245 266
adamc@154 267 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
adamc@154 268
adamc@245 269 (** To define a call-by-value small-step semantics, we rely on a standard judgment characterizing which expressions are values. *)
adamc@245 270
adamc@154 271 Inductive val : exp -> Prop :=
adamc@154 272 | VConst : forall b, val (Const b)
adamc@154 273 | VAbs : forall x e, val (Abs x e).
adamc@154 274
adamc@154 275 Hint Constructors val.
adamc@154 276
adamc@245 277 (** Now the step relation is easy to define. *)
adamc@245 278
adamc@154 279 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@154 280
adamc@154 281 Inductive step : exp -> exp -> Prop :=
adamc@154 282 | Beta : forall x e1 e2,
adamc@161 283 val e2
adamc@161 284 -> App (Abs x e1) e2 ==> [x ~> e2] e1
adamc@154 285 | Cong1 : forall e1 e2 e1',
adamc@154 286 e1 ==> e1'
adamc@154 287 -> App e1 e2 ==> App e1' e2
adamc@154 288 | Cong2 : forall e1 e2 e2',
adamc@154 289 val e1
adamc@154 290 -> e2 ==> e2'
adamc@154 291 -> App e1 e2 ==> App e1 e2'
adamc@154 292
adamc@154 293 where "e1 ==> e2" := (step e1 e2).
adamc@154 294
adamc@154 295 Hint Constructors step.
adamc@154 296
adamc@245 297 (** The progress theorem says that any well-typed expression can take a step. To deal with limitations of the [induction] tactic, we put most of the proof in a lemma whose statement uses the usual trick of introducing extra equality hypotheses. *)
adamc@245 298
adamc@155 299 Lemma progress' : forall G e t, G |-e e : t
adamc@154 300 -> G = nil
adamc@154 301 -> val e \/ exists e', e ==> e'.
adamc@154 302 induction 1; crush; eauto;
adamc@154 303 try match goal with
adamc@154 304 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@154 305 end;
adamc@245 306 match goal with
adamc@245 307 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@245 308 end.
adamc@154 309 Qed.
adamc@154 310
adamc@155 311 Theorem progress : forall e t, nil |-e e : t
adamc@155 312 -> val e \/ exists e', e ==> e'.
adamc@155 313 intros; eapply progress'; eauto.
adamc@155 314 Qed.
adamc@155 315
adamc@245 316 (** A similar pattern works for the preservation theorem, which says that any step of execution preserves an expression's type. *)
adamc@245 317
adamc@155 318 Lemma preservation' : forall G e t, G |-e e : t
adamc@154 319 -> G = nil
adamc@154 320 -> forall e', e ==> e'
adamc@155 321 -> nil |-e e' : t.
adamc@154 322 induction 1; inversion 2; crush; eauto;
adamc@154 323 match goal with
adamc@154 324 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
adamc@154 325 end; eauto.
adamc@154 326 Qed.
adamc@154 327
adamc@155 328 Theorem preservation : forall e t, nil |-e e : t
adamc@155 329 -> forall e', e ==> e'
adamc@155 330 -> nil |-e e' : t.
adamc@155 331 intros; eapply preservation'; eauto.
adamc@155 332 Qed.
adamc@155 333
adamc@152 334 End Concrete.
adamc@156 335
adamc@245 336 (** This was a relatively simple example, giving only a taste of the proof burden associated with concrete syntax. We were helped by the fact that, with call-by-value semantics, we only need to reason about substitution in closed expressions. There was also no need to alpha-vary an expression. *)
adamc@245 337
adamc@156 338
adamc@156 339 (** * De Bruijn Indices *)
adamc@156 340
adamc@245 341 (** De Bruijn indices are much more popular than concrete syntax. This technique provides a %\textit{%#<i>#canonical#</i>#%}% representation of syntax, where any two alpha-equivalent expressions have syntactically equal encodings, removing the need for explicit reasoning about alpha conversion. Variables are represented as natural numbers, where variable [n] denotes a reference to the [n]th closest enclosing binder. Because variable references in effect point to binders, there is no need to label binders, such as function abstraction, with variables. *)
adamc@245 342
adamc@156 343 Module DeBruijn.
adamc@156 344
adamc@156 345 Definition var := nat.
adamc@156 346 Definition var_eq := eq_nat_dec.
adamc@156 347
adamc@156 348 Inductive exp : Set :=
adamc@156 349 | Const : bool -> exp
adamc@156 350 | Var : var -> exp
adamc@156 351 | App : exp -> exp -> exp
adamc@156 352 | Abs : exp -> exp.
adamc@156 353
adamc@156 354 Inductive type : Set :=
adamc@156 355 | Bool : type
adamc@156 356 | Arrow : type -> type -> type.
adamc@156 357
adamc@156 358 Infix "-->" := Arrow (right associativity, at level 60).
adamc@156 359
adamc@245 360 (** The definition of typing proceeds much the same as in the last section. Since variables are numbers, contexts can be simple lists of types. This makes it possible to write the lookup judgment without mentioning inequality of variables. *)
adamc@245 361
adamc@156 362 Definition ctx := list type.
adamc@156 363
adamc@156 364 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@156 365
adamc@156 366 Inductive lookup : ctx -> var -> type -> Prop :=
adamc@156 367 | First : forall t G,
adamc@156 368 t :: G |-v O : t
adamc@156 369 | Next : forall x t t' G,
adamc@156 370 G |-v x : t
adamc@156 371 -> t' :: G |-v S x : t
adamc@156 372
adamc@156 373 where "G |-v x : t" := (lookup G x t).
adamc@156 374
adamc@156 375 Hint Constructors lookup.
adamc@156 376
adamc@156 377 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@156 378
adamc@156 379 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@156 380 | TConst : forall G b,
adamc@156 381 G |-e Const b : Bool
adamc@156 382 | TVar : forall G v t,
adamc@156 383 G |-v v : t
adamc@156 384 -> G |-e Var v : t
adamc@156 385 | TApp : forall G e1 e2 dom ran,
adamc@156 386 G |-e e1 : dom --> ran
adamc@156 387 -> G |-e e2 : dom
adamc@156 388 -> G |-e App e1 e2 : ran
adamc@156 389 | TAbs : forall G e' dom ran,
adamc@156 390 dom :: G |-e e' : ran
adamc@156 391 -> G |-e Abs e' : dom --> ran
adamc@156 392
adamc@156 393 where "G |-e e : t" := (hasType G e t).
adamc@156 394
adamc@245 395 (** In the [hasType] case for function abstraction, there is no need to choose a variable name. We simply push the function domain type onto the context [G]. *)
adamc@245 396
adamc@156 397 Hint Constructors hasType.
adamc@156 398
adamc@245 399 (** We prove roughly the same weakening theorems as before. *)
adamc@245 400
adamc@156 401 Lemma weaken_lookup : forall G' v t G,
adamc@156 402 G |-v v : t
adamc@156 403 -> G ++ G' |-v v : t.
adamc@156 404 induction 1; crush.
adamc@156 405 Qed.
adamc@156 406
adamc@156 407 Hint Resolve weaken_lookup.
adamc@156 408
adamc@156 409 Theorem weaken_hasType' : forall G' G e t,
adamc@156 410 G |-e e : t
adamc@156 411 -> G ++ G' |-e e : t.
adamc@156 412 induction 1; crush; eauto.
adamc@156 413 Qed.
adamc@156 414
adamc@156 415 Theorem weaken_hasType : forall e t,
adamc@156 416 nil |-e e : t
adamc@156 417 -> forall G', G' |-e e : t.
adamc@156 418 intros; change G' with (nil ++ G');
adamc@156 419 eapply weaken_hasType'; eauto.
adamc@156 420 Qed.
adamc@156 421
adamc@161 422 Hint Resolve weaken_hasType.
adamc@156 423
adamc@156 424 Section subst.
adamc@156 425 Variable e1 : exp.
adamc@156 426
adamc@245 427 (** Substitution is easier to define than with concrete syntax. While our old definition needed to use two comparisons for equality of variables, the de Bruijn substitution only needs one comparison. *)
adamc@245 428
adamc@156 429 Fixpoint subst (x : var) (e2 : exp) : exp :=
adamc@156 430 match e2 with
adamc@246 431 | Const _ => e2
adamc@246 432 | Var x' => if var_eq x' x then e1 else e2
adamc@156 433 | App e1 e2 => App (subst x e1) (subst x e2)
adamc@156 434 | Abs e' => Abs (subst (S x) e')
adamc@156 435 end.
adamc@156 436
adamc@156 437 Variable xt : type.
adamc@156 438
adamc@245 439 (** We prove similar theorems about inversion of variable lookup. *)
adamc@245 440
adamc@156 441 Lemma subst_eq : forall t G1,
adamc@156 442 G1 ++ xt :: nil |-v length G1 : t
adamc@156 443 -> t = xt.
adamc@156 444 induction G1; inversion 1; crush.
adamc@156 445 Qed.
adamc@156 446
adamc@156 447 Implicit Arguments subst_eq [t G1].
adamc@156 448
adamc@156 449 Lemma subst_eq' : forall t G1 x,
adamc@156 450 G1 ++ xt :: nil |-v x : t
adamc@156 451 -> x <> length G1
adamc@156 452 -> G1 |-v x : t.
adamc@156 453 induction G1; inversion 1; crush;
adamc@156 454 match goal with
adamc@156 455 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@156 456 end.
adamc@156 457 Qed.
adamc@156 458
adamc@156 459 Hint Resolve subst_eq'.
adamc@156 460
adamc@156 461 Lemma subst_neq : forall v t G1,
adamc@156 462 G1 ++ xt :: nil |-v v : t
adamc@156 463 -> v <> length G1
adamc@156 464 -> G1 |-e Var v : t.
adamc@156 465 induction G1; inversion 1; crush.
adamc@156 466 Qed.
adamc@156 467
adamc@156 468 Hint Resolve subst_neq.
adamc@156 469
adamc@156 470 Hypothesis Ht' : nil |-e e1 : xt.
adamc@156 471
adamc@245 472 (** The next lemma is included solely to guide [eauto], which will not apply computational equivalences automatically. *)
adamc@245 473
adamc@156 474 Lemma hasType_push : forall dom G1 e' ran,
adamc@156 475 dom :: G1 |-e subst (length (dom :: G1)) e' : ran
adamc@156 476 -> dom :: G1 |-e subst (S (length G1)) e' : ran.
adamc@156 477 trivial.
adamc@156 478 Qed.
adamc@156 479
adamc@156 480 Hint Resolve hasType_push.
adamc@156 481
adamc@245 482 (** Finally, we are ready for the main theorem about substitution and typing. *)
adamc@245 483
adamc@156 484 Theorem subst_hasType : forall G e2 t,
adamc@156 485 G |-e e2 : t
adamc@156 486 -> forall G1, G = G1 ++ xt :: nil
adamc@156 487 -> G1 |-e subst (length G1) e2 : t.
adamc@156 488 induction 1; crush;
adamc@156 489 try match goal with
adamc@156 490 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@156 491 end; crush; eauto 6;
adamc@156 492 try match goal with
adamc@156 493 | [ H : _ |-v _ : _ |- _ ] =>
adamc@156 494 rewrite (subst_eq H)
adamc@156 495 end; crush.
adamc@156 496 Qed.
adamc@156 497
adamc@156 498 Theorem subst_hasType_closed : forall e2 t,
adamc@156 499 xt :: nil |-e e2 : t
adamc@156 500 -> nil |-e subst O e2 : t.
adamc@156 501 intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
adamc@156 502 Qed.
adamc@156 503 End subst.
adamc@156 504
adamc@156 505 Hint Resolve subst_hasType_closed.
adamc@156 506
adamc@245 507 (** We define the operational semantics much as before. *)
adamc@245 508
adamc@156 509 Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
adamc@156 510
adamc@156 511 Inductive val : exp -> Prop :=
adamc@156 512 | VConst : forall b, val (Const b)
adamc@156 513 | VAbs : forall e, val (Abs e).
adamc@156 514
adamc@156 515 Hint Constructors val.
adamc@156 516
adamc@156 517 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@156 518
adamc@156 519 Inductive step : exp -> exp -> Prop :=
adamc@156 520 | Beta : forall e1 e2,
adamc@161 521 val e2
adamc@161 522 -> App (Abs e1) e2 ==> [O ~> e2] e1
adamc@156 523 | Cong1 : forall e1 e2 e1',
adamc@156 524 e1 ==> e1'
adamc@156 525 -> App e1 e2 ==> App e1' e2
adamc@156 526 | Cong2 : forall e1 e2 e2',
adamc@156 527 val e1
adamc@156 528 -> e2 ==> e2'
adamc@156 529 -> App e1 e2 ==> App e1 e2'
adamc@156 530
adamc@156 531 where "e1 ==> e2" := (step e1 e2).
adamc@156 532
adamc@156 533 Hint Constructors step.
adamc@156 534
adamc@245 535 (** Since we have added the right hints, the progress and preservation theorem statements and proofs are exactly the same as in the concrete encoding example. *)
adamc@245 536
adamc@156 537 Lemma progress' : forall G e t, G |-e e : t
adamc@156 538 -> G = nil
adamc@156 539 -> val e \/ exists e', e ==> e'.
adamc@156 540 induction 1; crush; eauto;
adamc@156 541 try match goal with
adamc@156 542 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@156 543 end;
adamc@156 544 repeat match goal with
adamc@156 545 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@156 546 end.
adamc@156 547 Qed.
adamc@156 548
adamc@156 549 Theorem progress : forall e t, nil |-e e : t
adamc@156 550 -> val e \/ exists e', e ==> e'.
adamc@156 551 intros; eapply progress'; eauto.
adamc@156 552 Qed.
adamc@156 553
adamc@156 554 Lemma preservation' : forall G e t, G |-e e : t
adamc@156 555 -> G = nil
adamc@156 556 -> forall e', e ==> e'
adamc@156 557 -> nil |-e e' : t.
adamc@156 558 induction 1; inversion 2; crush; eauto;
adamc@156 559 match goal with
adamc@156 560 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
adamc@156 561 end; eauto.
adamc@156 562 Qed.
adamc@156 563
adamc@156 564 Theorem preservation : forall e t, nil |-e e : t
adamc@156 565 -> forall e', e ==> e'
adamc@156 566 -> nil |-e e' : t.
adamc@156 567 intros; eapply preservation'; eauto.
adamc@156 568 Qed.
adamc@156 569
adamc@156 570 End DeBruijn.
adamc@246 571
adamc@246 572
adamc@246 573 (** * Locally Nameless Syntax *)
adamc@246 574
adamc@246 575 Module LocallyNameless.
adamc@246 576
adamc@246 577 Definition free_var := string.
adamc@246 578 Definition bound_var := nat.
adamc@246 579
adamc@246 580 Inductive exp : Set :=
adamc@246 581 | Const : bool -> exp
adamc@246 582 | FreeVar : free_var -> exp
adamc@246 583 | BoundVar : bound_var -> exp
adamc@246 584 | App : exp -> exp -> exp
adamc@246 585 | Abs : exp -> exp.
adamc@246 586
adamc@246 587 Inductive type : Set :=
adamc@246 588 | Bool : type
adamc@246 589 | Arrow : type -> type -> type.
adamc@246 590
adamc@246 591 Infix "-->" := Arrow (right associativity, at level 60).
adamc@246 592
adamc@246 593 Definition ctx := list (free_var * type).
adamc@246 594
adamc@246 595 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@246 596
adamc@246 597 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@246 598
adamc@246 599 Inductive lookup : ctx -> free_var -> type -> Prop :=
adamc@246 600 | First : forall x t G,
adamc@246 601 (x, t) :: G |-v x : t
adamc@246 602 | Next : forall x t x' t' G,
adamc@246 603 x <> x'
adamc@246 604 -> G |-v x : t
adamc@246 605 -> (x', t') :: G |-v x : t
adamc@246 606
adamc@246 607 where "G |-v x : t" := (lookup G x t).
adamc@246 608
adamc@246 609 Hint Constructors lookup.
adamc@246 610
adamc@246 611 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@246 612
adamc@246 613 Section open.
adamc@246 614 Variable x : free_var.
adamc@246 615
adamc@246 616 Fixpoint open (n : bound_var) (e : exp) : exp :=
adamc@246 617 match e with
adamc@246 618 | Const _ => e
adamc@246 619 | FreeVar _ => e
adamc@246 620 | BoundVar n' =>
adamc@246 621 if eq_nat_dec n' n
adamc@246 622 then FreeVar x
adamc@246 623 else if le_lt_dec n' n
adamc@246 624 then e
adamc@246 625 else BoundVar (pred n')
adamc@246 626 | App e1 e2 => App (open n e1) (open n e2)
adamc@246 627 | Abs e1 => Abs (open (S n) e1)
adamc@246 628 end.
adamc@246 629 End open.
adamc@246 630
adamc@247 631 Fixpoint freeVars (e : exp) : list free_var :=
adamc@247 632 match e with
adamc@247 633 | Const _ => nil
adamc@247 634 | FreeVar x => x :: nil
adamc@247 635 | BoundVar _ => nil
adamc@247 636 | App e1 e2 => freeVars e1 ++ freeVars e2
adamc@247 637 | Abs e1 => freeVars e1
adamc@247 638 end.
adamc@246 639
adamc@246 640 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@246 641 | TConst : forall G b,
adamc@246 642 G |-e Const b : Bool
adamc@246 643 | TFreeVar : forall G v t,
adamc@246 644 G |-v v : t
adamc@246 645 -> G |-e FreeVar v : t
adamc@246 646 | TApp : forall G e1 e2 dom ran,
adamc@246 647 G |-e e1 : dom --> ran
adamc@246 648 -> G |-e e2 : dom
adamc@246 649 -> G |-e App e1 e2 : ran
adamc@247 650 | TAbs : forall G e' dom ran L,
adamc@247 651 (forall x, ~In x L -> (x, dom) :: G |-e open x O e' : ran)
adamc@246 652 -> G |-e Abs e' : dom --> ran
adamc@246 653
adamc@246 654 where "G |-e e : t" := (hasType G e t).
adamc@246 655
adamc@246 656 Hint Constructors hasType.
adamc@246 657
adamc@247 658 Lemma lookup_push : forall G G' x t x' t',
adamc@247 659 (forall x t, G |-v x : t -> G' |-v x : t)
adamc@247 660 -> (x, t) :: G |-v x' : t'
adamc@247 661 -> (x, t) :: G' |-v x' : t'.
adamc@247 662 inversion 2; crush.
adamc@247 663 Qed.
adamc@246 664
adamc@247 665 Hint Resolve lookup_push.
adamc@247 666
adamc@247 667 Theorem weaken_hasType : forall G e t,
adamc@247 668 G |-e e : t
adamc@247 669 -> forall G', (forall x t, G |-v x : t -> G' |-v x : t)
adamc@247 670 -> G' |-e e : t.
adamc@247 671 induction 1; crush; eauto.
adamc@247 672 Qed.
adamc@247 673
adamc@247 674 Hint Resolve weaken_hasType.
adamc@247 675
adamc@247 676 Inductive lclosed : nat -> exp -> Prop :=
adamc@247 677 | CConst : forall n b, lclosed n (Const b)
adamc@247 678 | CFreeVar : forall n v, lclosed n (FreeVar v)
adamc@247 679 | CBoundVar : forall n v, v < n -> lclosed n (BoundVar v)
adamc@247 680 | CApp : forall n e1 e2, lclosed n e1 -> lclosed n e2 -> lclosed n (App e1 e2)
adamc@247 681 | CAbs : forall n e1, lclosed (S n) e1 -> lclosed n (Abs e1).
adamc@247 682
adamc@247 683 Hint Constructors lclosed.
adamc@247 684
adamc@248 685 Ltac ln := crush;
adamc@248 686 repeat (match goal with
adamc@248 687 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@248 688 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@248 689 end; crush); eauto.
adamc@248 690
adamc@247 691 Lemma lclosed_S : forall x e n,
adamc@247 692 lclosed n (open x n e)
adamc@247 693 -> lclosed (S n) e.
adamc@248 694 induction e; inversion 1; ln.
adamc@247 695 Qed.
adamc@247 696
adamc@247 697 Hint Resolve lclosed_S.
adamc@247 698
adamc@247 699 Lemma lclosed_weaken : forall n e,
adamc@247 700 lclosed n e
adamc@247 701 -> forall n', n' >= n
adamc@247 702 -> lclosed n' e.
adamc@246 703 induction 1; crush.
adamc@246 704 Qed.
adamc@246 705
adamc@247 706 Hint Resolve lclosed_weaken.
adamc@247 707 Hint Extern 1 (_ >= _) => omega.
adamc@246 708
adamc@247 709 Open Scope string_scope.
adamc@247 710
adamc@247 711 Fixpoint primes (n : nat) : string :=
adamc@247 712 match n with
adamc@247 713 | O => "x"
adamc@247 714 | S n' => primes n' ++ "'"
adamc@247 715 end.
adamc@247 716
adamc@247 717 Fixpoint sumLengths (L : list free_var) : nat :=
adamc@247 718 match L with
adamc@247 719 | nil => O
adamc@247 720 | x :: L' => String.length x + sumLengths L'
adamc@247 721 end.
adamc@248 722
adamc@247 723 Definition fresh (L : list free_var) := primes (sumLengths L).
adamc@247 724
adamc@247 725 Theorem freshOk' : forall x L, String.length x > sumLengths L
adamc@247 726 -> ~In x L.
adamc@247 727 induction L; crush.
adamc@246 728 Qed.
adamc@246 729
adamc@247 730 Lemma length_app : forall s2 s1, String.length (s1 ++ s2) = String.length s1 + String.length s2.
adamc@247 731 induction s1; crush.
adamc@246 732 Qed.
adamc@246 733
adamc@247 734 Hint Rewrite length_app : cpdt.
adamc@247 735
adamc@247 736 Lemma length_primes : forall n, String.length (primes n) = S n.
adamc@247 737 induction n; crush.
adamc@247 738 Qed.
adamc@247 739
adamc@247 740 Hint Rewrite length_primes : cpdt.
adamc@247 741
adamc@247 742 Theorem freshOk : forall L, ~In (fresh L) L.
adamc@247 743 intros; apply freshOk'; unfold fresh; crush.
adamc@247 744 Qed.
adamc@247 745
adamc@247 746 Hint Resolve freshOk.
adamc@247 747
adamc@247 748 Lemma hasType_lclosed : forall G e t,
adamc@247 749 G |-e e : t
adamc@247 750 -> lclosed O e.
adamc@247 751 induction 1; eauto.
adamc@247 752 Qed.
adamc@247 753
adamc@247 754 Lemma lclosed_open : forall n e, lclosed n e
adamc@247 755 -> forall x, open x n e = e.
adamc@248 756 induction 1; ln.
adamc@247 757 Qed.
adamc@247 758
adamc@247 759 Hint Resolve lclosed_open hasType_lclosed.
adamc@247 760
adamc@247 761 Open Scope list_scope.
adamc@247 762
adamc@248 763 Lemma In_cons1 : forall T (x x' : T) ls,
adamc@248 764 x = x'
adamc@248 765 -> In x (x' :: ls).
adamc@248 766 crush.
adamc@248 767 Qed.
adamc@248 768
adamc@248 769 Lemma In_cons2 : forall T (x x' : T) ls,
adamc@248 770 In x ls
adamc@248 771 -> In x (x' :: ls).
adamc@248 772 crush.
adamc@248 773 Qed.
adamc@248 774
adamc@247 775 Lemma In_app1 : forall T (x : T) ls2 ls1,
adamc@247 776 In x ls1
adamc@247 777 -> In x (ls1 ++ ls2).
adamc@247 778 induction ls1; crush.
adamc@247 779 Qed.
adamc@247 780
adamc@247 781 Lemma In_app2 : forall T (x : T) ls2 ls1,
adamc@247 782 In x ls2
adamc@247 783 -> In x (ls1 ++ ls2).
adamc@247 784 induction ls1; crush.
adamc@247 785 Qed.
adamc@247 786
adamc@248 787 Lemma freshOk_app1 : forall L1 L2,
adamc@248 788 ~ In (fresh (L1 ++ L2)) L1.
adamc@248 789 intros; generalize (freshOk (L1 ++ L2)); crush.
adamc@248 790 Qed.
adamc@248 791
adamc@248 792 Lemma freshOk_app2 : forall L1 L2,
adamc@248 793 ~ In (fresh (L1 ++ L2)) L2.
adamc@248 794 intros; generalize (freshOk (L1 ++ L2)); crush.
adamc@248 795 Qed.
adamc@248 796
adamc@248 797 Hint Resolve In_cons1 In_cons2 In_app1 In_app2.
adamc@246 798
adamc@246 799 Section subst.
adamc@248 800 Hint Resolve freshOk_app1 freshOk_app2.
adamc@248 801
adamc@246 802 Variable x : free_var.
adamc@246 803 Variable e1 : exp.
adamc@246 804
adamc@246 805 Fixpoint subst (e2 : exp) : exp :=
adamc@246 806 match e2 with
adamc@246 807 | Const _ => e2
adamc@246 808 | FreeVar x' => if string_dec x' x then e1 else e2
adamc@246 809 | BoundVar _ => e2
adamc@246 810 | App e1 e2 => App (subst e1) (subst e2)
adamc@246 811 | Abs e' => Abs (subst e')
adamc@246 812 end.
adamc@247 813
adamc@247 814 Variable xt : type.
adamc@247 815
adamc@247 816 Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False.
adamc@247 817 Infix "#" := disj (no associativity, at level 90).
adamc@247 818
adamc@248 819 Ltac disj := crush;
adamc@248 820 match goal with
adamc@248 821 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
adamc@248 822 end; crush; eauto.
adamc@248 823
adamc@247 824 Lemma lookup_disj' : forall t G1,
adamc@247 825 G1 |-v x : t
adamc@247 826 -> forall G, x # G
adamc@247 827 -> G1 = G ++ (x, xt) :: nil
adamc@247 828 -> t = xt.
adamc@248 829 unfold disj; induction 1; disj.
adamc@247 830 Qed.
adamc@247 831
adamc@247 832 Lemma lookup_disj : forall t G,
adamc@247 833 x # G
adamc@247 834 -> G ++ (x, xt) :: nil |-v x : t
adamc@247 835 -> t = xt.
adamc@247 836 intros; eapply lookup_disj'; eauto.
adamc@247 837 Qed.
adamc@247 838
adamc@247 839 Lemma lookup_ne' : forall G1 v t,
adamc@247 840 G1 |-v v : t
adamc@247 841 -> forall G, G1 = G ++ (x, xt) :: nil
adamc@247 842 -> v <> x
adamc@247 843 -> G |-v v : t.
adamc@248 844 induction 1; disj.
adamc@247 845 Qed.
adamc@247 846
adamc@247 847 Lemma lookup_ne : forall G v t,
adamc@247 848 G ++ (x, xt) :: nil |-v v : t
adamc@247 849 -> v <> x
adamc@247 850 -> G |-v v : t.
adamc@247 851 intros; eapply lookup_ne'; eauto.
adamc@247 852 Qed.
adamc@247 853
adamc@247 854 Hint Extern 1 (_ |-e _ : _) =>
adamc@247 855 match goal with
adamc@247 856 | [ H1 : _, H2 : _ |- _ ] => rewrite (lookup_disj H1 H2)
adamc@247 857 end.
adamc@247 858 Hint Resolve lookup_ne.
adamc@247 859
adamc@247 860 Hint Extern 1 (@eq exp _ _) => f_equal.
adamc@247 861
adamc@247 862 Lemma open_subst : forall x0 e' n,
adamc@247 863 lclosed n e1
adamc@247 864 -> x <> x0
adamc@247 865 -> open x0 n (subst e') = subst (open x0 n e').
adamc@248 866 induction e'; ln.
adamc@247 867 Qed.
adamc@247 868
adamc@248 869 Lemma hasType_open_subst : forall G x0 e t,
adamc@248 870 G |-e subst (open x0 0 e) : t
adamc@248 871 -> x <> x0
adamc@248 872 -> lclosed 0 e1
adamc@248 873 -> G |-e open x0 0 (subst e) : t.
adamc@248 874 intros; rewrite open_subst; eauto.
adamc@248 875 Qed.
adamc@248 876
adamc@248 877 Hint Resolve hasType_open_subst.
adamc@247 878
adamc@247 879 Lemma disj_push : forall x0 (t : type) G,
adamc@247 880 x # G
adamc@247 881 -> x <> x0
adamc@247 882 -> x # (x0, t) :: G.
adamc@247 883 unfold disj; crush.
adamc@247 884 Qed.
adamc@247 885
adamc@248 886 Hint Resolve disj_push.
adamc@247 887
adamc@247 888 Lemma lookup_cons : forall x0 dom G x1 t,
adamc@247 889 G |-v x1 : t
adamc@248 890 -> ~In x0 (map (@fst _ _) G)
adamc@247 891 -> (x0, dom) :: G |-v x1 : t.
adamc@248 892 induction 1; crush;
adamc@247 893 match goal with
adamc@247 894 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@247 895 end; crush.
adamc@247 896 Qed.
adamc@247 897
adamc@247 898 Hint Resolve lookup_cons.
adamc@247 899 Hint Unfold disj.
adamc@247 900
adamc@248 901 Lemma TAbs_specialized : forall G e' dom ran L x1,
adamc@248 902 (forall x, ~In x (x1 :: L ++ map (@fst _ _) G) -> (x, dom) :: G |-e open x O e' : ran)
adamc@248 903 -> G |-e Abs e' : dom --> ran.
adamc@248 904 eauto.
adamc@248 905 Qed.
adamc@248 906
adamc@247 907 Lemma hasType_subst' : forall G1 e t,
adamc@247 908 G1 |-e e : t
adamc@247 909 -> forall G, G1 = G ++ (x, xt) :: nil
adamc@247 910 -> x # G
adamc@247 911 -> G |-e e1 : xt
adamc@247 912 -> G |-e subst e : t.
adamc@248 913 induction 1; ln;
adamc@248 914 match goal with
adamc@248 915 | [ L : list free_var, _ : ?x # _ |- _ ] =>
adamc@248 916 apply TAbs_specialized with L x; eauto 20
adamc@248 917 end.
adamc@247 918 Qed.
adamc@247 919
adamc@247 920 Theorem hasType_subst : forall e t,
adamc@247 921 (x, xt) :: nil |-e e : t
adamc@247 922 -> nil |-e e1 : xt
adamc@247 923 -> nil |-e subst e : t.
adamc@247 924 intros; eapply hasType_subst'; eauto.
adamc@247 925 Qed.
adamc@246 926 End subst.
adamc@246 927
adamc@247 928 Hint Resolve hasType_subst.
adamc@246 929
adamc@247 930 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 60).
adamc@246 931
adamc@248 932 Lemma alpha_open : forall x1 x2 e1 e2 n,
adamc@248 933 ~In x1 (freeVars e2)
adamc@248 934 -> ~In x2 (freeVars e2)
adamc@248 935 -> [x1 ~> e1](open x1 n e2) = [x2 ~> e1](open x2 n e2).
adamc@248 936 induction e2; crush;
adamc@248 937 repeat (match goal with
adamc@248 938 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@248 939 end; crush).
adamc@248 940 Qed.
adamc@248 941
adamc@246 942 Inductive val : exp -> Prop :=
adamc@246 943 | VConst : forall b, val (Const b)
adamc@246 944 | VAbs : forall e, val (Abs e).
adamc@246 945
adamc@246 946 Hint Constructors val.
adamc@246 947
adamc@246 948 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@246 949
adamc@246 950 Inductive step : exp -> exp -> Prop :=
adamc@247 951 | Beta : forall e1 e2 x,
adamc@246 952 val e2
adamc@247 953 -> ~In x (freeVars e1)
adamc@246 954 -> App (Abs e1) e2 ==> [x ~> e2] (open x O e1)
adamc@246 955 | Cong1 : forall e1 e2 e1',
adamc@246 956 e1 ==> e1'
adamc@246 957 -> App e1 e2 ==> App e1' e2
adamc@246 958 | Cong2 : forall e1 e2 e2',
adamc@246 959 val e1
adamc@246 960 -> e2 ==> e2'
adamc@246 961 -> App e1 e2 ==> App e1 e2'
adamc@246 962
adamc@246 963 where "e1 ==> e2" := (step e1 e2).
adamc@246 964
adamc@246 965 Hint Constructors step.
adamc@246 966
adamc@246 967 Lemma progress' : forall G e t, G |-e e : t
adamc@246 968 -> G = nil
adamc@246 969 -> val e \/ exists e', e ==> e'.
adamc@246 970 induction 1; crush; eauto;
adamc@246 971 try match goal with
adamc@246 972 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@246 973 end;
adamc@246 974 repeat match goal with
adamc@246 975 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@246 976 end.
adamc@246 977 Qed.
adamc@246 978
adamc@246 979 Theorem progress : forall e t, nil |-e e : t
adamc@246 980 -> val e \/ exists e', e ==> e'.
adamc@246 981 intros; eapply progress'; eauto.
adamc@246 982 Qed.
adamc@246 983
adamc@248 984 Hint Resolve freshOk_app1 freshOk_app2.
adamc@248 985
adamc@248 986 Lemma hasType_alpha_open : forall G L e0 e2 x t,
adamc@248 987 ~ In x (freeVars e0)
adamc@248 988 -> G |-e [fresh (L ++ freeVars e0) ~> e2](open (fresh (L ++ freeVars e0)) 0 e0) : t
adamc@248 989 -> G |-e [x ~> e2](open x 0 e0) : t.
adamc@248 990 intros; rewrite (alpha_open x (fresh (L ++ freeVars e0))); auto.
adamc@247 991 Qed.
adamc@247 992
adamc@248 993 Hint Resolve hasType_alpha_open.
adamc@247 994
adamc@247 995 Lemma preservation' : forall G e t, G |-e e : t
adamc@246 996 -> G = nil
adamc@246 997 -> forall e', e ==> e'
adamc@246 998 -> nil |-e e' : t.
adamc@246 999 induction 1; inversion 2; crush; eauto;
adamc@246 1000 match goal with
adamc@246 1001 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
adamc@246 1002 end; eauto.
adamc@246 1003 Qed.
adamc@246 1004
adamc@246 1005 Theorem preservation : forall e t, nil |-e e : t
adamc@246 1006 -> forall e', e ==> e'
adamc@246 1007 -> nil |-e e' : t.
adamc@246 1008 intros; eapply preservation'; eauto.
adamc@247 1009 Qed.
adamc@246 1010
adamc@246 1011 End LocallyNameless.