Mercurial > cpdt > repo

annotate src/Firstorder.v @ 314:d5787b70cf48

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Rename Tactics; change 'principal typing' to 'principal types'
author Adam Chlipala <adam@chlipala.net>
date Wed, 07 Sep 2011 13:47:24 -0400
parents 758778c0468c
children
rev   line source
adam@290 1 (* Copyright (c) 2008-2010, 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
adam@314 13 Require Import CpdtTactics.
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
adam@290 53 (** printing --> $\longrightarrow$ *)
adamc@152 54 Infix "-->" := Arrow (right associativity, at level 60).
adamc@152 55
adamc@245 56 (** 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 57
adamc@152 58 Definition ctx := list (var * type).
adamc@152 59
adamc@245 60 (** 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 61
adam@290 62 (** printing |-v $\vdash_\mathsf{v}$ *)
adamc@152 63 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@152 64
adamc@250 65 (** Now we define the judgment itself, for variable typing, using a [where] clause to associate a notation definition. *)
adamc@245 66
adamc@152 67 Inductive lookup : ctx -> var -> type -> Prop :=
adamc@152 68 | First : forall x t G,
adamc@152 69 (x, t) :: G |-v x : t
adamc@152 70 | Next : forall x t x' t' G,
adamc@152 71 x <> x'
adamc@152 72 -> G |-v x : t
adamc@152 73 -> (x', t') :: G |-v x : t
adamc@152 74
adamc@152 75 where "G |-v x : t" := (lookup G x t).
adamc@152 76
adamc@152 77 Hint Constructors lookup.
adamc@152 78
adamc@245 79 (** 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 80
adam@290 81 (** printing |-e $\vdash_\mathsf{e}$ *)
adamc@152 82 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@152 83
adamc@152 84 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@152 85 | TConst : forall G b,
adamc@152 86 G |-e Const b : Bool
adamc@152 87 | TVar : forall G v t,
adamc@152 88 G |-v v : t
adamc@152 89 -> G |-e Var v : t
adamc@152 90 | TApp : forall G e1 e2 dom ran,
adamc@152 91 G |-e e1 : dom --> ran
adamc@152 92 -> G |-e e2 : dom
adamc@152 93 -> G |-e App e1 e2 : ran
adamc@152 94 | TAbs : forall G x e' dom ran,
adamc@152 95 (x, dom) :: G |-e e' : ran
adamc@152 96 -> G |-e Abs x e' : dom --> ran
adamc@152 97
adamc@152 98 where "G |-e e : t" := (hasType G e t).
adamc@152 99
adamc@152 100 Hint Constructors hasType.
adamc@152 101
adamc@245 102 (** It is useful to know that variable lookup results are unchanged by adding extra bindings to the end of a context. *)
adamc@245 103
adamc@155 104 Lemma weaken_lookup : forall x t G' G1,
adamc@155 105 G1 |-v x : t
adamc@155 106 -> G1 ++ G' |-v x : t.
adamc@245 107 induction G1 as [ | [? ?] ? ]; crush;
adamc@152 108 match goal with
adamc@152 109 | [ H : _ |-v _ : _ |- _ ] => inversion H; crush
adamc@152 110 end.
adamc@152 111 Qed.
adamc@152 112
adamc@152 113 Hint Resolve weaken_lookup.
adamc@152 114
adamc@245 115 (** The same property extends to the full typing judgment. *)
adamc@245 116
adamc@152 117 Theorem weaken_hasType' : forall G' G e t,
adamc@152 118 G |-e e : t
adamc@155 119 -> G ++ G' |-e e : t.
adamc@152 120 induction 1; crush; eauto.
adamc@152 121 Qed.
adamc@152 122
adamc@155 123 Theorem weaken_hasType : forall e t,
adamc@155 124 nil |-e e : t
adamc@155 125 -> forall G', G' |-e e : t.
adamc@155 126 intros; change G' with (nil ++ G');
adamc@152 127 eapply weaken_hasType'; eauto.
adamc@152 128 Qed.
adamc@152 129
adamc@161 130 Hint Resolve weaken_hasType.
adamc@152 131
adamc@245 132 (** 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 133
adamc@152 134 Section subst.
adamc@152 135 Variable x : var.
adamc@152 136 Variable e1 : exp.
adamc@152 137
adamc@245 138 (** 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 139
adamc@152 140 Fixpoint subst (e2 : exp) : exp :=
adamc@152 141 match e2 with
adamc@246 142 | Const _ => e2
adamc@246 143 | Var x' => if var_eq x' x then e1 else e2
adamc@152 144 | App e1 e2 => App (subst e1) (subst e2)
adamc@246 145 | Abs x' e' => Abs x' (if var_eq x' x then e' else subst e')
adamc@152 146 end.
adamc@152 147
adamc@245 148 (** 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 149
adamc@152 150 Variable xt : type.
adamc@152 151 Hypothesis Ht' : nil |-e e1 : xt.
adamc@152 152
adamc@245 153 (** It is helpful to establish a notation asserting the freshness of a particular variable in a context. *)
adamc@245 154
adamc@157 155 Notation "x # G" := (forall t' : type, In (x, t') G -> False) (no associativity, at level 90).
adamc@152 156
adamc@245 157 (** To prove type preservation, we will need lemmas proving consequences of variable lookup proofs. *)
adamc@245 158
adamc@157 159 Lemma subst_lookup' : forall x' t,
adamc@152 160 x <> x'
adamc@155 161 -> forall G1, G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 162 -> G1 |-v x' : t.
adamc@245 163 induction G1 as [ | [? ?] ? ]; crush;
adamc@152 164 match goal with
adamc@152 165 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@152 166 end; crush.
adamc@152 167 Qed.
adamc@152 168
adamc@157 169 Hint Resolve subst_lookup'.
adamc@152 170
adamc@157 171 Lemma subst_lookup : forall x' t G1,
adamc@157 172 x' # G1
adamc@155 173 -> G1 ++ (x, xt) :: nil |-v x' : t
adamc@155 174 -> t = xt.
adamc@245 175 induction G1 as [ | [? ?] ? ]; crush; eauto;
adamc@152 176 match goal with
adamc@152 177 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@183 178 end; crush; (elimtype False; eauto;
adamc@183 179 match goal with
adamc@183 180 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@183 181 end)
adamc@183 182 || match goal with
adamc@183 183 | [ H : _ |- _ ] => apply H; crush; eauto
adamc@183 184 end.
adamc@152 185 Qed.
adamc@152 186
adamc@157 187 Implicit Arguments subst_lookup [x' t G1].
adamc@152 188
adamc@245 189 (** Another set of lemmas allows us to remove provably unused variables from the ends of typing contexts. *)
adamc@245 190
adamc@155 191 Lemma shadow_lookup : forall v t t' G1,
adamc@152 192 G1 |-v x : t'
adamc@155 193 -> G1 ++ (x, xt) :: nil |-v v : t
adamc@155 194 -> G1 |-v v : t.
adamc@245 195 induction G1 as [ | [? ?] ? ]; crush;
adamc@152 196 match goal with
adamc@152 197 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@152 198 | [ H1 : _ |-v _ : _, H2 : _ |-v _ : _ |- _ ] =>
adamc@152 199 inversion H1; crush; inversion H2; crush
adamc@152 200 end.
adamc@152 201 Qed.
adamc@152 202
adamc@155 203 Lemma shadow_hasType' : forall G e t,
adamc@152 204 G |-e e : t
adamc@155 205 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@152 206 -> forall t'', G1 |-v x : t''
adamc@155 207 -> G1 |-e e : t.
adamc@152 208 Hint Resolve shadow_lookup.
adamc@152 209
adamc@152 210 induction 1; crush; eauto;
adamc@152 211 match goal with
adamc@245 212 | [ H : (?x0, _) :: _ ++ (?x, _) :: _ |-e _ : _ |- _ ] =>
adamc@152 213 destruct (var_eq x0 x); subst; eauto
adamc@152 214 end.
adamc@155 215 Qed.
adamc@152 216
adamc@155 217 Lemma shadow_hasType : forall G1 e t t'',
adamc@155 218 G1 ++ (x, xt) :: nil |-e e : t
adamc@152 219 -> G1 |-v x : t''
adamc@155 220 -> G1 |-e e : t.
adamc@152 221 intros; eapply shadow_hasType'; eauto.
adamc@152 222 Qed.
adamc@152 223
adamc@152 224 Hint Resolve shadow_hasType.
adamc@152 225
adamc@245 226 (** Disjointness facts may be extended to larger contexts when the appropriate obligations are met. *)
adamc@245 227
adamc@157 228 Lemma disjoint_cons : forall x x' t (G : ctx),
adamc@157 229 x # G
adamc@157 230 -> x' <> x
adamc@157 231 -> x # (x', t) :: G.
adamc@157 232 firstorder;
adamc@157 233 match goal with
adamc@157 234 | [ H : (_, _) = (_, _) |- _ ] => injection H
adamc@157 235 end; crush.
adamc@157 236 Qed.
adamc@157 237
adamc@157 238 Hint Resolve disjoint_cons.
adamc@157 239
adamc@245 240 (** Finally, we arrive at the main theorem about substitution: it preserves typing. *)
adamc@245 241
adamc@152 242 Theorem subst_hasType : forall G e2 t,
adamc@152 243 G |-e e2 : t
adamc@155 244 -> forall G1, G = G1 ++ (x, xt) :: nil
adamc@157 245 -> x # G1
adamc@155 246 -> G1 |-e subst e2 : t.
adamc@152 247 induction 1; crush;
adamc@152 248 try match goal with
adamc@152 249 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@152 250 end; crush; eauto 6;
adamc@152 251 match goal with
adamc@157 252 | [ H1 : x # _, H2 : _ |-v x : _ |- _ ] =>
adamc@157 253 rewrite (subst_lookup H1 H2)
adamc@152 254 end; crush.
adamc@152 255 Qed.
adamc@152 256
adamc@245 257 (** We wrap the last theorem into an easier-to-apply form specialized to closed expressions. *)
adamc@245 258
adamc@152 259 Theorem subst_hasType_closed : forall e2 t,
adamc@152 260 (x, xt) :: nil |-e e2 : t
adamc@152 261 -> nil |-e subst e2 : t.
adamc@155 262 intros; eapply subst_hasType; eauto.
adamc@152 263 Qed.
adamc@152 264 End subst.
adamc@152 265
adamc@154 266 Hint Resolve subst_hasType_closed.
adamc@154 267
adam@290 268 (** A notation for substitution will make the operational semantics easier to read. %The ASCII operator \texttt{\textasciitilde{}>} will afterward be rendered as $\leadsto$.% *)
adamc@245 269
adam@290 270 (** printing ~> $\leadsto$ *)
adamc@154 271 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 80).
adamc@154 272
adamc@245 273 (** To define a call-by-value small-step semantics, we rely on a standard judgment characterizing which expressions are values. *)
adamc@245 274
adamc@154 275 Inductive val : exp -> Prop :=
adamc@154 276 | VConst : forall b, val (Const b)
adamc@154 277 | VAbs : forall x e, val (Abs x e).
adamc@154 278
adamc@154 279 Hint Constructors val.
adamc@154 280
adamc@245 281 (** Now the step relation is easy to define. *)
adamc@245 282
adamc@154 283 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@154 284
adamc@154 285 Inductive step : exp -> exp -> Prop :=
adamc@154 286 | Beta : forall x e1 e2,
adamc@161 287 val e2
adamc@161 288 -> App (Abs x e1) e2 ==> [x ~> e2] e1
adamc@154 289 | Cong1 : forall e1 e2 e1',
adamc@154 290 e1 ==> e1'
adamc@154 291 -> App e1 e2 ==> App e1' e2
adamc@154 292 | Cong2 : forall e1 e2 e2',
adamc@154 293 val e1
adamc@154 294 -> e2 ==> e2'
adamc@154 295 -> App e1 e2 ==> App e1 e2'
adamc@154 296
adamc@154 297 where "e1 ==> e2" := (step e1 e2).
adamc@154 298
adamc@154 299 Hint Constructors step.
adamc@154 300
adam@290 301 (** The progress theorem says that any well-typed expression that is not a value 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 302
adamc@155 303 Lemma progress' : forall G e t, G |-e e : t
adamc@154 304 -> G = nil
adamc@154 305 -> val e \/ exists e', e ==> e'.
adamc@154 306 induction 1; crush; eauto;
adamc@154 307 try match goal with
adamc@154 308 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@154 309 end;
adamc@245 310 match goal with
adamc@245 311 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@245 312 end.
adamc@154 313 Qed.
adamc@154 314
adamc@155 315 Theorem progress : forall e t, nil |-e e : t
adamc@155 316 -> val e \/ exists e', e ==> e'.
adamc@155 317 intros; eapply progress'; eauto.
adamc@155 318 Qed.
adamc@155 319
adamc@245 320 (** A similar pattern works for the preservation theorem, which says that any step of execution preserves an expression's type. *)
adamc@245 321
adamc@155 322 Lemma preservation' : forall G e t, G |-e e : t
adamc@154 323 -> G = nil
adamc@154 324 -> forall e', e ==> e'
adamc@155 325 -> nil |-e e' : t.
adamc@154 326 induction 1; inversion 2; crush; eauto;
adamc@154 327 match goal with
adamc@154 328 | [ H : _ |-e Abs _ _ : _ |- _ ] => inversion H
adamc@154 329 end; eauto.
adamc@154 330 Qed.
adamc@154 331
adamc@155 332 Theorem preservation : forall e t, nil |-e e : t
adamc@155 333 -> forall e', e ==> e'
adamc@155 334 -> nil |-e e' : t.
adamc@155 335 intros; eapply preservation'; eauto.
adamc@155 336 Qed.
adamc@155 337
adamc@152 338 End Concrete.
adamc@156 339
adamc@245 340 (** 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 341
adamc@156 342
adamc@156 343 (** * De Bruijn Indices *)
adamc@156 344
adamc@245 345 (** 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 346
adamc@156 347 Module DeBruijn.
adamc@156 348
adamc@156 349 Definition var := nat.
adamc@156 350 Definition var_eq := eq_nat_dec.
adamc@156 351
adamc@156 352 Inductive exp : Set :=
adamc@156 353 | Const : bool -> exp
adamc@156 354 | Var : var -> exp
adamc@156 355 | App : exp -> exp -> exp
adamc@156 356 | Abs : exp -> exp.
adamc@156 357
adamc@156 358 Inductive type : Set :=
adamc@156 359 | Bool : type
adamc@156 360 | Arrow : type -> type -> type.
adamc@156 361
adamc@156 362 Infix "-->" := Arrow (right associativity, at level 60).
adamc@156 363
adamc@245 364 (** 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 365
adamc@156 366 Definition ctx := list type.
adamc@156 367
adamc@156 368 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@156 369
adamc@156 370 Inductive lookup : ctx -> var -> type -> Prop :=
adamc@156 371 | First : forall t G,
adamc@156 372 t :: G |-v O : t
adamc@156 373 | Next : forall x t t' G,
adamc@156 374 G |-v x : t
adamc@156 375 -> t' :: G |-v S x : t
adamc@156 376
adamc@156 377 where "G |-v x : t" := (lookup G x t).
adamc@156 378
adamc@156 379 Hint Constructors lookup.
adamc@156 380
adamc@156 381 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@156 382
adamc@156 383 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@156 384 | TConst : forall G b,
adamc@156 385 G |-e Const b : Bool
adamc@156 386 | TVar : forall G v t,
adamc@156 387 G |-v v : t
adamc@156 388 -> G |-e Var v : t
adamc@156 389 | TApp : forall G e1 e2 dom ran,
adamc@156 390 G |-e e1 : dom --> ran
adamc@156 391 -> G |-e e2 : dom
adamc@156 392 -> G |-e App e1 e2 : ran
adamc@156 393 | TAbs : forall G e' dom ran,
adamc@156 394 dom :: G |-e e' : ran
adamc@156 395 -> G |-e Abs e' : dom --> ran
adamc@156 396
adamc@156 397 where "G |-e e : t" := (hasType G e t).
adamc@156 398
adamc@245 399 (** 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 400
adamc@156 401 Hint Constructors hasType.
adamc@156 402
adamc@245 403 (** We prove roughly the same weakening theorems as before. *)
adamc@245 404
adamc@156 405 Lemma weaken_lookup : forall G' v t G,
adamc@156 406 G |-v v : t
adamc@156 407 -> G ++ G' |-v v : t.
adamc@156 408 induction 1; crush.
adamc@156 409 Qed.
adamc@156 410
adamc@156 411 Hint Resolve weaken_lookup.
adamc@156 412
adamc@156 413 Theorem weaken_hasType' : forall G' G e t,
adamc@156 414 G |-e e : t
adamc@156 415 -> G ++ G' |-e e : t.
adamc@156 416 induction 1; crush; eauto.
adamc@156 417 Qed.
adamc@156 418
adamc@156 419 Theorem weaken_hasType : forall e t,
adamc@156 420 nil |-e e : t
adamc@156 421 -> forall G', G' |-e e : t.
adamc@156 422 intros; change G' with (nil ++ G');
adamc@156 423 eapply weaken_hasType'; eauto.
adamc@156 424 Qed.
adamc@156 425
adamc@161 426 Hint Resolve weaken_hasType.
adamc@156 427
adamc@156 428 Section subst.
adamc@156 429 Variable e1 : exp.
adamc@156 430
adamc@245 431 (** 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 432
adamc@156 433 Fixpoint subst (x : var) (e2 : exp) : exp :=
adamc@156 434 match e2 with
adamc@246 435 | Const _ => e2
adamc@246 436 | Var x' => if var_eq x' x then e1 else e2
adamc@156 437 | App e1 e2 => App (subst x e1) (subst x e2)
adamc@156 438 | Abs e' => Abs (subst (S x) e')
adamc@156 439 end.
adamc@156 440
adamc@156 441 Variable xt : type.
adamc@156 442
adamc@245 443 (** We prove similar theorems about inversion of variable lookup. *)
adamc@245 444
adamc@156 445 Lemma subst_eq : forall t G1,
adamc@156 446 G1 ++ xt :: nil |-v length G1 : t
adamc@156 447 -> t = xt.
adamc@156 448 induction G1; inversion 1; crush.
adamc@156 449 Qed.
adamc@156 450
adamc@156 451 Implicit Arguments subst_eq [t G1].
adamc@156 452
adam@290 453 Lemma subst_neq' : forall t G1 x,
adamc@156 454 G1 ++ xt :: nil |-v x : t
adamc@156 455 -> x <> length G1
adamc@156 456 -> G1 |-v x : t.
adamc@156 457 induction G1; inversion 1; crush;
adamc@156 458 match goal with
adamc@156 459 | [ H : nil |-v _ : _ |- _ ] => inversion H
adamc@156 460 end.
adamc@156 461 Qed.
adamc@156 462
adam@290 463 Hint Resolve subst_neq'.
adamc@156 464
adamc@156 465 Lemma subst_neq : forall v t G1,
adamc@156 466 G1 ++ xt :: nil |-v v : t
adamc@156 467 -> v <> length G1
adamc@156 468 -> G1 |-e Var v : t.
adamc@156 469 induction G1; inversion 1; crush.
adamc@156 470 Qed.
adamc@156 471
adamc@156 472 Hint Resolve subst_neq.
adamc@156 473
adamc@156 474 Hypothesis Ht' : nil |-e e1 : xt.
adamc@156 475
adamc@245 476 (** The next lemma is included solely to guide [eauto], which will not apply computational equivalences automatically. *)
adamc@245 477
adamc@156 478 Lemma hasType_push : forall dom G1 e' ran,
adamc@156 479 dom :: G1 |-e subst (length (dom :: G1)) e' : ran
adamc@156 480 -> dom :: G1 |-e subst (S (length G1)) e' : ran.
adamc@156 481 trivial.
adamc@156 482 Qed.
adamc@156 483
adamc@156 484 Hint Resolve hasType_push.
adamc@156 485
adamc@245 486 (** Finally, we are ready for the main theorem about substitution and typing. *)
adamc@245 487
adamc@156 488 Theorem subst_hasType : forall G e2 t,
adamc@156 489 G |-e e2 : t
adamc@156 490 -> forall G1, G = G1 ++ xt :: nil
adamc@156 491 -> G1 |-e subst (length G1) e2 : t.
adamc@156 492 induction 1; crush;
adamc@156 493 try match goal with
adamc@156 494 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@156 495 end; crush; eauto 6;
adamc@156 496 try match goal with
adamc@156 497 | [ H : _ |-v _ : _ |- _ ] =>
adamc@156 498 rewrite (subst_eq H)
adamc@156 499 end; crush.
adamc@156 500 Qed.
adamc@156 501
adamc@156 502 Theorem subst_hasType_closed : forall e2 t,
adamc@156 503 xt :: nil |-e e2 : t
adamc@156 504 -> nil |-e subst O e2 : t.
adamc@156 505 intros; change O with (length (@nil type)); eapply subst_hasType; eauto.
adamc@156 506 Qed.
adamc@156 507 End subst.
adamc@156 508
adamc@156 509 Hint Resolve subst_hasType_closed.
adamc@156 510
adamc@245 511 (** We define the operational semantics much as before. *)
adamc@245 512
adamc@156 513 Notation "[ x ~> e1 ] e2" := (subst e1 x e2) (no associativity, at level 80).
adamc@156 514
adamc@156 515 Inductive val : exp -> Prop :=
adamc@156 516 | VConst : forall b, val (Const b)
adamc@156 517 | VAbs : forall e, val (Abs e).
adamc@156 518
adamc@156 519 Hint Constructors val.
adamc@156 520
adamc@156 521 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@156 522
adamc@156 523 Inductive step : exp -> exp -> Prop :=
adamc@156 524 | Beta : forall e1 e2,
adamc@161 525 val e2
adamc@161 526 -> App (Abs e1) e2 ==> [O ~> e2] e1
adamc@156 527 | Cong1 : forall e1 e2 e1',
adamc@156 528 e1 ==> e1'
adamc@156 529 -> App e1 e2 ==> App e1' e2
adamc@156 530 | Cong2 : forall e1 e2 e2',
adamc@156 531 val e1
adamc@156 532 -> e2 ==> e2'
adamc@156 533 -> App e1 e2 ==> App e1 e2'
adamc@156 534
adamc@156 535 where "e1 ==> e2" := (step e1 e2).
adamc@156 536
adamc@156 537 Hint Constructors step.
adamc@156 538
adamc@245 539 (** 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 540
adamc@156 541 Lemma progress' : forall G e t, G |-e e : t
adamc@156 542 -> G = nil
adamc@156 543 -> val e \/ exists e', e ==> e'.
adamc@156 544 induction 1; crush; eauto;
adamc@156 545 try match goal with
adamc@156 546 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@156 547 end;
adamc@156 548 repeat match goal with
adamc@156 549 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@156 550 end.
adamc@156 551 Qed.
adamc@156 552
adamc@156 553 Theorem progress : forall e t, nil |-e e : t
adamc@156 554 -> val e \/ exists e', e ==> e'.
adamc@156 555 intros; eapply progress'; eauto.
adamc@156 556 Qed.
adamc@156 557
adamc@156 558 Lemma preservation' : forall G e t, G |-e e : t
adamc@156 559 -> G = nil
adamc@156 560 -> forall e', e ==> e'
adamc@156 561 -> nil |-e e' : t.
adamc@156 562 induction 1; inversion 2; crush; eauto;
adamc@156 563 match goal with
adamc@156 564 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
adamc@156 565 end; eauto.
adamc@156 566 Qed.
adamc@156 567
adamc@156 568 Theorem preservation : forall e t, nil |-e e : t
adamc@156 569 -> forall e', e ==> e'
adamc@156 570 -> nil |-e e' : t.
adamc@156 571 intros; eapply preservation'; eauto.
adamc@156 572 Qed.
adamc@156 573
adamc@156 574 End DeBruijn.
adamc@246 575
adamc@246 576
adamc@246 577 (** * Locally Nameless Syntax *)
adamc@246 578
adam@290 579 (** 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 580
adamc@249 581 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 582
adam@290 583 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 584
adamc@246 585 Module LocallyNameless.
adamc@246 586
adamc@246 587 Definition free_var := string.
adamc@246 588 Definition bound_var := nat.
adamc@246 589
adamc@246 590 Inductive exp : Set :=
adamc@246 591 | Const : bool -> exp
adamc@246 592 | FreeVar : free_var -> exp
adamc@246 593 | BoundVar : bound_var -> exp
adamc@246 594 | App : exp -> exp -> exp
adamc@246 595 | Abs : exp -> exp.
adamc@246 596
adamc@249 597 (** 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 598
adamc@246 599 Inductive type : Set :=
adamc@246 600 | Bool : type
adamc@246 601 | Arrow : type -> type -> type.
adamc@246 602
adamc@246 603 Infix "-->" := Arrow (right associativity, at level 60).
adamc@246 604
adamc@249 605 (** As typing only depends on types of free variables, our contexts borrow their form from the concrete binding example. *)
adamc@249 606
adamc@246 607 Definition ctx := list (free_var * type).
adamc@246 608
adamc@246 609 Reserved Notation "G |-v x : t" (no associativity, at level 90, x at next level).
adamc@246 610
adamc@246 611 Inductive lookup : ctx -> free_var -> type -> Prop :=
adamc@246 612 | First : forall x t G,
adamc@246 613 (x, t) :: G |-v x : t
adamc@246 614 | Next : forall x t x' t' G,
adamc@246 615 x <> x'
adamc@246 616 -> G |-v x : t
adamc@246 617 -> (x', t') :: G |-v x : t
adamc@246 618
adamc@246 619 where "G |-v x : t" := (lookup G x t).
adamc@246 620
adamc@246 621 Hint Constructors lookup.
adamc@246 622
adam@290 623 (** 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. We implement opening with both the richly-typed natural number equality test [eq_nat_dec] that we have discussed previously and with another standard library function [le_lt_dec], which is an analogous richly-typed test for [<=]. *)
adamc@246 624
adamc@246 625 Section open.
adamc@246 626 Variable x : free_var.
adamc@246 627
adamc@246 628 Fixpoint open (n : bound_var) (e : exp) : exp :=
adamc@246 629 match e with
adamc@246 630 | Const _ => e
adamc@246 631 | FreeVar _ => e
adamc@246 632 | BoundVar n' =>
adamc@246 633 if eq_nat_dec n' n
adamc@246 634 then FreeVar x
adamc@246 635 else if le_lt_dec n' n
adamc@246 636 then e
adamc@246 637 else BoundVar (pred n')
adamc@246 638 | App e1 e2 => App (open n e1) (open n e2)
adamc@246 639 | Abs e1 => Abs (open (S n) e1)
adamc@246 640 end.
adamc@246 641 End open.
adamc@246 642
adamc@249 643 (** 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 644
adamc@247 645 Fixpoint freeVars (e : exp) : list free_var :=
adamc@247 646 match e with
adamc@247 647 | Const _ => nil
adamc@247 648 | FreeVar x => x :: nil
adamc@247 649 | BoundVar _ => nil
adamc@247 650 | App e1 e2 => freeVars e1 ++ freeVars e2
adamc@247 651 | Abs e1 => freeVars e1
adamc@247 652 end.
adamc@246 653
adamc@249 654 (** 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 655
adamc@249 656 Inductive lclosed : nat -> exp -> Prop :=
adamc@249 657 | CConst : forall n b, lclosed n (Const b)
adamc@249 658 | CFreeVar : forall n v, lclosed n (FreeVar v)
adamc@249 659 | CBoundVar : forall n v, v < n -> lclosed n (BoundVar v)
adamc@249 660 | CApp : forall n e1 e2, lclosed n e1 -> lclosed n e2 -> lclosed n (App e1 e2)
adamc@249 661 | CAbs : forall n e1, lclosed (S n) e1 -> lclosed n (Abs e1).
adamc@249 662
adamc@249 663 Hint Constructors lclosed.
adamc@249 664
adamc@249 665 (** Now we are ready to define the typing judgment. *)
adamc@249 666
adamc@249 667 Reserved Notation "G |-e e : t" (no associativity, at level 90, e at next level).
adamc@249 668
adamc@246 669 Inductive hasType : ctx -> exp -> type -> Prop :=
adamc@246 670 | TConst : forall G b,
adamc@246 671 G |-e Const b : Bool
adamc@246 672 | TFreeVar : forall G v t,
adamc@246 673 G |-v v : t
adamc@246 674 -> G |-e FreeVar v : t
adamc@246 675 | TApp : forall G e1 e2 dom ran,
adamc@246 676 G |-e e1 : dom --> ran
adamc@246 677 -> G |-e e2 : dom
adamc@246 678 -> G |-e App e1 e2 : ran
adamc@247 679 | TAbs : forall G e' dom ran L,
adamc@249 680 (forall x, ~ In x L -> (x, dom) :: G |-e open x O e' : ran)
adamc@246 681 -> G |-e Abs e' : dom --> ran
adamc@246 682
adamc@246 683 where "G |-e e : t" := (hasType G e t).
adamc@246 684
adamc@249 685 (** 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 686
adamc@249 687 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 688
adamc@246 689 Hint Constructors hasType.
adamc@246 690
adamc@249 691 (** We prove a standard weakening theorem for typing, adopting a more general form than in the previous sections. *)
adamc@249 692
adamc@247 693 Lemma lookup_push : forall G G' x t x' t',
adamc@247 694 (forall x t, G |-v x : t -> G' |-v x : t)
adamc@247 695 -> (x, t) :: G |-v x' : t'
adamc@247 696 -> (x, t) :: G' |-v x' : t'.
adamc@247 697 inversion 2; crush.
adamc@247 698 Qed.
adamc@246 699
adamc@247 700 Hint Resolve lookup_push.
adamc@247 701
adamc@247 702 Theorem weaken_hasType : forall G e t,
adamc@247 703 G |-e e : t
adamc@247 704 -> forall G', (forall x t, G |-v x : t -> G' |-v x : t)
adamc@247 705 -> G' |-e e : t.
adamc@247 706 induction 1; crush; eauto.
adamc@247 707 Qed.
adamc@247 708
adamc@247 709 Hint Resolve weaken_hasType.
adamc@247 710
adamc@249 711 (** We define a simple extension of [crush] to apply in many of the lemmas that follow. *)
adamc@247 712
adamc@248 713 Ltac ln := crush;
adamc@248 714 repeat (match goal with
adamc@248 715 | [ |- context[if ?E then _ else _] ] => destruct E
adamc@248 716 | [ _ : context[if ?E then _ else _] |- _ ] => destruct E
adamc@248 717 end; crush); eauto.
adamc@249 718
adamc@249 719 (** Two basic properties of local closure will be useful later. *)
adamc@248 720
adamc@247 721 Lemma lclosed_S : forall x e n,
adamc@247 722 lclosed n (open x n e)
adamc@247 723 -> lclosed (S n) e.
adamc@248 724 induction e; inversion 1; ln.
adamc@247 725 Qed.
adamc@247 726
adamc@247 727 Hint Resolve lclosed_S.
adamc@247 728
adamc@247 729 Lemma lclosed_weaken : forall n e,
adamc@247 730 lclosed n e
adamc@247 731 -> forall n', n' >= n
adamc@247 732 -> lclosed n' e.
adamc@246 733 induction 1; crush.
adamc@246 734 Qed.
adamc@246 735
adamc@247 736 Hint Resolve lclosed_weaken.
adamc@247 737 Hint Extern 1 (_ >= _) => omega.
adamc@246 738
adamc@249 739 (** 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 740
adamc@247 741 Open Scope string_scope.
adamc@247 742
adamc@247 743 Fixpoint primes (n : nat) : string :=
adamc@247 744 match n with
adamc@247 745 | O => "x"
adamc@247 746 | S n' => primes n' ++ "'"
adamc@247 747 end.
adamc@247 748
adamc@247 749 Fixpoint sumLengths (L : list free_var) : nat :=
adamc@247 750 match L with
adamc@247 751 | nil => O
adamc@247 752 | x :: L' => String.length x + sumLengths L'
adamc@247 753 end.
adamc@248 754
adamc@247 755 Definition fresh (L : list free_var) := primes (sumLengths L).
adamc@247 756
adamc@249 757 (** A few lemmas suffice to establish the correctness theorem [freshOk] for [fresh]. *)
adamc@249 758
adamc@247 759 Theorem freshOk' : forall x L, String.length x > sumLengths L
adamc@249 760 -> ~ In x L.
adamc@247 761 induction L; crush.
adamc@246 762 Qed.
adamc@246 763
adamc@249 764 Lemma length_app : forall s2 s1,
adamc@249 765 String.length (s1 ++ s2) = String.length s1 + String.length s2.
adamc@247 766 induction s1; crush.
adamc@246 767 Qed.
adamc@246 768
adamc@247 769 Hint Rewrite length_app : cpdt.
adamc@247 770
adamc@247 771 Lemma length_primes : forall n, String.length (primes n) = S n.
adamc@247 772 induction n; crush.
adamc@247 773 Qed.
adamc@247 774
adamc@247 775 Hint Rewrite length_primes : cpdt.
adamc@247 776
adamc@249 777 Theorem freshOk : forall L, ~ In (fresh L) L.
adamc@247 778 intros; apply freshOk'; unfold fresh; crush.
adamc@247 779 Qed.
adamc@247 780
adamc@247 781 Hint Resolve freshOk.
adamc@247 782
adamc@249 783 (** 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 784
adamc@247 785 Lemma hasType_lclosed : forall G e t,
adamc@247 786 G |-e e : t
adamc@247 787 -> lclosed O e.
adamc@247 788 induction 1; eauto.
adamc@247 789 Qed.
adamc@247 790
adamc@249 791 (** An important consequence of local closure is that certain openings are idempotent. *)
adamc@249 792
adamc@247 793 Lemma lclosed_open : forall n e, lclosed n e
adamc@247 794 -> forall x, open x n e = e.
adamc@248 795 induction 1; ln.
adamc@247 796 Qed.
adamc@247 797
adamc@247 798 Hint Resolve lclosed_open hasType_lclosed.
adamc@247 799
adamc@247 800 Open Scope list_scope.
adamc@247 801
adamc@249 802 (** 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 803
adamc@248 804 Lemma In_cons1 : forall T (x x' : T) ls,
adamc@248 805 x = x'
adamc@248 806 -> In x (x' :: ls).
adamc@248 807 crush.
adamc@248 808 Qed.
adamc@248 809
adamc@248 810 Lemma In_cons2 : forall T (x x' : T) ls,
adamc@248 811 In x ls
adamc@248 812 -> In x (x' :: ls).
adamc@248 813 crush.
adamc@248 814 Qed.
adamc@248 815
adamc@247 816 Lemma In_app1 : forall T (x : T) ls2 ls1,
adamc@247 817 In x ls1
adamc@247 818 -> In x (ls1 ++ ls2).
adamc@247 819 induction ls1; crush.
adamc@247 820 Qed.
adamc@247 821
adamc@247 822 Lemma In_app2 : forall T (x : T) ls2 ls1,
adamc@247 823 In x ls2
adamc@247 824 -> In x (ls1 ++ ls2).
adamc@247 825 induction ls1; crush.
adamc@247 826 Qed.
adamc@247 827
adamc@248 828 Lemma freshOk_app1 : forall L1 L2,
adamc@248 829 ~ In (fresh (L1 ++ L2)) L1.
adamc@248 830 intros; generalize (freshOk (L1 ++ L2)); crush.
adamc@248 831 Qed.
adamc@248 832
adamc@248 833 Lemma freshOk_app2 : forall L1 L2,
adamc@248 834 ~ In (fresh (L1 ++ L2)) L2.
adamc@248 835 intros; generalize (freshOk (L1 ++ L2)); crush.
adamc@248 836 Qed.
adamc@248 837
adamc@248 838 Hint Resolve In_cons1 In_cons2 In_app1 In_app2.
adamc@246 839
adamc@249 840 (** 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 841
adamc@246 842 Section subst.
adamc@248 843 Hint Resolve freshOk_app1 freshOk_app2.
adamc@248 844
adamc@246 845 Variable x : free_var.
adamc@246 846 Variable e1 : exp.
adamc@246 847
adamc@246 848 Fixpoint subst (e2 : exp) : exp :=
adamc@246 849 match e2 with
adamc@246 850 | Const _ => e2
adamc@246 851 | FreeVar x' => if string_dec x' x then e1 else e2
adamc@246 852 | BoundVar _ => e2
adamc@246 853 | App e1 e2 => App (subst e1) (subst e2)
adamc@246 854 | Abs e' => Abs (subst e')
adamc@246 855 end.
adamc@247 856
adamc@247 857 Variable xt : type.
adamc@247 858
adamc@249 859 (** 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 860
adamc@247 861 Definition disj x (G : ctx) := In x (map (@fst _ _) G) -> False.
adamc@247 862 Infix "#" := disj (no associativity, at level 90).
adamc@247 863
adamc@248 864 Ltac disj := crush;
adamc@248 865 match goal with
adamc@248 866 | [ _ : _ :: _ = ?G0 ++ _ |- _ ] => destruct G0
adamc@248 867 end; crush; eauto.
adamc@248 868
adamc@249 869 (** Some basic properties of variable lookup will be needed on the road to our usual theorem connecting substitution and typing. *)
adamc@249 870
adamc@247 871 Lemma lookup_disj' : forall t G1,
adamc@247 872 G1 |-v x : t
adamc@247 873 -> forall G, x # G
adamc@247 874 -> G1 = G ++ (x, xt) :: nil
adamc@247 875 -> t = xt.
adamc@248 876 unfold disj; induction 1; disj.
adamc@247 877 Qed.
adamc@247 878
adamc@247 879 Lemma lookup_disj : forall t G,
adamc@247 880 x # G
adamc@247 881 -> G ++ (x, xt) :: nil |-v x : t
adamc@247 882 -> t = xt.
adamc@247 883 intros; eapply lookup_disj'; eauto.
adamc@247 884 Qed.
adamc@247 885
adamc@247 886 Lemma lookup_ne' : forall G1 v t,
adamc@247 887 G1 |-v v : t
adamc@249 888 -> forall G, G1 = G ++ (x, xt) :: nil
adamc@249 889 -> v <> x
adamc@249 890 -> G |-v v : t.
adamc@248 891 induction 1; disj.
adamc@247 892 Qed.
adamc@247 893
adamc@247 894 Lemma lookup_ne : forall G v t,
adamc@247 895 G ++ (x, xt) :: nil |-v v : t
adamc@247 896 -> v <> x
adamc@247 897 -> G |-v v : t.
adamc@247 898 intros; eapply lookup_ne'; eauto.
adamc@247 899 Qed.
adamc@247 900
adamc@247 901 Hint Extern 1 (_ |-e _ : _) =>
adamc@247 902 match goal with
adamc@247 903 | [ H1 : _, H2 : _ |- _ ] => rewrite (lookup_disj H1 H2)
adamc@247 904 end.
adamc@247 905 Hint Resolve lookup_ne.
adamc@247 906
adamc@247 907 Hint Extern 1 (@eq exp _ _) => f_equal.
adamc@247 908
adamc@249 909 (** We need to know that substitution and opening commute under appropriate circumstances. *)
adamc@249 910
adamc@247 911 Lemma open_subst : forall x0 e' n,
adamc@247 912 lclosed n e1
adamc@247 913 -> x <> x0
adamc@247 914 -> open x0 n (subst e') = subst (open x0 n e').
adamc@248 915 induction e'; ln.
adamc@247 916 Qed.
adamc@247 917
adamc@249 918 (** We state a corollary of the last result which will work more smoothly with [eauto]. *)
adamc@249 919
adamc@248 920 Lemma hasType_open_subst : forall G x0 e t,
adamc@248 921 G |-e subst (open x0 0 e) : t
adamc@248 922 -> x <> x0
adamc@248 923 -> lclosed 0 e1
adamc@248 924 -> G |-e open x0 0 (subst e) : t.
adamc@248 925 intros; rewrite open_subst; eauto.
adamc@248 926 Qed.
adamc@248 927
adamc@248 928 Hint Resolve hasType_open_subst.
adamc@247 929
adamc@249 930 (** Another lemma establishes the validity of weakening variable lookup judgments with fresh variables. *)
adamc@249 931
adamc@247 932 Lemma disj_push : forall x0 (t : type) G,
adamc@247 933 x # G
adamc@247 934 -> x <> x0
adamc@247 935 -> x # (x0, t) :: G.
adamc@247 936 unfold disj; crush.
adamc@247 937 Qed.
adamc@247 938
adamc@248 939 Hint Resolve disj_push.
adamc@247 940
adamc@247 941 Lemma lookup_cons : forall x0 dom G x1 t,
adamc@247 942 G |-v x1 : t
adamc@249 943 -> ~ In x0 (map (@fst _ _) G)
adamc@247 944 -> (x0, dom) :: G |-v x1 : t.
adamc@248 945 induction 1; crush;
adamc@247 946 match goal with
adamc@247 947 | [ H : _ |-v _ : _ |- _ ] => inversion H
adamc@247 948 end; crush.
adamc@247 949 Qed.
adamc@247 950
adamc@247 951 Hint Resolve lookup_cons.
adamc@247 952 Hint Unfold disj.
adamc@247 953
adamc@249 954 (** 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 955
adamc@248 956 Lemma TAbs_specialized : forall G e' dom ran L x1,
adamc@249 957 (forall x, ~ In x (x1 :: L ++ map (@fst _ _) G) -> (x, dom) :: G |-e open x O e' : ran)
adamc@248 958 -> G |-e Abs e' : dom --> ran.
adamc@248 959 eauto.
adamc@248 960 Qed.
adamc@248 961
adamc@249 962 (** Now we can prove the main inductive lemma in a manner similar to what worked for concrete binding. *)
adamc@249 963
adamc@247 964 Lemma hasType_subst' : forall G1 e t,
adamc@247 965 G1 |-e e : t
adamc@247 966 -> forall G, G1 = G ++ (x, xt) :: nil
adamc@247 967 -> x # G
adamc@247 968 -> G |-e e1 : xt
adamc@247 969 -> G |-e subst e : t.
adamc@248 970 induction 1; ln;
adamc@248 971 match goal with
adamc@248 972 | [ L : list free_var, _ : ?x # _ |- _ ] =>
adamc@248 973 apply TAbs_specialized with L x; eauto 20
adamc@248 974 end.
adamc@247 975 Qed.
adamc@249 976
adamc@249 977 (** The main theorem about substitution of closed expressions follows easily. *)
adamc@249 978
adamc@247 979 Theorem hasType_subst : forall e t,
adamc@247 980 (x, xt) :: nil |-e e : t
adamc@247 981 -> nil |-e e1 : xt
adamc@247 982 -> nil |-e subst e : t.
adamc@247 983 intros; eapply hasType_subst'; eauto.
adamc@247 984 Qed.
adamc@246 985 End subst.
adamc@246 986
adamc@247 987 Hint Resolve hasType_subst.
adamc@246 988
adamc@249 989 (** We can define the operational semantics in almost the same way as in previous examples. *)
adamc@249 990
adamc@247 991 Notation "[ x ~> e1 ] e2" := (subst x e1 e2) (no associativity, at level 60).
adamc@246 992
adamc@246 993 Inductive val : exp -> Prop :=
adamc@246 994 | VConst : forall b, val (Const b)
adamc@246 995 | VAbs : forall e, val (Abs e).
adamc@246 996
adamc@246 997 Hint Constructors val.
adamc@246 998
adamc@246 999 Reserved Notation "e1 ==> e2" (no associativity, at level 90).
adamc@246 1000
adamc@246 1001 Inductive step : exp -> exp -> Prop :=
adamc@247 1002 | Beta : forall e1 e2 x,
adamc@246 1003 val e2
adamc@249 1004 -> ~ In x (freeVars e1)
adamc@246 1005 -> App (Abs e1) e2 ==> [x ~> e2] (open x O e1)
adamc@246 1006 | Cong1 : forall e1 e2 e1',
adamc@246 1007 e1 ==> e1'
adamc@246 1008 -> App e1 e2 ==> App e1' e2
adamc@246 1009 | Cong2 : forall e1 e2 e2',
adamc@246 1010 val e1
adamc@246 1011 -> e2 ==> e2'
adamc@246 1012 -> App e1 e2 ==> App e1 e2'
adamc@246 1013
adamc@246 1014 where "e1 ==> e2" := (step e1 e2).
adamc@246 1015
adamc@246 1016 Hint Constructors step.
adamc@246 1017
adamc@249 1018 (** 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 1019
adamc@249 1020 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 1021
adamc@246 1022 Lemma progress' : forall G e t, G |-e e : t
adamc@246 1023 -> G = nil
adamc@246 1024 -> val e \/ exists e', e ==> e'.
adamc@246 1025 induction 1; crush; eauto;
adamc@246 1026 try match goal with
adamc@246 1027 | [ H : _ |-e _ : _ --> _ |- _ ] => inversion H
adamc@246 1028 end;
adamc@246 1029 repeat match goal with
adamc@246 1030 | [ H : _ |- _ ] => solve [ inversion H; crush; eauto ]
adamc@246 1031 end.
adamc@246 1032 Qed.
adamc@246 1033
adamc@246 1034 Theorem progress : forall e t, nil |-e e : t
adamc@246 1035 -> val e \/ exists e', e ==> e'.
adamc@246 1036 intros; eapply progress'; eauto.
adamc@246 1037 Qed.
adamc@246 1038
adamc@249 1039 (** 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 1040
adamc@249 1041 Lemma alpha_open : forall x1 x2 e1 e2 n,
adamc@249 1042 ~ In x1 (freeVars e2)
adamc@249 1043 -> ~ In x2 (freeVars e2)
adamc@249 1044 -> [x1 ~> e1](open x1 n e2) = [x2 ~> e1](open x2 n e2).
adamc@249 1045 induction e2; ln.
adamc@249 1046 Qed.
adamc@249 1047
adamc@248 1048 Hint Resolve freshOk_app1 freshOk_app2.
adamc@248 1049
adamc@249 1050 (** Again it is useful to state a direct corollary which is easier to apply in proof search. *)
adamc@249 1051
adamc@248 1052 Lemma hasType_alpha_open : forall G L e0 e2 x t,
adamc@248 1053 ~ In x (freeVars e0)
adamc@248 1054 -> G |-e [fresh (L ++ freeVars e0) ~> e2](open (fresh (L ++ freeVars e0)) 0 e0) : t
adamc@248 1055 -> G |-e [x ~> e2](open x 0 e0) : t.
adamc@248 1056 intros; rewrite (alpha_open x (fresh (L ++ freeVars e0))); auto.
adamc@247 1057 Qed.
adamc@247 1058
adamc@248 1059 Hint Resolve hasType_alpha_open.
adamc@247 1060
adamc@249 1061 (** Now the previous sections' preservation proof scripts finish the job. *)
adamc@249 1062
adamc@247 1063 Lemma preservation' : forall G e t, G |-e e : t
adamc@246 1064 -> G = nil
adamc@246 1065 -> forall e', e ==> e'
adamc@246 1066 -> nil |-e e' : t.
adamc@246 1067 induction 1; inversion 2; crush; eauto;
adamc@246 1068 match goal with
adamc@246 1069 | [ H : _ |-e Abs _ : _ |- _ ] => inversion H
adamc@246 1070 end; eauto.
adamc@246 1071 Qed.
adamc@246 1072
adamc@246 1073 Theorem preservation : forall e t, nil |-e e : t
adamc@246 1074 -> forall e', e ==> e'
adamc@246 1075 -> nil |-e e' : t.
adamc@246 1076 intros; eapply preservation'; eauto.
adamc@247 1077 Qed.
adamc@246 1078
adamc@246 1079 End LocallyNameless.