Mercurial > cpdt > repo

annotate src/Firstorder.v @ 246:cca30734ab40

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