Mercurial > cpdt > repo

annotate src/Firstorder.v @ 245:4b001a611e79

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prose for old part of Firstorder
author Adam Chlipala <adamc@hcoop.net>
date Wed, 09 Dec 2009 15:26:22 -0500
parents 13620dfd5f97
children cca30734ab40
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@152 139 | Const b => Const b
adamc@152 140 | Var x' =>
adamc@152 141 if var_eq x' x
adamc@152 142 then e1
adamc@152 143 else Var x'
adamc@152 144 | App e1 e2 => App (subst e1) (subst e2)
adamc@152 145 | Abs x' e' =>
adamc@152 146 Abs x' (if var_eq x' x
adamc@152 147 then e'
adamc@152 148 else subst e')
adamc@152 149 end.
adamc@152 150
adamc@245 151 (** 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 152
adamc@152 153 Variable xt : type.
adamc@152 154 Hypothesis Ht' : nil |-e e1 : xt.
adamc@152 155
adamc@245 156 (** It is helpful to establish a notation asserting the freshness of a particular variable in a context. *)
adamc@245 157
adamc@157 158 Notation "x # G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
adamc@152 159
adamc@245 160 (** To prove type preservation, we will need lemmas proving consequences of variable lookup proofs. *)
adamc@245 161
adamc@157 162 Lemma subst_lookup' : forall x' t,
adamc@152 163 x <> x'
adamc@155 164 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 165 -> G1 |-v x' : t.
adamc@245 166 induction G1 as [ | [? ?] ? ]; crush;
adamc@152 167 match goal with
adamc@152 168 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@152 169 end; crush.
adamc@152 170 Qed.
adamc@152 171
adamc@157 172 Hint Resolve subst_lookup'.
adamc@152 173
adamc@157 174 Lemma subst_lookup : forall x' t G1,
adamc@157 175 x' # G1
adamc@155 176 -> G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 177 -> t = xt.
adamc@245 178 induction G1 as [ | [? ?] ? ]; crush; eauto;
adamc@152 179 match goal with
adamc@152 180 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@183 181 end; crush; (elimtype False; eauto;
adamc@183 182 match goal with
adamc@183 183 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@183 184 end)
adamc@183 185 || match goal with
adamc@183 186 | [ H : _ |- _ ] => apply H; crush; eauto
adamc@183 187 end.
adamc@152 188 Qed.
adamc@152 189
adamc@157 190 Implicit Arguments subst_lookup [x' t G1].
adamc@152 191
adamc@245 192 (** Another set of lemmas allows us to remove provably unused variables from the ends of typing contexts. *)
adamc@245 193
adamc@155 194 Lemma shadow_lookup : forall v t t' G1,
adamc@152 195 G1 |-v x : t'
adamc@155 196 -> G1 ++ (x, xt) :: nil |-v v : t
adamc@155 197 -> G1 |-v v : t.
adamc@245 198 induction G1 as [ | [? ?] ? ]; crush;
adamc@152 199 match goal with
adamc@152 200 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@152 201 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
adamc@152 202 inversion H1; crush; inversion H2; crush
adamc@152 203 end.
adamc@152 204 Qed.
adamc@152 205
adamc@155 206 Lemma shadow_hasType' : forall G e t,
adamc@152 207 G |-e e : t
adamc@155 208 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@152 209 -> forall t'', G1 |-v x : t''
adamc@155 210 -> G1 |-e e : t.
adamc@152 211 Hint Resolve shadow_lookup.
adamc@152 212
adamc@152 213 induction 1; crush; eauto;
adamc@152 214 match goal with
adamc@245 215 | [ H : (?x0, _) :: _ ++ (?x, _) :: _ |-e _ : _ |- _ ] =>
adamc@152 216 destruct (var_eq x0 x); subst; eauto
adamc@152 217 end.
adamc@155 218 Qed.
adamc@152 219
adamc@155 220 Lemma shadow_hasType : forall G1 e t t'',
adamc@155 221 G1 ++ (x, xt) :: nil |-e e : t
adamc@152 222 -> G1 |-v x : t''
adamc@155 223 -> G1 |-e e : t.
adamc@152 224 intros; eapply shadow_hasType'; eauto.
adamc@152 225 Qed.
adamc@152 226
adamc@152 227 Hint Resolve shadow_hasType.
adamc@152 228
adamc@245 229 (** Disjointness facts may be extended to larger contexts when the appropriate obligations are met. *)
adamc@245 230
adamc@157 231 Lemma disjoint_cons : forall x x' t (G : ctx),
adamc@157 232 x # G
adamc@157 233 -> x' <> x
adamc@157 234 -> x # (x', t) :: G.
adamc@157 235 firstorder;
adamc@157 236 match goal with
adamc@157 237 | [ H : (_, _) = (_, _) |- _ ] => injection H
adamc@157 238 end; crush.
adamc@157 239 Qed.
adamc@157 240
adamc@157 241 Hint Resolve disjoint_cons.
adamc@157 242
adamc@245 243 (** Finally, we arrive at the main theorem about substitution: it preserves typing. *)
adamc@245 244
adamc@152 245 Theorem subst_hasType : forall G e2 t,
adamc@152 246 G |-e e2 : t
adamc@155 247 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@157 248 -> x # G1
adamc@155 249 -> G1 |-e subst e2 : t.
adamc@152 250 induction 1; crush;
adamc@152 251 try match goal with
adamc@152 252 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@152 253 end; crush; eauto 6;
adamc@152 254 match goal with
adamc@157 255 | [ H1 : x # _, H2 : _ |-v x : _ |- _ ] =>
adamc@157 256 rewrite (subst_lookup H1 H2)
adamc@152 257 end; crush.
adamc@152 258 Qed.
adamc@152 259
adamc@245 260 (** We wrap the last theorem into an easier-to-apply form specialized to closed expressions. *)
adamc@245 261
adamc@152 262 Theorem subst_hasType_closed : forall e2 t,
adamc@152 263 (x, xt) :: nil |-e e2 : t
adamc@152 264 -> nil |-e subst e2 : t.
adamc@155 265 intros; eapply subst_hasType; eauto.
adamc@152 266 Qed.
adamc@152 267 End subst.
adamc@152 268
adamc@154 269 Hint Resolve subst_hasType_closed.
adamc@154 270
adamc@245 271 (** A notation for substitution will make the operational semantics easier to read. *)
adamc@245 272
adamc@154 273 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
adamc@154 274
adamc@245 275 (** To define a call-by-value small-step semantics, we rely on a standard judgment characterizing which expressions are values. *)
adamc@245 276
adamc@154 277 Inductive val : exp -> Prop :=
adamc@154 278 | VConst : forall b, val (Const b)
adamc@154 279 | VAbs : forall x e, val (Abs x e).
adamc@154 280
adamc@154 281 Hint Constructors val.
adamc@154 282
adamc@245 283 (** Now the step relation is easy to define. *)
adamc@245 284
adamc@154 285 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@154 286
adamc@154 287 Inductive step : exp -> exp -> Prop :=
adamc@154 288 | Beta : forall x e1 e2,
adamc@161 289 val e2
adamc@161 290 -> App (Abs x e1) e2 ==> [x ~> e2] e1
adamc@154 291 | Cong1 : forall e1 e2 e1',
adamc@154 292 e1 ==> e1'
adamc@154 293 -> App e1 e2 ==> App e1' e2
adamc@154 294 | Cong2 : forall e1 e2 e2',
adamc@154 295 val e1
adamc@154 296 -> e2 ==> e2'
adamc@154 297 -> App e1 e2 ==> App e1 e2'
adamc@154 298
adamc@154 299 where "e1 ==> e2" := (step e1 e2).
adamc@154 300
adamc@154 301 Hint Constructors step.
adamc@154 302
adamc@245 303 (** 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 304
adamc@155 305 Lemma progress' : forall G e t, G |-e e : t
adamc@154 306 -> G = nil
adamc@154 307 -> val e \/ exists e', e ==> e'.
adamc@154 308 induction 1; crush; eauto;
adamc@154 309 try match goal with
adamc@154 310 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@154 311 end;
adamc@245 312 match goal with
adamc@245 313 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@245 314 end.
adamc@154 315 Qed.
adamc@154 316
adamc@155 317 Theorem progress : forall e t, nil |-e e : t
adamc@155 318 -> val e \/ exists e', e ==> e'.
adamc@155 319 intros; eapply progress'; eauto.
adamc@155 320 Qed.
adamc@155 321
adamc@245 322 (** A similar pattern works for the preservation theorem, which says that any step of execution preserves an expression's type. *)
adamc@245 323
adamc@155 324 Lemma preservation' : forall G e t, G |-e e : t
adamc@154 325 -> G = nil
adamc@154 326 -> forall e', e ==> e'
adamc@155 327 -> nil |-e e' : t.
adamc@154 328 induction 1; inversion 2; crush; eauto;
adamc@154 329 match goal with
adamc@154 330 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
adamc@154 331 end; eauto.
adamc@154 332 Qed.
adamc@154 333
adamc@155 334 Theorem preservation : forall e t, nil |-e e : t
adamc@155 335 -> forall e', e ==> e'
adamc@155 336 -> nil |-e e' : t.
adamc@155 337 intros; eapply preservation'; eauto.
adamc@155 338 Qed.
adamc@155 339
adamc@152 340 End Concrete.
adamc@156 341
adamc@245 342 (** 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 343
adamc@156 344
adamc@156 345 (** * De Bruijn Indices *)
adamc@156 346
adamc@245 347 (** 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 348
adamc@156 349 Module DeBruijn.
adamc@156 350
adamc@156 351 Definition var := nat.
adamc@156 352 Definition var_eq := eq_nat_dec.
adamc@156 353
adamc@156 354 Inductive exp : Set :=
adamc@156 355 | Const : bool -> exp
adamc@156 356 | Var : var -> exp
adamc@156 357 | App : exp -> exp -> exp
adamc@156 358 | Abs : exp -> exp.
adamc@156 359
adamc@156 360 Inductive type : Set :=
adamc@156 361 | Bool : type
adamc@156 362 | Arrow : type -> type -> type.
adamc@156 363
adamc@156 364 Infix "-->" := Arrow (right associativity, at level 60).
adamc@156 365
adamc@245 366 (** 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 367
adamc@156 368 Definition ctx := list type.
adamc@156 369
adamc@156 370 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@156 371
adamc@156 372 Inductive lookup : ctx -> var -> type -> Prop :=
adamc@156 373 | First : forall t G,
adamc@156 374 t :: G |-v O : t
adamc@156 375 | Next : forall x t t' G,
adamc@156 376 G |-v x : t
adamc@156 377 -> t' :: G |-v S x : t
adamc@156 378
adamc@156 379 where "G |-v x : t" := (lookup G x t).
adamc@156 380
adamc@156 381 Hint Constructors lookup.
adamc@156 382
adamc@156 383 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@156 384
adamc@156 385 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@156 386 | TConst : forall G b,
adamc@156 387 G |-e Const b : Bool
adamc@156 388 | TVar : forall G v t,
adamc@156 389 G |-v v : t
adamc@156 390 -> G |-e Var v : t
adamc@156 391 | TApp : forall G e1 e2 dom ran,
adamc@156 392 G |-e e1 : dom --> ran
adamc@156 393 -> G |-e e2 : dom
adamc@156 394 -> G |-e App e1 e2 : ran
adamc@156 395 | TAbs : forall G e' dom ran,
adamc@156 396 dom :: G |-e e' : ran
adamc@156 397 -> G |-e Abs e' : dom --> ran
adamc@156 398
adamc@156 399 where "G |-e e : t" := (hasType G e t).
adamc@156 400
adamc@245 401 (** 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 402
adamc@156 403 Hint Constructors hasType.
adamc@156 404
adamc@245 405 (** We prove roughly the same weakening theorems as before. *)
adamc@245 406
adamc@156 407 Lemma weaken_lookup : forall G' v t G,
adamc@156 408 G |-v v : t
adamc@156 409 -> G ++ G' |-v v : t.
adamc@156 410 induction 1; crush.
adamc@156 411 Qed.
adamc@156 412
adamc@156 413 Hint Resolve weaken_lookup.
adamc@156 414
adamc@156 415 Theorem weaken_hasType' : forall G' G e t,
adamc@156 416 G |-e e : t
adamc@156 417 -> G ++ G' |-e e : t.
adamc@156 418 induction 1; crush; eauto.
adamc@156 419 Qed.
adamc@156 420
adamc@156 421 Theorem weaken_hasType : forall e t,
adamc@156 422 nil |-e e : t
adamc@156 423 -> forall G', G' |-e e : t.
adamc@156 424 intros; change G' with (nil ++ G');
adamc@156 425 eapply weaken_hasType'; eauto.
adamc@156 426 Qed.
adamc@156 427
adamc@161 428 Hint Resolve weaken_hasType.
adamc@156 429
adamc@156 430 Section subst.
adamc@156 431 Variable e1 : exp.
adamc@156 432
adamc@245 433 (** 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 434
adamc@156 435 Fixpoint subst (x : var) (e2 : exp) : exp :=
adamc@156 436 match e2 with
adamc@156 437 | Const b => Const b
adamc@156 438 | Var x' =>
adamc@156 439 if var_eq x' x
adamc@156 440 then e1
adamc@156 441 else Var x'
adamc@156 442 | App e1 e2 => App (subst x e1) (subst x e2)
adamc@156 443 | Abs e' => Abs (subst (S x) e')
adamc@156 444 end.
adamc@156 445
adamc@156 446 Variable xt : type.
adamc@156 447
adamc@245 448 (** We prove similar theorems about inversion of variable lookup. *)
adamc@245 449
adamc@156 450 Lemma subst_eq : forall t G1,
adamc@156 451 G1 ++ xt :: nil |-v length G1 : t
adamc@156 452 -> t = xt.
adamc@156 453 induction G1; inversion 1; crush.
adamc@156 454 Qed.
adamc@156 455
adamc@156 456 Implicit Arguments subst_eq [t G1].
adamc@156 457
adamc@156 458 Lemma subst_eq' : forall t G1 x,
adamc@156 459 G1 ++ xt :: nil |-v x : t
adamc@156 460 -> x <> length G1
adamc@156 461 -> G1 |-v x : t.
adamc@156 462 induction G1; inversion 1; crush;
adamc@156 463 match goal with
adamc@156 464 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@156 465 end.
adamc@156 466 Qed.
adamc@156 467
adamc@156 468 Hint Resolve subst_eq'.
adamc@156 469
adamc@156 470 Lemma subst_neq : forall v t G1,
adamc@156 471 G1 ++ xt :: nil |-v v : t
adamc@156 472 -> v <> length G1
adamc@156 473 -> G1 |-e Var v : t.
adamc@156 474 induction G1; inversion 1; crush.
adamc@156 475 Qed.
adamc@156 476
adamc@156 477 Hint Resolve subst_neq.
adamc@156 478
adamc@156 479 Hypothesis Ht' : nil |-e e1 : xt.
adamc@156 480
adamc@245 481 (** The next lemma is included solely to guide [eauto], which will not apply computational equivalences automatically. *)
adamc@245 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@245 491 (** Finally, we are ready for the main theorem about substitution and typing. *)
adamc@245 492
adamc@156 493 Theorem subst_hasType : forall G e2 t,
adamc@156 494 G |-e e2 : t
adamc@156 495 -> forall G1, G = G1 ++ xt :: nil
adamc@156 496 -> G1 |-e subst (length G1) e2 : t.
adamc@156 497 induction 1; crush;
adamc@156 498 try match goal with
adamc@156 499 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@156 500 end; crush; eauto 6;
adamc@156 501 try match goal with
adamc@156 502 | [ H : _ |-v _ : _ |- _ ] =>
adamc@156 503 rewrite (subst_eq H)
adamc@156 504 end; crush.
adamc@156 505 Qed.
adamc@156 506
adamc@156 507 Theorem subst_hasType_closed : forall e2 t,
adamc@156 508 xt :: nil |-e e2 : t
adamc@156 509 -> nil |-e subst O e2 : t.
adamc@156 510 intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
adamc@156 511 Qed.
adamc@156 512 End subst.
adamc@156 513
adamc@156 514 Hint Resolve subst_hasType_closed.
adamc@156 515
adamc@245 516 (** We define the operational semantics much as before. *)
adamc@245 517
adamc@156 518 Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
adamc@156 519
adamc@156 520 Inductive val : exp -> Prop :=
adamc@156 521 | VConst : forall b, val (Const b)
adamc@156 522 | VAbs : forall e, val (Abs e).
adamc@156 523
adamc@156 524 Hint Constructors val.
adamc@156 525
adamc@156 526 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@156 527
adamc@156 528 Inductive step : exp -> exp -> Prop :=
adamc@156 529 | Beta : forall e1 e2,
adamc@161 530 val e2
adamc@161 531 -> App (Abs e1) e2 ==> [O ~> e2] e1
adamc@156 532 | Cong1 : forall e1 e2 e1',
adamc@156 533 e1 ==> e1'
adamc@156 534 -> App e1 e2 ==> App e1' e2
adamc@156 535 | Cong2 : forall e1 e2 e2',
adamc@156 536 val e1
adamc@156 537 -> e2 ==> e2'
adamc@156 538 -> App e1 e2 ==> App e1 e2'
adamc@156 539
adamc@156 540 where "e1 ==> e2" := (step e1 e2).
adamc@156 541
adamc@156 542 Hint Constructors step.
adamc@156 543
adamc@245 544 (** 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 545
adamc@156 546 Lemma progress' : forall G e t, G |-e e : t
adamc@156 547 -> G = nil
adamc@156 548 -> val e \/ exists e', e ==> e'.
adamc@156 549 induction 1; crush; eauto;
adamc@156 550 try match goal with
adamc@156 551 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@156 552 end;
adamc@156 553 repeat match goal with
adamc@156 554 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@156 555 end.
adamc@156 556 Qed.
adamc@156 557
adamc@156 558 Theorem progress : forall e t, nil |-e e : t
adamc@156 559 -> val e \/ exists e', e ==> e'.
adamc@156 560 intros; eapply progress'; eauto.
adamc@156 561 Qed.
adamc@156 562
adamc@156 563 Lemma preservation' : forall G e t, G |-e e : t
adamc@156 564 -> G = nil
adamc@156 565 -> forall e', e ==> e'
adamc@156 566 -> nil |-e e' : t.
adamc@156 567 induction 1; inversion 2; crush; eauto;
adamc@156 568 match goal with
adamc@156 569 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
adamc@156 570 end; eauto.
adamc@156 571 Qed.
adamc@156 572
adamc@156 573 Theorem preservation : forall e t, nil |-e e : t
adamc@156 574 -> forall e', e ==> e'
adamc@156 575 -> nil |-e e' : t.
adamc@156 576 intros; eapply preservation'; eauto.
adamc@156 577 Qed.
adamc@156 578
adamc@156 579 End DeBruijn.