Mercurial > cpdt > repo

annotate src/Firstorder.v @ 279:fabbc71abd80

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Incorporate PC's comments on InductiveTypes
author Adam Chlipala <adam@chlipala.net>
date Fri, 01 Oct 2010 14:19:20 -0400
parents 76043a960a38
children 758778c0468c
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@250 63 (** Now we define the judgment itself, for variable typing, 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@249 575 (** The most popular Coq syntax encoding today is the %\textit{%#<i>#locally nameless#</i>#%}% style, which has been around for a while but was popularized recently by Aydemir et al., following a methodology summarized in their paper "Engineering Formal Metatheory." #<a href="http://www.cis.upenn.edu/~plclub/oregon08/">#A specialized tutorial by that group#</a>#%\footnote{\url{http://www.cis.upenn.edu/~plclub/oregon08/}}% explains the approach, based on a library. In this section, we will build up all of the necessary ingredients from scratch.
adamc@249 576
adamc@249 577 The one-sentence summary of locally nameless encoding is that we represent free variables as concrete syntax does, and we represent bound variables with de Bruijn indices. Many proofs involve reasoning about terms transplanted into different free variable contexts; concrete encoding of free variables means that, to perform such a transplanting, we need no fix-up operation to adjust de Bruijn indices. At the same time, use of de Bruijn indices for local variables gives us canonical representations of expressions, with respect to the usual convention of alpha-equivalence. This makes many operations, including substitution of open terms in open terms, easier to implement.
adamc@249 578
adamc@249 579 The "Engineering Formal Metatheory" methodology involves a number of subtle design decisions, which we will describe as they appear in the latest version of our running example. *)
adamc@249 580
adamc@246 581 Module LocallyNameless.
adamc@246 582
adamc@246 583 Definition free_var := string.
adamc@246 584 Definition bound_var := nat.
adamc@246 585
adamc@246 586 Inductive exp : Set :=
adamc@246 587 | Const : bool -> exp
adamc@246 588 | FreeVar : free_var -> exp
adamc@246 589 | BoundVar : bound_var -> exp
adamc@246 590 | App : exp -> exp -> exp
adamc@246 591 | Abs : exp -> exp.
adamc@246 592
adamc@249 593 (** Note the different constructors for free vs. bound variables, and note that the lack of a variable annotation on [Abs] nodes is inherited from the de Bruijn convention. *)
adamc@249 594
adamc@246 595 Inductive type : Set :=
adamc@246 596 | Bool : type
adamc@246 597 | Arrow : type -> type -> type.
adamc@246 598
adamc@246 599 Infix "-->" := Arrow (right associativity, at level 60).
adamc@246 600
adamc@249 601 (** As typing only depends on types of free variables, our contexts borrow their form from the concrete binding example. *)
adamc@249 602
adamc@246 603 Definition ctx := list (free_var * type).
adamc@246 604
adamc@246 605 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@246 606
adamc@246 607 Inductive lookup : ctx -> free_var -> type -> Prop :=
adamc@246 608 | First : forall x t G,
adamc@246 609 (x, t) :: G |-v x : t
adamc@246 610 | Next : forall x t x' t' G,
adamc@246 611 x <> x'
adamc@246 612 -> G |-v x : t
adamc@246 613 -> (x', t') :: G |-v x : t
adamc@246 614
adamc@246 615 where "G |-v x : t" := (lookup G x t).
adamc@246 616
adamc@246 617 Hint Constructors lookup.
adamc@246 618
adamc@249 619 (** The first unusual operation we need is %\textit{%#<i>#opening#</i>#%}%, where we replace a particular bound variable with a particular free variable. Whenever we "go under a binder," in the typing judgment or elsewhere, we choose a new free variable to replace the old bound variable of the binder. Opening implements the replacement of one by the other. It is like a specialized version of the substitution function we used for pure de Bruijn terms. *)
adamc@246 620
adamc@246 621 Section open.
adamc@246 622 Variable x : free_var.
adamc@246 623
adamc@246 624 Fixpoint open (n : bound_var) (e : exp) : exp :=
adamc@246 625 match e with
adamc@246 626 | Const _ => e
adamc@246 627 | FreeVar _ => e
adamc@246 628 | BoundVar n' =>
adamc@246 629 if eq_nat_dec n' n
adamc@246 630 then FreeVar x
adamc@246 631 else if le_lt_dec n' n
adamc@246 632 then e
adamc@246 633 else BoundVar (pred n')
adamc@246 634 | App e1 e2 => App (open n e1) (open n e2)
adamc@246 635 | Abs e1 => Abs (open (S n) e1)
adamc@246 636 end.
adamc@246 637 End open.
adamc@246 638
adamc@249 639 (** We will also need to reason about an expression's set of free variables. To keep things simple, we represent sets as lists that may contain duplicates. Note how much easier this operation is to implement than over pure de Bruijn terms, since we do not need to maintain a separate numeric argument that keeps track of how deeply we have descended into the input expression. *)
adamc@249 640
adamc@247 641 Fixpoint freeVars (e : exp) : list free_var :=
adamc@247 642 match e with
adamc@247 643 | Const _ => nil
adamc@247 644 | FreeVar x => x :: nil
adamc@247 645 | BoundVar _ => nil
adamc@247 646 | App e1 e2 => freeVars e1 ++ freeVars e2
adamc@247 647 | Abs e1 => freeVars e1
adamc@247 648 end.
adamc@246 649
adamc@249 650 (** It will be useful to have a well-formedness judgment for our terms. This notion is called %\textit{%#<i>#local closure#</i>#%}%. An expression may be declared to be closed, up to a particular maximum de Bruijn index. *)
adamc@249 651
adamc@249 652 Inductive lclosed : nat -> exp -> Prop :=
adamc@249 653 | CConst : forall n b, lclosed n (Const b)
adamc@249 654 | CFreeVar : forall n v, lclosed n (FreeVar v)
adamc@249 655 | CBoundVar : forall n v, v < n -> lclosed n (BoundVar v)
adamc@249 656 | CApp : forall n e1 e2, lclosed n e1 -> lclosed n e2 -> lclosed n (App e1 e2)
adamc@249 657 | CAbs : forall n e1, lclosed (S n) e1 -> lclosed n (Abs e1).
adamc@249 658
adamc@249 659 Hint Constructors lclosed.
adamc@249 660
adamc@249 661 (** Now we are ready to define the typing judgment. *)
adamc@249 662
adamc@249 663 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@249 664
adamc@246 665 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@246 666 | TConst : forall G b,
adamc@246 667 G |-e Const b : Bool
adamc@246 668 | TFreeVar : forall G v t,
adamc@246 669 G |-v v : t
adamc@246 670 -> G |-e FreeVar v : t
adamc@246 671 | TApp : forall G e1 e2 dom ran,
adamc@246 672 G |-e e1 : dom --> ran
adamc@246 673 -> G |-e e2 : dom
adamc@246 674 -> G |-e App e1 e2 : ran
adamc@247 675 | TAbs : forall G e' dom ran L,
adamc@249 676 (forall x, ~ In x L -> (x, dom) :: G |-e open x O e' : ran)
adamc@246 677 -> G |-e Abs e' : dom --> ran
adamc@246 678
adamc@246 679 where "G |-e e : t" := (hasType G e t).
adamc@246 680
adamc@249 681 (** Compared to the previous versions, only the [TAbs] rule is surprising. The rule uses %\textit{%#<i>#co-finite quantiifcation#</i>#%}%. That is, the premise of the rule quantifies over all [x] values that are not members of a finite set [L]. A proof may choose any value of [L] when applying [TAbs]. An alternate, more intuitive version of the rule would fix [L] to be [freeVars e']. It turns out that the greater flexibility of the rule above simplifies many proofs significantly. This typing judgment may be proved equivalent to the more intuitive version, though we will not carry out the proof here.
adamc@249 682
adamc@249 683 Specifially, what our version of [TAbs] says is that, to prove that [Abs e'] has a function type, we must prove that any opening of [e'] with a variable not in [L] has the proper type. For each [x] choice, we extend the context [G] in the usual way. *)
adamc@249 684
adamc@246 685 Hint Constructors hasType.
adamc@246 686
adamc@249 687 (** We prove a standard weakening theorem for typing, adopting a more general form than in the previous sections. *)
adamc@249 688
adamc@247 689 Lemma lookup_push : forall G G' x t x' t',
adamc@247 690 (forall x t, G |-v x : t -> G' |-v x : t)
adamc@247 691 -> (x, t) :: G |-v x' : t'
adamc@247 692 -> (x, t) :: G' |-v x' : t'.
adamc@247 693 inversion 2; crush.
adamc@247 694 Qed.
adamc@246 695
adamc@247 696 Hint Resolve lookup_push.
adamc@247 697
adamc@247 698 Theorem weaken_hasType : forall G e t,
adamc@247 699 G |-e e : t
adamc@247 700 -> forall G', (forall x t, G |-v x : t -> G' |-v x : t)
adamc@247 701 -> G' |-e e : t.
adamc@247 702 induction 1; crush; eauto.
adamc@247 703 Qed.
adamc@247 704
adamc@247 705 Hint Resolve weaken_hasType.
adamc@247 706
adamc@249 707 (** We define a simple extension of [crush] to apply in many of the lemmas that follow. *)
adamc@247 708
adamc@248 709 Ltac ln := crush;
adamc@248 710 repeat (match goal with
adamc@248 711 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@248 712 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@248 713 end; crush); eauto.
adamc@249 714
adamc@249 715 (** Two basic properties of local closure will be useful later. *)
adamc@248 716
adamc@247 717 Lemma lclosed_S : forall x e n,
adamc@247 718 lclosed n (open x n e)
adamc@247 719 -> lclosed (S n) e.
adamc@248 720 induction e; inversion 1; ln.
adamc@247 721 Qed.
adamc@247 722
adamc@247 723 Hint Resolve lclosed_S.
adamc@247 724
adamc@247 725 Lemma lclosed_weaken : forall n e,
adamc@247 726 lclosed n e
adamc@247 727 -> forall n', n' >= n
adamc@247 728 -> lclosed n' e.
adamc@246 729 induction 1; crush.
adamc@246 730 Qed.
adamc@246 731
adamc@247 732 Hint Resolve lclosed_weaken.
adamc@247 733 Hint Extern 1 (_ >= _) => omega.
adamc@246 734
adamc@249 735 (** To prove some further properties, we need the ability to choose a variable that is disjoint from a particular finite set. We implement a specific choice function [fresh]; its details do not matter, as all we need is the final theorem about it, [freshOk]. Concretely, to choose a variable disjoint from set [L], we sum the lengths of the variable names in [L] and choose a new variable name that is one longer than that sum. This variable can be the string ["x"], followed by a number of primes equal to the sum. *)
adamc@249 736
adamc@247 737 Open Scope string_scope.
adamc@247 738
adamc@247 739 Fixpoint primes (n : nat) : string :=
adamc@247 740 match n with
adamc@247 741 | O => "x"
adamc@247 742 | S n' => primes n' ++ "'"
adamc@247 743 end.
adamc@247 744
adamc@247 745 Fixpoint sumLengths (L : list free_var) : nat :=
adamc@247 746 match L with
adamc@247 747 | nil => O
adamc@247 748 | x :: L' => String.length x + sumLengths L'
adamc@247 749 end.
adamc@248 750
adamc@247 751 Definition fresh (L : list free_var) := primes (sumLengths L).
adamc@247 752
adamc@249 753 (** A few lemmas suffice to establish the correctness theorem [freshOk] for [fresh]. *)
adamc@249 754
adamc@247 755 Theorem freshOk' : forall x L, String.length x > sumLengths L
adamc@249 756 -> ~ In x L.
adamc@247 757 induction L; crush.
adamc@246 758 Qed.
adamc@246 759
adamc@249 760 Lemma length_app : forall s2 s1,
adamc@249 761 String.length (s1 ++ s2) = String.length s1 + String.length s2.
adamc@247 762 induction s1; crush.
adamc@246 763 Qed.
adamc@246 764
adamc@247 765 Hint Rewrite length_app : cpdt.
adamc@247 766
adamc@247 767 Lemma length_primes : forall n, String.length (primes n) = S n.
adamc@247 768 induction n; crush.
adamc@247 769 Qed.
adamc@247 770
adamc@247 771 Hint Rewrite length_primes : cpdt.
adamc@247 772
adamc@249 773 Theorem freshOk : forall L, ~ In (fresh L) L.
adamc@247 774 intros; apply freshOk'; unfold fresh; crush.
adamc@247 775 Qed.
adamc@247 776
adamc@247 777 Hint Resolve freshOk.
adamc@247 778
adamc@249 779 (** Now we can prove that well-typedness implies local closure. [fresh] will be used for us automatically by [eauto] in the [Abs] case, driven by the presence of [freshOk] as a hint. *)
adamc@249 780
adamc@247 781 Lemma hasType_lclosed : forall G e t,
adamc@247 782 G |-e e : t
adamc@247 783 -> lclosed O e.
adamc@247 784 induction 1; eauto.
adamc@247 785 Qed.
adamc@247 786
adamc@249 787 (** An important consequence of local closure is that certain openings are idempotent. *)
adamc@249 788
adamc@247 789 Lemma lclosed_open : forall n e, lclosed n e
adamc@247 790 -> forall x, open x n e = e.
adamc@248 791 induction 1; ln.
adamc@247 792 Qed.
adamc@247 793
adamc@247 794 Hint Resolve lclosed_open hasType_lclosed.
adamc@247 795
adamc@247 796 Open Scope list_scope.
adamc@247 797
adamc@249 798 (** We are now almost ready to get down to the details of substitution. First, we prove six lemmas related to treating lists as sets. *)
adamc@249 799
adamc@248 800 Lemma In_cons1 : forall T (x x' : T) ls,
adamc@248 801 x = x'
adamc@248 802 -> In x (x' :: ls).
adamc@248 803 crush.
adamc@248 804 Qed.
adamc@248 805
adamc@248 806 Lemma In_cons2 : forall T (x x' : T) ls,
adamc@248 807 In x ls
adamc@248 808 -> In x (x' :: ls).
adamc@248 809 crush.
adamc@248 810 Qed.
adamc@248 811
adamc@247 812 Lemma In_app1 : forall T (x : T) ls2 ls1,
adamc@247 813 In x ls1
adamc@247 814 -> In x (ls1 ++ ls2).
adamc@247 815 induction ls1; crush.
adamc@247 816 Qed.
adamc@247 817
adamc@247 818 Lemma In_app2 : forall T (x : T) ls2 ls1,
adamc@247 819 In x ls2
adamc@247 820 -> In x (ls1 ++ ls2).
adamc@247 821 induction ls1; crush.
adamc@247 822 Qed.
adamc@247 823
adamc@248 824 Lemma freshOk_app1 : forall L1 L2,
adamc@248 825 ~ In (fresh (L1 ++ L2)) L1.
adamc@248 826 intros; generalize (freshOk (L1 ++ L2)); crush.
adamc@248 827 Qed.
adamc@248 828
adamc@248 829 Lemma freshOk_app2 : forall L1 L2,
adamc@248 830 ~ In (fresh (L1 ++ L2)) L2.
adamc@248 831 intros; generalize (freshOk (L1 ++ L2)); crush.
adamc@248 832 Qed.
adamc@248 833
adamc@248 834 Hint Resolve In_cons1 In_cons2 In_app1 In_app2.
adamc@246 835
adamc@249 836 (** Now we can define our simplest substitution function yet, thanks to the fact that we only subsitute for free variables, which are distinguished syntactically from bound variables. *)
adamc@249 837
adamc@246 838 Section subst.
adamc@248 839 Hint Resolve freshOk_app1 freshOk_app2.
adamc@248 840
adamc@246 841 Variable x : free_var.
adamc@246 842 Variable e1 : exp.
adamc@246 843
adamc@246 844 Fixpoint subst (e2 : exp) : exp :=
adamc@246 845 match e2 with
adamc@246 846 | Const _ => e2
adamc@246 847 | FreeVar x' => if string_dec x' x then e1 else e2
adamc@246 848 | BoundVar _ => e2
adamc@246 849 | App e1 e2 => App (subst e1) (subst e2)
adamc@246 850 | Abs e' => Abs (subst e')
adamc@246 851 end.
adamc@247 852
adamc@247 853 Variable xt : type.
adamc@247 854
adamc@249 855 (** It comes in handy to define disjointness of a variable and a context differently than in previous examples. We use the standard list function [map], as well as the function [fst] for projecting the first element of a pair. We write [@fst _ _] rather than just [fst] to ask that [fst]'s implicit arguments be instantiated with inferred values. *)
adamc@249 856
adamc@247 857 Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False.
adamc@247 858 Infix "#" := disj (no associativity, at level 90).
adamc@247 859
adamc@248 860 Ltac disj := crush;
adamc@248 861 match goal with
adamc@248 862 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
adamc@248 863 end; crush; eauto.
adamc@248 864
adamc@249 865 (** Some basic properties of variable lookup will be needed on the road to our usual theorem connecting substitution and typing. *)
adamc@249 866
adamc@247 867 Lemma lookup_disj' : forall t G1,
adamc@247 868 G1 |-v x : t
adamc@247 869 -> forall G, x # G
adamc@247 870 -> G1 = G ++ (x, xt) :: nil
adamc@247 871 -> t = xt.
adamc@248 872 unfold disj; induction 1; disj.
adamc@247 873 Qed.
adamc@247 874
adamc@247 875 Lemma lookup_disj : forall t G,
adamc@247 876 x # G
adamc@247 877 -> G ++ (x, xt) :: nil |-v x : t
adamc@247 878 -> t = xt.
adamc@247 879 intros; eapply lookup_disj'; eauto.
adamc@247 880 Qed.
adamc@247 881
adamc@247 882 Lemma lookup_ne' : forall G1 v t,
adamc@247 883 G1 |-v v : t
adamc@249 884 -> forall G, G1 = G ++ (x, xt) :: nil
adamc@249 885 -> v <> x
adamc@249 886 -> G |-v v : t.
adamc@248 887 induction 1; disj.
adamc@247 888 Qed.
adamc@247 889
adamc@247 890 Lemma lookup_ne : forall G v t,
adamc@247 891 G ++ (x, xt) :: nil |-v v : t
adamc@247 892 -> v <> x
adamc@247 893 -> G |-v v : t.
adamc@247 894 intros; eapply lookup_ne'; eauto.
adamc@247 895 Qed.
adamc@247 896
adamc@247 897 Hint Extern 1 (_ |-e _ : _) =>
adamc@247 898 match goal with
adamc@247 899 | [ H1 : _, H2 : _ |- _ ] => rewrite (lookup_disj H1 H2)
adamc@247 900 end.
adamc@247 901 Hint Resolve lookup_ne.
adamc@247 902
adamc@247 903 Hint Extern 1 (@eq exp _ _) => f_equal.
adamc@247 904
adamc@249 905 (** We need to know that substitution and opening commute under appropriate circumstances. *)
adamc@249 906
adamc@247 907 Lemma open_subst : forall x0 e' n,
adamc@247 908 lclosed n e1
adamc@247 909 -> x <> x0
adamc@247 910 -> open x0 n (subst e') = subst (open x0 n e').
adamc@248 911 induction e'; ln.
adamc@247 912 Qed.
adamc@247 913
adamc@249 914 (** We state a corollary of the last result which will work more smoothly with [eauto]. *)
adamc@249 915
adamc@248 916 Lemma hasType_open_subst : forall G x0 e t,
adamc@248 917 G |-e subst (open x0 0 e) : t
adamc@248 918 -> x <> x0
adamc@248 919 -> lclosed 0 e1
adamc@248 920 -> G |-e open x0 0 (subst e) : t.
adamc@248 921 intros; rewrite open_subst; eauto.
adamc@248 922 Qed.
adamc@248 923
adamc@248 924 Hint Resolve hasType_open_subst.
adamc@247 925
adamc@249 926 (** Another lemma establishes the validity of weakening variable lookup judgments with fresh variables. *)
adamc@249 927
adamc@247 928 Lemma disj_push : forall x0 (t : type) G,
adamc@247 929 x # G
adamc@247 930 -> x <> x0
adamc@247 931 -> x # (x0, t) :: G.
adamc@247 932 unfold disj; crush.
adamc@247 933 Qed.
adamc@247 934
adamc@248 935 Hint Resolve disj_push.
adamc@247 936
adamc@247 937 Lemma lookup_cons : forall x0 dom G x1 t,
adamc@247 938 G |-v x1 : t
adamc@249 939 -> ~ In x0 (map (@fst _ _) G)
adamc@247 940 -> (x0, dom) :: G |-v x1 : t.
adamc@248 941 induction 1; crush;
adamc@247 942 match goal with
adamc@247 943 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@247 944 end; crush.
adamc@247 945 Qed.
adamc@247 946
adamc@247 947 Hint Resolve lookup_cons.
adamc@247 948 Hint Unfold disj.
adamc@247 949
adamc@249 950 (** Finally, it is useful to state a version of the [TAbs] rule specialized to the choice of [L] that is useful in our main substitution proof. *)
adamc@249 951
adamc@248 952 Lemma TAbs_specialized : forall G e' dom ran L x1,
adamc@249 953 (forall x, ~ In x (x1 :: L ++ map (@fst _ _) G) -> (x, dom) :: G |-e open x O e' : ran)
adamc@248 954 -> G |-e Abs e' : dom --> ran.
adamc@248 955 eauto.
adamc@248 956 Qed.
adamc@248 957
adamc@249 958 (** Now we can prove the main inductive lemma in a manner similar to what worked for concrete binding. *)
adamc@249 959
adamc@247 960 Lemma hasType_subst' : forall G1 e t,
adamc@247 961 G1 |-e e : t
adamc@247 962 -> forall G, G1 = G ++ (x, xt) :: nil
adamc@247 963 -> x # G
adamc@247 964 -> G |-e e1 : xt
adamc@247 965 -> G |-e subst e : t.
adamc@248 966 induction 1; ln;
adamc@248 967 match goal with
adamc@248 968 | [ L : list free_var, _ : ?x # _ |- _ ] =>
adamc@248 969 apply TAbs_specialized with L x; eauto 20
adamc@248 970 end.
adamc@247 971 Qed.
adamc@249 972
adamc@249 973 (** The main theorem about substitution of closed expressions follows easily. *)
adamc@249 974
adamc@247 975 Theorem hasType_subst : forall e t,
adamc@247 976 (x, xt) :: nil |-e e : t
adamc@247 977 -> nil |-e e1 : xt
adamc@247 978 -> nil |-e subst e : t.
adamc@247 979 intros; eapply hasType_subst'; eauto.
adamc@247 980 Qed.
adamc@246 981 End subst.
adamc@246 982
adamc@247 983 Hint Resolve hasType_subst.
adamc@246 984
adamc@249 985 (** We can define the operational semantics in almost the same way as in previous examples. *)
adamc@249 986
adamc@247 987 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 60).
adamc@246 988
adamc@246 989 Inductive val : exp -> Prop :=
adamc@246 990 | VConst : forall b, val (Const b)
adamc@246 991 | VAbs : forall e, val (Abs e).
adamc@246 992
adamc@246 993 Hint Constructors val.
adamc@246 994
adamc@246 995 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@246 996
adamc@246 997 Inductive step : exp -> exp -> Prop :=
adamc@247 998 | Beta : forall e1 e2 x,
adamc@246 999 val e2
adamc@249 1000 -> ~ In x (freeVars e1)
adamc@246 1001 -> App (Abs e1) e2 ==> [x ~> e2] (open x O e1)
adamc@246 1002 | Cong1 : forall e1 e2 e1',
adamc@246 1003 e1 ==> e1'
adamc@246 1004 -> App e1 e2 ==> App e1' e2
adamc@246 1005 | Cong2 : forall e1 e2 e2',
adamc@246 1006 val e1
adamc@246 1007 -> e2 ==> e2'
adamc@246 1008 -> App e1 e2 ==> App e1 e2'
adamc@246 1009
adamc@246 1010 where "e1 ==> e2" := (step e1 e2).
adamc@246 1011
adamc@246 1012 Hint Constructors step.
adamc@246 1013
adamc@249 1014 (** The only interesting change is that the [Beta] rule requires identifying a fresh variable [x] to use in opening the abstraction body. We could have avoided this by implementing a more general [open] that allows substituting expressions for variables, not just variables for variables, but it simplifies the proofs to have just one general substitution function.
adamc@249 1015
adamc@249 1016 Now we are ready to prove progress and preservation. The same proof script from the last examples suffices to prove progress, though significantly different lemmas are applied for us by [eauto]. *)
adamc@249 1017
adamc@246 1018 Lemma progress' : forall G e t, G |-e e : t
adamc@246 1019 -> G = nil
adamc@246 1020 -> val e \/ exists e', e ==> e'.
adamc@246 1021 induction 1; crush; eauto;
adamc@246 1022 try match goal with
adamc@246 1023 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@246 1024 end;
adamc@246 1025 repeat match goal with
adamc@246 1026 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@246 1027 end.
adamc@246 1028 Qed.
adamc@246 1029
adamc@246 1030 Theorem progress : forall e t, nil |-e e : t
adamc@246 1031 -> val e \/ exists e', e ==> e'.
adamc@246 1032 intros; eapply progress'; eauto.
adamc@246 1033 Qed.
adamc@246 1034
adamc@249 1035 (** To establish preservation, it is useful to formalize a principle of sound alpha-variation. In particular, when we open an expression with a particular variable and then immediately substitute for the same variable, we can replace that variable with any other that is not free in the body of the opened expression. *)
adamc@249 1036
adamc@249 1037 Lemma alpha_open : forall x1 x2 e1 e2 n,
adamc@249 1038 ~ In x1 (freeVars e2)
adamc@249 1039 -> ~ In x2 (freeVars e2)
adamc@249 1040 -> [x1 ~> e1](open x1 n e2) = [x2 ~> e1](open x2 n e2).
adamc@249 1041 induction e2; ln.
adamc@249 1042 Qed.
adamc@249 1043
adamc@248 1044 Hint Resolve freshOk_app1 freshOk_app2.
adamc@248 1045
adamc@249 1046 (** Again it is useful to state a direct corollary which is easier to apply in proof search. *)
adamc@249 1047
adamc@248 1048 Lemma hasType_alpha_open : forall G L e0 e2 x t,
adamc@248 1049 ~ In x (freeVars e0)
adamc@248 1050 -> G |-e [fresh (L ++ freeVars e0) ~> e2](open (fresh (L ++ freeVars e0)) 0 e0) : t
adamc@248 1051 -> G |-e [x ~> e2](open x 0 e0) : t.
adamc@248 1052 intros; rewrite (alpha_open x (fresh (L ++ freeVars e0))); auto.
adamc@247 1053 Qed.
adamc@247 1054
adamc@248 1055 Hint Resolve hasType_alpha_open.
adamc@247 1056
adamc@249 1057 (** Now the previous sections' preservation proof scripts finish the job. *)
adamc@249 1058
adamc@247 1059 Lemma preservation' : forall G e t, G |-e e : t
adamc@246 1060 -> G = nil
adamc@246 1061 -> forall e', e ==> e'
adamc@246 1062 -> nil |-e e' : t.
adamc@246 1063 induction 1; inversion 2; crush; eauto;
adamc@246 1064 match goal with
adamc@246 1065 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
adamc@246 1066 end; eauto.
adamc@246 1067 Qed.
adamc@246 1068
adamc@246 1069 Theorem preservation : forall e t, nil |-e e : t
adamc@246 1070 -> forall e', e ==> e'
adamc@246 1071 -> nil |-e e' : t.
adamc@246 1072 intros; eapply preservation'; eauto.
adamc@247 1073 Qed.
adamc@246 1074
adamc@246 1075 End LocallyNameless.