Mercurial > cpdt > repo

annotate src/Hoas.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 7b38729be069
children
rev   line source
adam@297 1 (* Copyright (c) 2008-2011, Adam Chlipala
adamc@158 2 *
adamc@158 3 * This work is licensed under a
adamc@158 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@158 5 * Unported License.
adamc@158 6 * The license text is available at:
adamc@158 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@158 8 *)
adamc@158 9
adamc@158 10 (* begin hide *)
adam@297 11 Require Import Eqdep String List FunctionalExtensionality.
adamc@158 12
adam@314 13 Require Import CpdtTactics.
adamc@158 14
adamc@158 15 Set Implicit Arguments.
adamc@158 16 (* end hide *)
adamc@158 17
adamc@158 18
adamc@158 19 (** %\chapter{Higher-Order Abstract Syntax}% *)
adamc@158 20
adamc@252 21 (** In many cases, detailed reasoning about variable binders and substitution is a small annoyance; in other cases, it becomes the dominant cost of proving a theorem formally. No matter which of these possibilities prevails, it is clear that it would be very pragmatic to find a way to avoid reasoning about variable identity or freshness. A well-established alternative to first-order encodings is %\textit{%#<i>#higher-order abstract syntax#</i>#%}%, or HOAS. In mechanized theorem-proving, HOAS is most closely associated with the LF meta logic and the tools based on it, including Twelf.
adamc@158 22
adamc@252 23 In this chapter, we will see that HOAS cannot be implemented directly in Coq. However, a few very similar encodings are possible and are in fact very effective in some important domains. *)
adamc@158 24
adamc@252 25
adamc@252 26 (** * Classic HOAS *)
adamc@252 27
adam@292 28 (** The motto of HOAS is simple: represent object language binders using meta language binders. Here, %``%#"#object language#"#%''% refers to the language being formalized, while the meta language is the language in which the formalization is done. Our usual meta language, Coq's Gallina, contains the standard binding facilities of functional programming, making it a promising base for higher-order encodings.
adamc@252 29
adamc@252 30 Recall the concrete encoding of basic untyped lambda calculus expressions. *)
adamc@252 31
adamc@252 32 Inductive uexp : Set :=
adamc@252 33 | UVar : string -> uexp
adamc@252 34 | UApp : uexp -> uexp -> uexp
adamc@252 35 | UAbs : string -> uexp -> uexp.
adamc@252 36
adamc@252 37 (** The explicit presence of variable names forces us to think about issues of freshness and variable capture. The HOAS alternative would look like this. *)
adamc@252 38
adamc@252 39 Reset uexp.
adamc@252 40
adamc@252 41 (** [[
adamc@252 42 Inductive uexp : Set :=
adamc@252 43 | UApp : uexp -> uexp -> uexp
adamc@252 44 | UAbs : (uexp -> uexp) -> uexp.
adamc@252 45
adamc@252 46 ]]
adamc@252 47
adamc@252 48 We have avoided any mention of variables. Instead, we encode the binding done by abstraction using the binding facilities associated with Gallina functions. For instance, we might represent the term $\lambda x. \; x \; x$#<tt>\x. x x</tt># as [UAbs (fun x => UApp x x)]. Coq has built-in support for matching binders in anonymous [fun] expressions to their uses, so we avoid needing to implement our own binder-matching logic.
adamc@252 49
adamc@252 50 This definition is not quite HOAS, because of the broad variety of functions that Coq would allow us to pass as arguments to [UAbs]. We can thus construct many [uexp]s that do not correspond to normal lambda terms. These deviants are called %\textit{%#<i>#exotic terms#</i>#%}%. In LF, functions may only be written in a very restrictive computational language, lacking, among other things, pattern matching and recursive function definitions. Thus, thanks to a careful balancing act of design decisions, exotic terms are not possible with usual HOAS encodings in LF.
adamc@252 51
adamc@252 52 Our definition of [uexp] has a more fundamental problem: it is invalid in Gallina.
adamc@252 53
adamc@252 54 [[
adamc@252 55 Error: Non strictly positive occurrence of "uexp" in
adamc@252 56 "(uexp -> uexp) -> uexp".
adamc@252 57
adamc@252 58 ]]
adamc@252 59
adamc@252 60 We have violated a rule that we considered before: an inductive type may not be defined in terms of functions over itself. Way back in Chapter 3, we considered this example and the reasons why we should be glad that Coq rejects it. Thus, we will need to use more cleverness to reap similar benefits.
adamc@252 61
adamc@252 62 The root problem is that our expressions contain variables representing expressions of the same kind. Many useful kinds of syntax involve no such cycles. For instance, it is easy to use HOAS to encode standard first-order logic in Coq. *)
adamc@252 63
adamc@252 64 Inductive prop : Type :=
adamc@252 65 | Eq : forall T, T -> T -> prop
adamc@252 66 | Not : prop -> prop
adamc@252 67 | And : prop -> prop -> prop
adamc@252 68 | Or : prop -> prop -> prop
adamc@252 69 | Forall : forall T, (T -> prop) -> prop
adamc@252 70 | Exists : forall T, (T -> prop) -> prop.
adamc@252 71
adamc@252 72 Fixpoint propDenote (p : prop) : Prop :=
adamc@252 73 match p with
adamc@252 74 | Eq _ x y => x = y
adamc@252 75 | Not p => ~ (propDenote p)
adamc@252 76 | And p1 p2 => propDenote p1 /\ propDenote p2
adamc@252 77 | Or p1 p2 => propDenote p1 \/ propDenote p2
adamc@252 78 | Forall _ f => forall x, propDenote (f x)
adamc@252 79 | Exists _ f => exists x, propDenote (f x)
adamc@252 80 end.
adamc@252 81
adamc@252 82 (** Unfortunately, there are other recursive functions that we might like to write but cannot. One simple example is a function to count the number of constructors used to build a [prop]. To look inside a [Forall] or [Exists], we need to look inside the quantifier's body, which is represented as a function. In Gallina, as in most statically-typed functional languages, the only way to interact with a function is to call it. We have no hope of doing that here; the domain of the function in question has an arbitary type [T], so [T] may even be uninhabited. If we had a universal way of constructing values to look inside functions, we would have uncovered a consistency bug in Coq!
adamc@252 83
adamc@252 84 We are still suffering from the possibility of writing exotic terms, such as this example: *)
adamc@252 85
adamc@252 86 Example true_prop := Eq 1 1.
adamc@252 87 Example false_prop := Not true_prop.
adamc@252 88 Example exotic_prop := Forall (fun b : bool => if b then true_prop else false_prop).
adamc@252 89
adamc@252 90 (** Thus, the idea of a uniform way of looking inside a binder to find another well-defined [prop] is hopelessly doomed.
adamc@252 91
adamc@252 92 A clever HOAS variant called %\textit{%#<i>#weak HOAS#</i>#%}% manages to rule out exotic terms in Coq. Here is a weak HOAS version of untyped lambda terms. *)
adamc@252 93
adamc@252 94 Parameter var : Set.
adamc@252 95
adamc@252 96 Inductive uexp : Set :=
adamc@252 97 | UVar : var -> uexp
adamc@252 98 | UApp : uexp -> uexp -> uexp
adamc@252 99 | UAbs : (var -> uexp) -> uexp.
adamc@252 100
adamc@252 101 (** We postulate the existence of some set [var] of variables, and variable nodes appear explicitly in our syntax. A binder is represented as a function over %\textit{%#<i>#variables#</i>#%}%, rather than as a function over %\textit{%#<i>#expressions#</i>#%}%. This breaks the cycle that led Coq to reject the literal HOAS definition. It is easy to encode our previous example, $\lambda x. \; x \; x$#<tt>\x. x x</tt>#: *)
adamc@252 102
adamc@252 103 Example self_app := UAbs (fun x => UApp (UVar x) (UVar x)).
adamc@252 104
adamc@252 105 (** What about exotic terms? The problems they caused earlier came from the fact that Gallina is expressive enough to allow us to perform case analysis on the types we used as the domains of binder functions. With weak HOAS, we use an abstract type [var] as the domain. Since we assume the existence of no functions for deconstructing [var]s, Coq's type soundness enforces that no Gallina term of type [uexp] can take different values depending on the value of a [var] available in the typing context, %\textit{%#<i>#except#</i>#%}% by incorporating those variables into a [uexp] value in a legal way.
adamc@252 106
adamc@252 107 Weak HOAS retains the other disadvantage of our previous example: it is hard to write recursive functions that deconstruct terms. As with the previous example, some functions %\textit{%#<i>#are#</i>#%}% implementable. For instance, we can write a function to reverse the function and argument positions of every [UApp] node. *)
adamc@252 108
adamc@252 109 Fixpoint swap (e : uexp) : uexp :=
adamc@252 110 match e with
adamc@252 111 | UVar _ => e
adamc@252 112 | UApp e1 e2 => UApp (swap e2) (swap e1)
adamc@252 113 | UAbs e1 => UAbs (fun x => swap (e1 x))
adamc@252 114 end.
adamc@252 115
adamc@252 116 (** However, it is still impossible to write a function to compute the size of an expression. We would still need to manufacture a value of type [var] to peer under a binder, and that is impossible, because [var] is an abstract type. *)
adamc@252 117
adamc@252 118
adamc@252 119 (** * Parametric HOAS *)
adamc@158 120
adamc@253 121 (** In the context of Haskell, Washburn and Weirich introduced a technique called %\emph{%#<i>#parametric HOAS#</i>#%}%, or PHOAS. By making a slight alteration in the spirit of weak HOAS, we arrive at an encoding that addresses all three of the complaints above: the encoding is legal in Coq, exotic terms are impossible, and it is possible to write any syntax-deconstructing function that we can write with first-order encodings. The last of these advantages is not even present with HOAS in Twelf. In a sense, we receive it in exchange for giving up a free implementation of capture-avoiding substitution.
adamc@253 122
adamc@253 123 The first step is to change the weak HOAS type so that [var] is a variable inside a section, rather than a global parameter. *)
adamc@253 124
adamc@253 125 Reset uexp.
adamc@253 126
adamc@253 127 Section uexp.
adamc@253 128 Variable var : Set.
adamc@253 129
adamc@253 130 Inductive uexp : Set :=
adamc@253 131 | UVar : var -> uexp
adamc@253 132 | UApp : uexp -> uexp -> uexp
adamc@253 133 | UAbs : (var -> uexp) -> uexp.
adamc@253 134 End uexp.
adamc@253 135
adamc@253 136 (** Next, we can encapsulate choices of [var] inside a polymorphic function type. *)
adamc@253 137
adamc@253 138 Definition Uexp := forall var, uexp var.
adamc@253 139
adamc@253 140 (** This type [Uexp] is our final, exotic-term-free representation of lambda terms. Inside the body of a [Uexp] function, [var] values may not be deconstructed illegaly, for much the same reason as with weak HOAS. We simply trade an abstract type for parametric polymorphism.
adamc@253 141
adamc@253 142 Our running example $\lambda x. \; x \; x$#<tt>\x. x x</tt># is easily expressed: *)
adamc@253 143
adamc@253 144 Example self_app : Uexp := fun var => UAbs (var := var)
adamc@253 145 (fun x : var => UApp (var := var) (UVar (var := var) x) (UVar (var := var) x)).
adamc@253 146
adamc@253 147 (** Including all mentions of [var] explicitly helps clarify what is happening here, but it is convenient to let Coq's local type inference fill in these occurrences for us. *)
adamc@253 148
adamc@253 149 Example self_app' : Uexp := fun _ => UAbs (fun x => UApp (UVar x) (UVar x)).
adamc@253 150
adamc@253 151 (** We can go further and apply the PHOAS technique to dependently-typed ASTs, where Gallina typing guarantees that only well-typed terms can be represented. For the rest of this chapter, we consider the example of simply-typed lambda calculus with natural numbers and addition. We start with a conventional definition of the type language. *)
adamc@253 152
adamc@158 153 Inductive type : Type :=
adamc@159 154 | Nat : type
adamc@158 155 | Arrow : type -> type -> type.
adamc@158 156
adamc@158 157 Infix "-->" := Arrow (right associativity, at level 60).
adamc@158 158
adamc@253 159 (** Our definition of the expression type follows the definition for untyped lambda calculus, with one important change. Now our section variable [var] is not just a type. Rather, it is a %\textit{%#<i>#function#</i>#%}% returning types. The idea is that a variable of object language type [t] is represented by a [var t]. Note how this enables us to avoid indexing the [exp] type with a representation of typing contexts. *)
adamc@253 160
adamc@158 161 Section exp.
adamc@158 162 Variable var : type -> Type.
adamc@158 163
adamc@158 164 Inductive exp : type -> Type :=
adamc@159 165 | Const' : nat -> exp Nat
adamc@159 166 | Plus' : exp Nat -> exp Nat -> exp Nat
adamc@159 167
adamc@158 168 | Var : forall t, var t -> exp t
adamc@158 169 | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran
adamc@158 170 | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran).
adamc@158 171 End exp.
adamc@158 172
adamc@158 173 Implicit Arguments Const' [var].
adamc@158 174 Implicit Arguments Var [var t].
adamc@158 175 Implicit Arguments Abs' [var dom ran].
adamc@158 176
adamc@253 177 (** Our final representation type wraps [exp] as before. *)
adamc@253 178
adamc@158 179 Definition Exp t := forall var, exp var t.
adamc@253 180
adamc@169 181 (* begin thide *)
adamc@253 182
adamc@253 183 (** We can define some smart constructors to make it easier to build [Exp]s without using polymorphism explicitly. *)
adamc@158 184
adamc@159 185 Definition Const (n : nat) : Exp Nat :=
adamc@159 186 fun _ => Const' n.
adamc@159 187 Definition Plus (E1 E2 : Exp Nat) : Exp Nat :=
adamc@159 188 fun _ => Plus' (E1 _) (E2 _).
adamc@158 189 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
adamc@158 190 fun _ => App' (F _) (X _).
adamc@253 191
adamc@253 192 (** A case for function abstraction is not as natural, but we can implement one candidate in terms of a type family [Exp1], such that [Exp1 free result] represents an expression of type [result] with one free variable of type [free]. *)
adamc@253 193
adamc@253 194 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
adamc@158 195 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
adamc@158 196 fun _ => Abs' (B _).
adamc@169 197 (* end thide *)
adamc@169 198
adamc@169 199 (* EX: Define appropriate shorthands, so that these definitions type-check. *)
adamc@158 200
adamc@253 201 (** Now it is easy to encode a number of example programs. *)
adamc@253 202
adamc@253 203 Example zero := Const 0.
adamc@253 204 Example one := Const 1.
adamc@253 205 Example one_again := Plus zero one.
adamc@253 206 Example ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X).
adamc@253 207 Example app_ident := App ident one_again.
adamc@253 208 Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@166 209 Abs' (fun f => Abs' (fun x => App' (Var f) (Var x))).
adamc@253 210 Example app_ident' := App (App app ident) one_again.
adamc@166 211
adamc@169 212 (* EX: Define a function to count the number of variable occurrences in an [Exp]. *)
adamc@169 213
adamc@253 214 (** We can write syntax-deconstructing functions, such as [CountVars], which counts how many [Var] nodes appear in an [Exp]. First, we write a version [countVars] for [exp]s. The main trick is to specialize [countVars] to work over expressions where [var] is instantiated as [fun _ => unit]. That is, every variable is just a value of type [unit], such that variables carry no information. The important thing is that we have a value [tt] of type [unit] available, to use in descending into binders. *)
adamc@253 215
adamc@169 216 (* begin thide *)
adamc@222 217 Fixpoint countVars t (e : exp (fun _ => unit) t) : nat :=
adamc@166 218 match e with
adamc@166 219 | Const' _ => 0
adamc@166 220 | Plus' e1 e2 => countVars e1 + countVars e2
adamc@166 221 | Var _ _ => 1
adamc@166 222 | App' _ _ e1 e2 => countVars e1 + countVars e2
adamc@166 223 | Abs' _ _ e' => countVars (e' tt)
adamc@166 224 end.
adamc@166 225
adamc@253 226 (** We turn [countVars] into [CountVars] with explicit instantiation of a polymorphic [Exp] value [E]. We can write an underscore for the paramter to [E], because local type inference is able to infer the proper value. *)
adamc@253 227
adamc@166 228 Definition CountVars t (E : Exp t) : nat := countVars (E _).
adamc@169 229 (* end thide *)
adamc@166 230
adamc@253 231 (** A few evaluations establish that [CountVars] behaves plausibly. *)
adamc@253 232
adamc@166 233 Eval compute in CountVars zero.
adamc@253 234 (** %\vspace{-.15in}% [[
adamc@253 235 = 0
adamc@253 236 : nat
adam@302 237 ]]
adam@302 238 *)
adamc@253 239
adamc@166 240 Eval compute in CountVars one.
adamc@253 241 (** %\vspace{-.15in}% [[
adamc@253 242 = 0
adamc@253 243 : nat
adam@302 244 ]]
adam@302 245 *)
adamc@253 246
adamc@166 247 Eval compute in CountVars one_again.
adamc@253 248 (** %\vspace{-.15in}% [[
adamc@253 249 = 0
adamc@253 250 : nat
adam@302 251 ]]
adam@302 252 *)
adamc@253 253
adamc@166 254 Eval compute in CountVars ident.
adamc@253 255 (** %\vspace{-.15in}% [[
adamc@253 256 = 1
adamc@253 257 : nat
adam@302 258 ]]
adam@302 259 *)
adamc@253 260
adamc@166 261 Eval compute in CountVars app_ident.
adamc@253 262 (** %\vspace{-.15in}% [[
adamc@253 263 = 1
adamc@253 264 : nat
adam@302 265 ]]
adam@302 266 *)
adamc@253 267
adamc@166 268 Eval compute in CountVars app.
adamc@253 269 (** %\vspace{-.15in}% [[
adamc@253 270 = 2
adamc@253 271 : nat
adam@302 272 ]]
adam@302 273 *)
adamc@253 274
adamc@166 275 Eval compute in CountVars app_ident'.
adamc@253 276 (** %\vspace{-.15in}% [[
adamc@253 277 = 3
adamc@253 278 : nat
adam@302 279 ]]
adam@302 280 *)
adamc@253 281
adamc@166 282
adamc@169 283 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *)
adamc@169 284
adamc@253 285 (** We might want to go further and count occurrences of a single distinguished free variable in an expression. In this case, it is useful to instantiate [var] as [fun _ => bool]. We will represent the distinguished variable with [true] and all other variables with [false]. *)
adamc@253 286
adamc@169 287 (* begin thide *)
adamc@222 288 Fixpoint countOne t (e : exp (fun _ => bool) t) : nat :=
adamc@166 289 match e with
adamc@166 290 | Const' _ => 0
adamc@166 291 | Plus' e1 e2 => countOne e1 + countOne e2
adamc@166 292 | Var _ true => 1
adamc@166 293 | Var _ false => 0
adamc@166 294 | App' _ _ e1 e2 => countOne e1 + countOne e2
adamc@166 295 | Abs' _ _ e' => countOne (e' false)
adamc@166 296 end.
adamc@166 297
adamc@253 298 (** We wrap [countOne] into [CountOne], which we type using the [Exp1] definition from before. [CountOne] operates on an expression [E] with a single free variable. We apply an instantiated [E] to [true] to mark this variable as the one [countOne] should look for. [countOne] itself is careful to instantiate all other variables with [false]. *)
adamc@253 299
adamc@166 300 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat :=
adamc@166 301 countOne (E _ true).
adamc@169 302 (* end thide *)
adamc@166 303
adamc@253 304 (** We can check the behavior of [CountOne] on a few examples. *)
adamc@253 305
adamc@253 306 Example ident1 : Exp1 Nat Nat := fun _ X => Var X.
adamc@253 307 Example add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X).
adamc@253 308 Example app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0).
adamc@253 309 Example app_ident1 : Exp1 Nat Nat := fun _ X =>
adamc@253 310 App' (Abs' (fun Y => Var Y)) (Var X).
adamc@166 311
adamc@166 312 Eval compute in CountOne ident1.
adamc@253 313 (** %\vspace{-.15in}% [[
adamc@253 314 = 1
adamc@253 315 : nat
adam@302 316 ]]
adam@302 317 *)
adamc@253 318
adamc@166 319 Eval compute in CountOne add_self.
adamc@253 320 (** %\vspace{-.15in}% [[
adamc@253 321 = 2
adamc@253 322 : nat
adam@302 323 ]]
adam@302 324 *)
adamc@253 325
adamc@166 326 Eval compute in CountOne app_zero.
adamc@253 327 (** %\vspace{-.15in}% [[
adamc@253 328 = 1
adamc@253 329 : nat
adam@302 330 ]]
adam@302 331 *)
adamc@253 332
adamc@166 333 Eval compute in CountOne app_ident1.
adamc@253 334 (** %\vspace{-.15in}% [[
adamc@253 335 = 1
adamc@253 336 : nat
adam@302 337 ]]
adam@302 338 *)
adamc@253 339
adamc@166 340
adamc@169 341 (* EX: Define a function to pretty-print [Exp]s as strings. *)
adamc@169 342
adamc@253 343 (** The PHOAS encoding turns out to be just as general as the first-order encodings we saw previously. To provide a taste of that generality, we implement a translation into concrete syntax, rendered in human-readable strings. This is as easy as representing variables as strings. *)
adamc@253 344
adamc@169 345 (* begin thide *)
adamc@166 346 Section ToString.
adamc@166 347 Open Scope string_scope.
adamc@166 348
adamc@166 349 Fixpoint natToString (n : nat) : string :=
adamc@166 350 match n with
adamc@166 351 | O => "O"
adamc@166 352 | S n' => "S(" ++ natToString n' ++ ")"
adamc@166 353 end.
adamc@166 354
adamc@253 355 (** Function [toString] takes an extra argument [cur], which holds the last variable name assigned to a binder. We build new variable names by extending [cur] with primes. The function returns a pair of the next available variable name and of the actual expression rendering. *)
adamc@253 356
adamc@222 357 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) : string * string :=
adamc@166 358 match e with
adamc@166 359 | Const' n => (cur, natToString n)
adamc@166 360 | Plus' e1 e2 =>
adamc@166 361 let (cur', s1) := toString e1 cur in
adamc@166 362 let (cur'', s2) := toString e2 cur' in
adamc@166 363 (cur'', "(" ++ s1 ++ ") + (" ++ s2 ++ ")")
adamc@166 364 | Var _ s => (cur, s)
adamc@166 365 | App' _ _ e1 e2 =>
adamc@166 366 let (cur', s1) := toString e1 cur in
adamc@166 367 let (cur'', s2) := toString e2 cur' in
adamc@166 368 (cur'', "(" ++ s1 ++ ") (" ++ s2 ++ ")")
adamc@166 369 | Abs' _ _ e' =>
adamc@166 370 let (cur', s) := toString (e' cur) (cur ++ "'") in
adamc@166 371 (cur', "(\" ++ cur ++ ", " ++ s ++ ")")
adamc@166 372 end.
adamc@166 373
adamc@166 374 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x").
adamc@166 375 End ToString.
adamc@169 376 (* end thide *)
adamc@166 377
adamc@166 378 Eval compute in ToString zero.
adamc@253 379 (** %\vspace{-.15in}% [[
adamc@253 380 = "O"%string
adamc@253 381 : string
adam@302 382 ]]
adam@302 383 *)
adamc@253 384
adamc@166 385 Eval compute in ToString one.
adamc@253 386 (** %\vspace{-.15in}% [[
adamc@253 387 = "S(O)"%string
adamc@253 388 : string
adam@302 389 ]]
adam@302 390 *)
adamc@253 391
adamc@166 392 Eval compute in ToString one_again.
adamc@253 393 (** %\vspace{-.15in}% [[
adamc@253 394 = "(O) + (S(O))"%string
adamc@253 395 : string
adam@302 396 ]]
adam@302 397 *)
adamc@253 398
adamc@166 399 Eval compute in ToString ident.
adamc@253 400 (** %\vspace{-.15in}% [[
adamc@253 401 = "(\x, x)"%string
adamc@253 402 : string
adam@302 403 ]]
adam@302 404 *)
adamc@253 405
adamc@166 406 Eval compute in ToString app_ident.
adamc@253 407 (** %\vspace{-.15in}% [[
adamc@253 408 = "((\x, x)) ((O) + (S(O)))"%string
adamc@253 409 : string
adam@302 410 ]]
adam@302 411 *)
adamc@253 412
adamc@166 413 Eval compute in ToString app.
adamc@253 414 (** %\vspace{-.15in}% [[
adamc@253 415 = "(\x, (\x', (x) (x')))"%string
adamc@253 416 : string
adam@302 417 ]]
adam@302 418 *)
adamc@253 419
adamc@166 420 Eval compute in ToString app_ident'.
adamc@253 421 (** %\vspace{-.15in}% [[
adamc@253 422 = "(((\x, (\x', (x) (x')))) ((\x'', x''))) ((O) + (S(O)))"%string
adamc@253 423 : string
adam@302 424 ]]
adam@302 425 *)
adamc@253 426
adamc@166 427
adamc@169 428 (* EX: Define a substitution function. *)
adamc@169 429
adamc@253 430 (** Our final example is crucial to using PHOAS to encode standard operational semantics. We define capture-avoiding substitution, in terms of a function [flatten] which takes in an expression that represents variables as expressions. [flatten] replaces every node [Var e] with [e]. *)
adamc@253 431
adamc@169 432 (* begin thide *)
adamc@158 433 Section flatten.
adamc@158 434 Variable var : type -> Type.
adamc@158 435
adamc@222 436 Fixpoint flatten t (e : exp (exp var) t) : exp var t :=
adamc@222 437 match e with
adamc@159 438 | Const' n => Const' n
adamc@159 439 | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
adamc@158 440 | Var _ e' => e'
adamc@158 441 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
adamc@158 442 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
adamc@158 443 end.
adamc@158 444 End flatten.
adamc@158 445
adamc@253 446 (** Flattening turns out to implement the heart of substitution. We apply [E2], which has one free variable, to [E1], replacing the occurrences of the free variable by copies of [E1]. [flatten] takes care of removing the extra [Var] applications around these copies. *)
adamc@253 447
adamc@158 448 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
adamc@158 449 flatten (E2 _ (E1 _)).
adamc@169 450 (* end thide *)
adamc@158 451
adamc@166 452 Eval compute in Subst one ident1.
adamc@253 453 (** %\vspace{-.15in}% [[
adamc@253 454 = fun var : type -> Type => Const' 1
adamc@253 455 : Exp Nat
adam@302 456 ]]
adam@302 457 *)
adamc@253 458
adamc@166 459 Eval compute in Subst one add_self.
adamc@253 460 (** %\vspace{-.15in}% [[
adamc@253 461 = fun var : type -> Type => Plus' (Const' 1) (Const' 1)
adamc@253 462 : Exp Nat
adam@302 463 ]]
adam@302 464 *)
adamc@253 465
adamc@166 466 Eval compute in Subst ident app_zero.
adamc@253 467 (** %\vspace{-.15in}% [[
adamc@253 468 = fun var : type -> Type =>
adamc@253 469 App' (Abs' (fun X : var Nat => Var X)) (Const' 0)
adamc@253 470 : Exp Nat
adam@302 471 ]]
adam@302 472 *)
adamc@253 473
adamc@166 474 Eval compute in Subst one app_ident1.
adamc@253 475 (** %\vspace{-.15in}% [[
adamc@253 476 = fun var : type -> Type =>
adamc@253 477 App' (Abs' (fun x : var Nat => Var x)) (Const' 1)
adamc@253 478 : Exp Nat
adam@302 479 ]]
adam@302 480 *)
adamc@166 481
adamc@158 482
adamc@158 483 (** * A Type Soundness Proof *)
adamc@158 484
adamc@254 485 (** With [Subst] defined, there are few surprises encountered in defining a standard small-step, call-by-value semantics for our object language. We begin by classifying a subset of expressions as values. *)
adamc@158 486
adamc@158 487 Inductive Val : forall t, Exp t -> Prop :=
adamc@159 488 | VConst : forall n, Val (Const n)
adamc@158 489 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
adamc@158 490
adamc@158 491 Hint Constructors Val.
adamc@158 492
adamc@254 493 (** Since this language is more complicated than the one we considered in the chapter on first-order encodings, we will use explicit evaluation contexts to define the semantics. A value of type [Ctx t u] is a context that yields an expression of type [u] when filled by an expression of type [t]. We have one context for each position of the [App] and [Plus] constructors. *)
adamc@254 494
adamc@162 495 Inductive Ctx : type -> type -> Type :=
adamc@162 496 | AppCong1 : forall (dom ran : type),
adamc@162 497 Exp dom -> Ctx (dom --> ran) ran
adamc@162 498 | AppCong2 : forall (dom ran : type),
adamc@162 499 Exp (dom --> ran) -> Ctx dom ran
adamc@162 500 | PlusCong1 : Exp Nat -> Ctx Nat Nat
adamc@162 501 | PlusCong2 : Exp Nat -> Ctx Nat Nat.
adamc@162 502
adamc@254 503 (** A judgment characterizes when contexts are valid, enforcing the standard call-by-value restriction that certain positions must hold values. *)
adamc@254 504
adamc@162 505 Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop :=
adamc@162 506 | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X)
adamc@162 507 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F)
adamc@162 508 | IsPlus1 : forall E2, isCtx (PlusCong1 E2)
adamc@162 509 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).
adamc@162 510
adamc@254 511 (** A simple definition implements plugging a context with a specific expression. *)
adamc@254 512
adamc@162 513 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
adamc@222 514 match C with
adamc@162 515 | AppCong1 _ _ X => fun F => App F X
adamc@162 516 | AppCong2 _ _ F => fun X => App F X
adamc@162 517 | PlusCong1 E2 => fun E1 => Plus E1 E2
adamc@162 518 | PlusCong2 E1 => fun E2 => Plus E1 E2
adamc@162 519 end.
adamc@162 520
adamc@162 521 Infix "@" := plug (no associativity, at level 60).
adamc@162 522
adamc@254 523 (** Finally, we have the step relation itself, which combines our ingredients in the standard way. In the congruence rule, we introduce the extra variable [E1] and its associated equality to make the rule easier for [eauto] to apply. *)
adamc@254 524
adam@292 525 (** printing ==> $\Rightarrow$ *)
adamc@254 526 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
adamc@254 527
adamc@158 528 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
adamc@158 529 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
adamc@160 530 Val X
adamc@160 531 -> App (Abs B) X ==> Subst X B
adamc@159 532 | Sum : forall n1 n2,
adamc@159 533 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
adamc@162 534 | Cong : forall t t' (C : Ctx t t') E E' E1,
adamc@162 535 isCtx C
adamc@162 536 -> E1 = C @ E
adamc@162 537 -> E ==> E'
adamc@162 538 -> E1 ==> C @ E'
adamc@159 539
adamc@158 540 where "E1 ==> E2" := (Step E1 E2).
adamc@158 541
adamc@162 542 Hint Constructors isCtx Step.
adamc@158 543
adamc@169 544 (* EX: Prove type soundness. *)
adamc@169 545
adamc@254 546 (** To prove type soundness for this semantics, we need to overcome one crucial obstacle. Standard proofs use induction on the structure of typing derivations. Our encoding mixes typing derivations with expression syntax, so we want to induct over expression structure. Our expressions are represented as functions, which do not, in general, admit induction in Coq. However, because of our use of parametric polymorphism, we know that our expressions do, in fact, have inductive structure. In particular, every closed value of [Exp] type must belong to the following relation. *)
adamc@254 547
adamc@169 548 (* begin thide *)
adamc@158 549 Inductive Closed : forall t, Exp t -> Prop :=
adamc@164 550 | CConst : forall n,
adamc@164 551 Closed (Const n)
adamc@159 552 | CPlus : forall E1 E2,
adamc@159 553 Closed E1
adamc@159 554 -> Closed E2
adamc@159 555 -> Closed (Plus E1 E2)
adamc@158 556 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
adamc@158 557 Closed E1
adamc@158 558 -> Closed E2
adamc@158 559 -> Closed (App E1 E2)
adamc@158 560 | CAbs : forall dom ran (E1 : Exp1 dom ran),
adamc@158 561 Closed (Abs E1).
adamc@158 562
adamc@254 563 (** How can we prove such a fact? It probably cannot be established in Coq without axioms. Rather, one would have to establish it metatheoretically, reasoning informally outside of Coq. For now, we assert the fact as an axiom. The later chapter on intensional transformations shows one approach to removing the need for an axiom. *)
adamc@254 564
adamc@158 565 Axiom closed : forall t (E : Exp t), Closed E.
adamc@158 566
adamc@254 567 (** The usual progress and preservation theorems are now very easy to prove. In fact, preservation is implicit in our dependently-typed definition of [Step]. This is a huge win, because we avoid completely the theorem about substitution and typing that made up the bulk of each proof in the chapter on first-order encodings. The progress theorem yields to a few lines of automation.
adamc@254 568
adamc@254 569 We define a slight variant of [crush] which also looks for chances to use the theorem [inj_pair2] on hypotheses. This theorem deals with an artifact of the way that [inversion] works on dependently-typed hypotheses. *)
adamc@254 570
adamc@160 571 Ltac my_crush' :=
adamc@167 572 crush;
adamc@158 573 repeat (match goal with
adamc@254 574 | [ H : _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
adamc@167 575 end; crush).
adamc@160 576
adamc@162 577 Hint Extern 1 (_ = _ @ _) => simpl.
adamc@162 578
adamc@254 579 (** This is the point where we need to do induction over functions, in the form of expressions [E]. The judgment [Closed] provides the perfect framework; we induct over [Closed] derivations. *)
adamc@254 580
adamc@158 581 Lemma progress' : forall t (E : Exp t),
adamc@158 582 Closed E
adamc@158 583 -> Val E \/ exists E', E ==> E'.
adamc@158 584 induction 1; crush;
adamc@159 585 repeat match goal with
adamc@167 586 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush'
adamc@162 587 end; eauto 6.
adamc@158 588 Qed.
adamc@158 589
adamc@254 590 (** Our final proof of progress makes one top-level use of the axiom [closed] that we asserted above. *)
adamc@254 591
adamc@158 592 Theorem progress : forall t (E : Exp t),
adamc@158 593 Val E \/ exists E', E ==> E'.
adamc@158 594 intros; apply progress'; apply closed.
adamc@158 595 Qed.
adamc@169 596 (* end thide *)
adamc@158 597
adamc@160 598
adamc@160 599 (** * Big-Step Semantics *)
adamc@160 600
adamc@254 601 (** Another standard exercise in operational semantics is proving the equivalence of small-step and big-step semantics. We can carry out this exercise for our PHOAS lambda calculus. Most of the steps are just as pleasant as in the previous section, but things get complicated near to the end.
adamc@254 602
adamc@254 603 We must start by defining the big-step semantics itself. The definition is completely standard. *)
adamc@254 604
adam@292 605 (** printing ===> $\Longrightarrow$ *)
adamc@160 606 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
adamc@160 607
adamc@160 608 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 609 | SConst : forall n,
adamc@160 610 Const n ===> Const n
adamc@160 611 | SPlus : forall E1 E2 n1 n2,
adamc@160 612 E1 ===> Const n1
adamc@160 613 -> E2 ===> Const n2
adamc@160 614 -> Plus E1 E2 ===> Const (n1 + n2)
adamc@160 615
adamc@160 616 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
adamc@160 617 E1 ===> Abs B
adamc@160 618 -> E2 ===> V2
adamc@160 619 -> Subst V2 B ===> V
adamc@160 620 -> App E1 E2 ===> V
adamc@160 621 | SAbs : forall dom ran (B : Exp1 dom ran),
adamc@160 622 Abs B ===> Abs B
adamc@160 623
adamc@160 624 where "E1 ===> E2" := (BigStep E1 E2).
adamc@160 625
adamc@160 626 Hint Constructors BigStep.
adamc@160 627
adamc@169 628 (* EX: Prove the equivalence of the small- and big-step semantics. *)
adamc@169 629
adamc@254 630 (** To prove a crucial intermediate lemma, we will want to name the transitive-reflexive closure of the small-step relation. *)
adamc@254 631
adamc@169 632 (* begin thide *)
adam@292 633 (** printing ==>* $\Rightarrow^*$ *)
adamc@160 634 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
adamc@160 635
adamc@160 636 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 637 | Done : forall t (E : Exp t), E ==>* E
adamc@160 638 | OneStep : forall t (E E' E'' : Exp t),
adamc@160 639 E ==> E'
adamc@160 640 -> E' ==>* E''
adamc@160 641 -> E ==>* E''
adamc@160 642
adamc@160 643 where "E1 ==>* E2" := (MultiStep E1 E2).
adamc@160 644
adamc@160 645 Hint Constructors MultiStep.
adamc@160 646
adamc@254 647 (** A few basic properties of evaluation and values admit easy proofs. *)
adamc@254 648
adamc@160 649 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
adamc@160 650 E1 ==>* E2
adamc@160 651 -> E2 ==>* E3
adamc@160 652 -> E1 ==>* E3.
adamc@160 653 induction 1; eauto.
adamc@160 654 Qed.
adamc@160 655
adamc@160 656 Theorem Big_Val : forall t (E V : Exp t),
adamc@160 657 E ===> V
adamc@160 658 -> Val V.
adamc@160 659 induction 1; crush.
adamc@160 660 Qed.
adamc@160 661
adamc@160 662 Theorem Val_Big : forall t (V : Exp t),
adamc@160 663 Val V
adamc@160 664 -> V ===> V.
adamc@160 665 destruct 1; crush.
adamc@160 666 Qed.
adamc@160 667
adamc@160 668 Hint Resolve Big_Val Val_Big.
adamc@160 669
adamc@254 670 (** Another useful property deals with pushing multi-step evaluation inside of contexts. *)
adamc@254 671
adamc@162 672 Lemma Multi_Cong : forall t t' (C : Ctx t t'),
adamc@162 673 isCtx C
adamc@162 674 -> forall E E', E ==>* E'
adamc@162 675 -> C @ E ==>* C @ E'.
adamc@160 676 induction 2; crush; eauto.
adamc@160 677 Qed.
adamc@160 678
adamc@162 679 Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
adamc@162 680 isCtx C
adamc@162 681 -> E1 = C @ E
adamc@162 682 -> E2 = C @ E'
adamc@162 683 -> E ==>* E'
adamc@162 684 -> E1 ==>* E2.
adamc@162 685 crush; apply Multi_Cong; auto.
adamc@162 686 Qed.
adamc@162 687
adamc@162 688 Hint Resolve Multi_Cong'.
adamc@162 689
adamc@254 690 (** Unrestricted use of transitivity of [==>*] can lead to very large [eauto] search spaces, which has very inconvenient efficiency consequences. Instead, we define a special tactic [mtrans] that tries applying transitivity with a particular intermediate expression. *)
adamc@254 691
adamc@162 692 Ltac mtrans E :=
adamc@162 693 match goal with
adamc@162 694 | [ |- E ==>* _ ] => fail 1
adamc@162 695 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
adamc@162 696 end.
adamc@160 697
adamc@254 698 (** With [mtrans], we can give a reasonably short proof of one direction of the equivalence between big-step and small-step semantics. We include proof cases specific to rules of the big-step semantics, since leaving the details to [eauto] would lead to a very slow proof script. The use of [solve] in [mtrans]'s definition keeps us from going down unfruitful paths. *)
adamc@254 699
adamc@160 700 Theorem Big_Multi : forall t (E V : Exp t),
adamc@160 701 E ===> V
adamc@160 702 -> E ==>* V.
adamc@162 703 induction 1; crush; eauto;
adamc@162 704 repeat match goal with
adamc@162 705 | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
adamc@162 706 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
adamc@162 707 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
adamc@162 708 end.
adamc@160 709 Qed.
adamc@160 710
adamc@254 711 (** We are almost ready to prove the other direction of the equivalence. First, we wrap an earlier lemma in a form that will work better with [eauto]. *)
adamc@254 712
adamc@160 713 Lemma Big_Val' : forall t (V1 V2 : Exp t),
adamc@160 714 Val V2
adamc@160 715 -> V1 = V2
adamc@160 716 -> V1 ===> V2.
adamc@160 717 crush.
adamc@160 718 Qed.
adamc@160 719
adamc@160 720 Hint Resolve Big_Val'.
adamc@160 721
adamc@254 722 (** Now we build some quite involved tactic support for reasoning about equalities over PHOAS terms. First, we will call [equate_conj F G] to determine the consequences of an equality [F = G]. When [F = f e_1 ... e_n] and [G = f e'_1 ... e'_n], [equate_conj] will return a conjunction [e_1 = e'_1 /\ ... /\ e_n = e'_n]. We hardcode a pattern for each value of [n] from 1 to 5. *)
adamc@254 723
adamc@167 724 Ltac equate_conj F G :=
adamc@167 725 match constr:(F, G) with
adamc@167 726 | (_ ?x1, _ ?x2) => constr:(x1 = x2)
adamc@167 727 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
adamc@167 728 | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
adamc@222 729 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) =>
adamc@222 730 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
adamc@222 731 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) =>
adamc@222 732 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
adamc@167 733 end.
adamc@167 734
adamc@254 735 (** The main tactic is [my_crush], which generalizes our earlier [my_crush'] by performing inversion on hypotheses that equate PHOAS terms. Coq's built-in [inversion] is only designed to be useful on equalities over inductive types. PHOAS terms are functions, so [inversion] is not very helpful on them. To perform the equivalent of [discriminate], we instantiate the terms with [var] as [fun _ => unit] and then appeal to normal [discriminate]. This eliminates some contradictory cases. To perform the equivalent of [injection], we must consider all possible [var] instantiations. Some fairly intricate logic strings together these elements. The details are not worth discussing, since our conclusion will be that one should avoid dealing with proofs of facts like this one. *)
adamc@254 736
adamc@167 737 Ltac my_crush :=
adamc@167 738 my_crush';
adamc@167 739 repeat (match goal with
adamc@167 740 | [ H : ?F = ?G |- _ ] =>
adamc@167 741 (let H' := fresh "H'" in
adamc@167 742 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
adamc@167 743 | discriminate || injection H'; clear H' ];
adamc@167 744 my_crush';
adamc@167 745 repeat match goal with
adamc@167 746 | [ H : context[fun _ => unit] |- _ ] => clear H
adamc@167 747 end;
adamc@167 748 match type of H with
adamc@167 749 | ?F = ?G =>
adamc@167 750 let ec := equate_conj F G in
adamc@167 751 let var := fresh "var" in
adam@297 752 assert ec; [ intuition; unfold Exp; extensionality var;
adam@297 753 assert (H' : F var = G var); try congruence;
adam@297 754 match type of H' with
adam@297 755 | ?X = ?Y =>
adam@297 756 let X := eval hnf in X in
adam@297 757 let Y := eval hnf in Y in
adam@297 758 change (X = Y) in H'
adam@297 759 end; injection H'; my_crush'; tauto
adamc@167 760 | intuition; subst ]
adamc@167 761 end);
adamc@167 762 clear H
adamc@167 763 end; my_crush');
adamc@167 764 my_crush'.
adamc@167 765
adamc@254 766 (** With that complicated tactic available, the proof of the main lemma is straightforward. *)
adamc@254 767
adamc@160 768 Lemma Multi_Big' : forall t (E E' : Exp t),
adamc@160 769 E ==> E'
adamc@160 770 -> forall E'', E' ===> E''
adamc@160 771 -> E ===> E''.
adamc@160 772 induction 1; crush; eauto;
adamc@160 773 match goal with
adamc@160 774 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
adamc@162 775 end;
adamc@162 776 match goal with
adamc@162 777 | [ H : isCtx _ |- _ ] => inversion H; my_crush; eauto
adamc@160 778 end.
adamc@160 779 Qed.
adamc@160 780
adamc@160 781 Hint Resolve Multi_Big'.
adamc@160 782
adamc@254 783 (** The other direction of the overall equivalence follows as an easy corollary. *)
adamc@254 784
adamc@160 785 Theorem Multi_Big : forall t (E V : Exp t),
adamc@160 786 E ==>* V
adamc@160 787 -> Val V
adamc@160 788 -> E ===> V.
adamc@160 789 induction 1; crush; eauto.
adamc@160 790 Qed.
adamc@169 791 (* end thide *)
adamc@254 792
adamc@254 793 (** The lesson here is that working directly with PHOAS terms can easily lead to extremely intricate proofs. It is usually a better idea to stick to inductive proofs about %\textit{%#<i>#instantiated#</i>#%}% PHOAS terms; in the case of this example, that means proofs about [exp] instead of [Exp]. Such results can usually be wrapped into results about [Exp] without further induction. Different theorems demand different variants of this underlying advice, and we will consider several of them in the chapters to come. *)