Mercurial > cpdt > repo

annotate src/Hoas.v @ 256:4293dd6912cd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Prosified Extensional
author Adam Chlipala <adamc@hcoop.net>
date Wed, 16 Dec 2009 15:31:54 -0500
parents e3c3b7ef5901
children 2c88fc1dbe33
rev   line source
adamc@222 1 (* Copyright (c) 2008-2009, 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 *)
adamc@168 11 Require Import Eqdep String List.
adamc@158 12
adamc@168 13 Require Import Axioms Tactics.
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
adamc@252 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
adamc@253 237 ]] *)
adamc@253 238
adamc@166 239 Eval compute in CountVars one.
adamc@253 240 (** %\vspace{-.15in}% [[
adamc@253 241 = 0
adamc@253 242 : nat
adamc@253 243 ]] *)
adamc@253 244
adamc@166 245 Eval compute in CountVars one_again.
adamc@253 246 (** %\vspace{-.15in}% [[
adamc@253 247 = 0
adamc@253 248 : nat
adamc@253 249 ]] *)
adamc@253 250
adamc@166 251 Eval compute in CountVars ident.
adamc@253 252 (** %\vspace{-.15in}% [[
adamc@253 253 = 1
adamc@253 254 : nat
adamc@253 255 ]] *)
adamc@253 256
adamc@166 257 Eval compute in CountVars app_ident.
adamc@253 258 (** %\vspace{-.15in}% [[
adamc@253 259 = 1
adamc@253 260 : nat
adamc@253 261 ]] *)
adamc@253 262
adamc@166 263 Eval compute in CountVars app.
adamc@253 264 (** %\vspace{-.15in}% [[
adamc@253 265 = 2
adamc@253 266 : nat
adamc@253 267 ]] *)
adamc@253 268
adamc@166 269 Eval compute in CountVars app_ident'.
adamc@253 270 (** %\vspace{-.15in}% [[
adamc@253 271 = 3
adamc@253 272 : nat
adamc@253 273 ]] *)
adamc@253 274
adamc@166 275
adamc@169 276 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *)
adamc@169 277
adamc@253 278 (** 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 279
adamc@169 280 (* begin thide *)
adamc@222 281 Fixpoint countOne t (e : exp (fun _ => bool) t) : nat :=
adamc@166 282 match e with
adamc@166 283 | Const' _ => 0
adamc@166 284 | Plus' e1 e2 => countOne e1 + countOne e2
adamc@166 285 | Var _ true => 1
adamc@166 286 | Var _ false => 0
adamc@166 287 | App' _ _ e1 e2 => countOne e1 + countOne e2
adamc@166 288 | Abs' _ _ e' => countOne (e' false)
adamc@166 289 end.
adamc@166 290
adamc@253 291 (** 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 292
adamc@166 293 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat :=
adamc@166 294 countOne (E _ true).
adamc@169 295 (* end thide *)
adamc@166 296
adamc@253 297 (** We can check the behavior of [CountOne] on a few examples. *)
adamc@253 298
adamc@253 299 Example ident1 : Exp1 Nat Nat := fun _ X => Var X.
adamc@253 300 Example add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X).
adamc@253 301 Example app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0).
adamc@253 302 Example app_ident1 : Exp1 Nat Nat := fun _ X =>
adamc@253 303 App' (Abs' (fun Y => Var Y)) (Var X).
adamc@166 304
adamc@166 305 Eval compute in CountOne ident1.
adamc@253 306 (** %\vspace{-.15in}% [[
adamc@253 307 = 1
adamc@253 308 : nat
adamc@253 309 ]] *)
adamc@253 310
adamc@166 311 Eval compute in CountOne add_self.
adamc@253 312 (** %\vspace{-.15in}% [[
adamc@253 313 = 2
adamc@253 314 : nat
adamc@253 315 ]] *)
adamc@253 316
adamc@166 317 Eval compute in CountOne app_zero.
adamc@253 318 (** %\vspace{-.15in}% [[
adamc@253 319 = 1
adamc@253 320 : nat
adamc@253 321 ]] *)
adamc@253 322
adamc@166 323 Eval compute in CountOne app_ident1.
adamc@253 324 (** %\vspace{-.15in}% [[
adamc@253 325 = 1
adamc@253 326 : nat
adamc@253 327 ]] *)
adamc@253 328
adamc@166 329
adamc@169 330 (* EX: Define a function to pretty-print [Exp]s as strings. *)
adamc@169 331
adamc@253 332 (** 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 333
adamc@169 334 (* begin thide *)
adamc@166 335 Section ToString.
adamc@166 336 Open Scope string_scope.
adamc@166 337
adamc@166 338 Fixpoint natToString (n : nat) : string :=
adamc@166 339 match n with
adamc@166 340 | O => "O"
adamc@166 341 | S n' => "S(" ++ natToString n' ++ ")"
adamc@166 342 end.
adamc@166 343
adamc@253 344 (** 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 345
adamc@222 346 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) : string * string :=
adamc@166 347 match e with
adamc@166 348 | Const' n => (cur, natToString n)
adamc@166 349 | Plus' e1 e2 =>
adamc@166 350 let (cur', s1) := toString e1 cur in
adamc@166 351 let (cur'', s2) := toString e2 cur' in
adamc@166 352 (cur'', "(" ++ s1 ++ ") + (" ++ s2 ++ ")")
adamc@166 353 | Var _ s => (cur, s)
adamc@166 354 | App' _ _ e1 e2 =>
adamc@166 355 let (cur', s1) := toString e1 cur in
adamc@166 356 let (cur'', s2) := toString e2 cur' in
adamc@166 357 (cur'', "(" ++ s1 ++ ") (" ++ s2 ++ ")")
adamc@166 358 | Abs' _ _ e' =>
adamc@166 359 let (cur', s) := toString (e' cur) (cur ++ "'") in
adamc@166 360 (cur', "(\" ++ cur ++ ", " ++ s ++ ")")
adamc@166 361 end.
adamc@166 362
adamc@166 363 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x").
adamc@166 364 End ToString.
adamc@169 365 (* end thide *)
adamc@166 366
adamc@166 367 Eval compute in ToString zero.
adamc@253 368 (** %\vspace{-.15in}% [[
adamc@253 369 = "O"%string
adamc@253 370 : string
adamc@253 371 ]] *)
adamc@253 372
adamc@166 373 Eval compute in ToString one.
adamc@253 374 (** %\vspace{-.15in}% [[
adamc@253 375 = "S(O)"%string
adamc@253 376 : string
adamc@253 377 ]] *)
adamc@253 378
adamc@166 379 Eval compute in ToString one_again.
adamc@253 380 (** %\vspace{-.15in}% [[
adamc@253 381 = "(O) + (S(O))"%string
adamc@253 382 : string
adamc@253 383 ]] *)
adamc@253 384
adamc@166 385 Eval compute in ToString ident.
adamc@253 386 (** %\vspace{-.15in}% [[
adamc@253 387 = "(\x, x)"%string
adamc@253 388 : string
adamc@253 389 ]] *)
adamc@253 390
adamc@166 391 Eval compute in ToString app_ident.
adamc@253 392 (** %\vspace{-.15in}% [[
adamc@253 393 = "((\x, x)) ((O) + (S(O)))"%string
adamc@253 394 : string
adamc@253 395 ]] *)
adamc@253 396
adamc@166 397 Eval compute in ToString app.
adamc@253 398 (** %\vspace{-.15in}% [[
adamc@253 399 = "(\x, (\x', (x) (x')))"%string
adamc@253 400 : string
adamc@253 401 ]] *)
adamc@253 402
adamc@166 403 Eval compute in ToString app_ident'.
adamc@253 404 (** %\vspace{-.15in}% [[
adamc@253 405 = "(((\x, (\x', (x) (x')))) ((\x'', x''))) ((O) + (S(O)))"%string
adamc@253 406 : string
adamc@253 407 ]] *)
adamc@253 408
adamc@166 409
adamc@169 410 (* EX: Define a substitution function. *)
adamc@169 411
adamc@253 412 (** 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 413
adamc@169 414 (* begin thide *)
adamc@158 415 Section flatten.
adamc@158 416 Variable var : type -> Type.
adamc@158 417
adamc@222 418 Fixpoint flatten t (e : exp (exp var) t) : exp var t :=
adamc@222 419 match e with
adamc@159 420 | Const' n => Const' n
adamc@159 421 | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
adamc@158 422 | Var _ e' => e'
adamc@158 423 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
adamc@158 424 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
adamc@158 425 end.
adamc@158 426 End flatten.
adamc@158 427
adamc@253 428 (** 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 429
adamc@158 430 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
adamc@158 431 flatten (E2 _ (E1 _)).
adamc@169 432 (* end thide *)
adamc@158 433
adamc@166 434 Eval compute in Subst one ident1.
adamc@253 435 (** %\vspace{-.15in}% [[
adamc@253 436 = fun var : type -> Type => Const' 1
adamc@253 437 : Exp Nat
adamc@253 438 ]] *)
adamc@253 439
adamc@166 440 Eval compute in Subst one add_self.
adamc@253 441 (** %\vspace{-.15in}% [[
adamc@253 442 = fun var : type -> Type => Plus' (Const' 1) (Const' 1)
adamc@253 443 : Exp Nat
adamc@253 444 ]] *)
adamc@253 445
adamc@166 446 Eval compute in Subst ident app_zero.
adamc@253 447 (** %\vspace{-.15in}% [[
adamc@253 448 = fun var : type -> Type =>
adamc@253 449 App' (Abs' (fun X : var Nat => Var X)) (Const' 0)
adamc@253 450 : Exp Nat
adamc@253 451 ]] *)
adamc@253 452
adamc@166 453 Eval compute in Subst one app_ident1.
adamc@253 454 (** %\vspace{-.15in}% [[
adamc@253 455 = fun var : type -> Type =>
adamc@253 456 App' (Abs' (fun x : var Nat => Var x)) (Const' 1)
adamc@253 457 : Exp Nat
adamc@253 458 ]] *)
adamc@166 459
adamc@158 460
adamc@158 461 (** * A Type Soundness Proof *)
adamc@158 462
adamc@254 463 (** 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 464
adamc@158 465 Inductive Val : forall t, Exp t -> Prop :=
adamc@159 466 | VConst : forall n, Val (Const n)
adamc@158 467 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
adamc@158 468
adamc@158 469 Hint Constructors Val.
adamc@158 470
adamc@254 471 (** 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 472
adamc@162 473 Inductive Ctx : type -> type -> Type :=
adamc@162 474 | AppCong1 : forall (dom ran : type),
adamc@162 475 Exp dom -> Ctx (dom --> ran) ran
adamc@162 476 | AppCong2 : forall (dom ran : type),
adamc@162 477 Exp (dom --> ran) -> Ctx dom ran
adamc@162 478 | PlusCong1 : Exp Nat -> Ctx Nat Nat
adamc@162 479 | PlusCong2 : Exp Nat -> Ctx Nat Nat.
adamc@162 480
adamc@254 481 (** A judgment characterizes when contexts are valid, enforcing the standard call-by-value restriction that certain positions must hold values. *)
adamc@254 482
adamc@162 483 Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop :=
adamc@162 484 | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X)
adamc@162 485 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F)
adamc@162 486 | IsPlus1 : forall E2, isCtx (PlusCong1 E2)
adamc@162 487 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).
adamc@162 488
adamc@254 489 (** A simple definition implements plugging a context with a specific expression. *)
adamc@254 490
adamc@162 491 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
adamc@222 492 match C with
adamc@162 493 | AppCong1 _ _ X => fun F => App F X
adamc@162 494 | AppCong2 _ _ F => fun X => App F X
adamc@162 495 | PlusCong1 E2 => fun E1 => Plus E1 E2
adamc@162 496 | PlusCong2 E1 => fun E2 => Plus E1 E2
adamc@162 497 end.
adamc@162 498
adamc@162 499 Infix "@" := plug (no associativity, at level 60).
adamc@162 500
adamc@254 501 (** 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 502
adamc@254 503 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
adamc@254 504
adamc@158 505 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
adamc@158 506 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
adamc@160 507 Val X
adamc@160 508 -> App (Abs B) X ==> Subst X B
adamc@159 509 | Sum : forall n1 n2,
adamc@159 510 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
adamc@162 511 | Cong : forall t t' (C : Ctx t t') E E' E1,
adamc@162 512 isCtx C
adamc@162 513 -> E1 = C @ E
adamc@162 514 -> E ==> E'
adamc@162 515 -> E1 ==> C @ E'
adamc@159 516
adamc@158 517 where "E1 ==> E2" := (Step E1 E2).
adamc@158 518
adamc@162 519 Hint Constructors isCtx Step.
adamc@158 520
adamc@169 521 (* EX: Prove type soundness. *)
adamc@169 522
adamc@254 523 (** 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 524
adamc@169 525 (* begin thide *)
adamc@158 526 Inductive Closed : forall t, Exp t -> Prop :=
adamc@164 527 | CConst : forall n,
adamc@164 528 Closed (Const n)
adamc@159 529 | CPlus : forall E1 E2,
adamc@159 530 Closed E1
adamc@159 531 -> Closed E2
adamc@159 532 -> Closed (Plus E1 E2)
adamc@158 533 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
adamc@158 534 Closed E1
adamc@158 535 -> Closed E2
adamc@158 536 -> Closed (App E1 E2)
adamc@158 537 | CAbs : forall dom ran (E1 : Exp1 dom ran),
adamc@158 538 Closed (Abs E1).
adamc@158 539
adamc@254 540 (** 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 541
adamc@158 542 Axiom closed : forall t (E : Exp t), Closed E.
adamc@158 543
adamc@254 544 (** 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 545
adamc@254 546 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 547
adamc@160 548 Ltac my_crush' :=
adamc@167 549 crush;
adamc@158 550 repeat (match goal with
adamc@254 551 | [ H : _ |- _ ] => generalize (inj_pair2 _ _ _ _ _ H); clear H
adamc@167 552 end; crush).
adamc@160 553
adamc@162 554 Hint Extern 1 (_ = _ @ _) => simpl.
adamc@162 555
adamc@254 556 (** 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 557
adamc@158 558 Lemma progress' : forall t (E : Exp t),
adamc@158 559 Closed E
adamc@158 560 -> Val E \/ exists E', E ==> E'.
adamc@158 561 induction 1; crush;
adamc@159 562 repeat match goal with
adamc@167 563 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush'
adamc@162 564 end; eauto 6.
adamc@158 565 Qed.
adamc@158 566
adamc@254 567 (** Our final proof of progress makes one top-level use of the axiom [closed] that we asserted above. *)
adamc@254 568
adamc@158 569 Theorem progress : forall t (E : Exp t),
adamc@158 570 Val E \/ exists E', E ==> E'.
adamc@158 571 intros; apply progress'; apply closed.
adamc@158 572 Qed.
adamc@169 573 (* end thide *)
adamc@158 574
adamc@160 575
adamc@160 576 (** * Big-Step Semantics *)
adamc@160 577
adamc@254 578 (** 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 579
adamc@254 580 We must start by defining the big-step semantics itself. The definition is completely standard. *)
adamc@254 581
adamc@160 582 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
adamc@160 583
adamc@160 584 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 585 | SConst : forall n,
adamc@160 586 Const n ===> Const n
adamc@160 587 | SPlus : forall E1 E2 n1 n2,
adamc@160 588 E1 ===> Const n1
adamc@160 589 -> E2 ===> Const n2
adamc@160 590 -> Plus E1 E2 ===> Const (n1 + n2)
adamc@160 591
adamc@160 592 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
adamc@160 593 E1 ===> Abs B
adamc@160 594 -> E2 ===> V2
adamc@160 595 -> Subst V2 B ===> V
adamc@160 596 -> App E1 E2 ===> V
adamc@160 597 | SAbs : forall dom ran (B : Exp1 dom ran),
adamc@160 598 Abs B ===> Abs B
adamc@160 599
adamc@160 600 where "E1 ===> E2" := (BigStep E1 E2).
adamc@160 601
adamc@160 602 Hint Constructors BigStep.
adamc@160 603
adamc@169 604 (* EX: Prove the equivalence of the small- and big-step semantics. *)
adamc@169 605
adamc@254 606 (** To prove a crucial intermediate lemma, we will want to name the transitive-reflexive closure of the small-step relation. *)
adamc@254 607
adamc@169 608 (* begin thide *)
adamc@160 609 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
adamc@160 610
adamc@160 611 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 612 | Done : forall t (E : Exp t), E ==>* E
adamc@160 613 | OneStep : forall t (E E' E'' : Exp t),
adamc@160 614 E ==> E'
adamc@160 615 -> E' ==>* E''
adamc@160 616 -> E ==>* E''
adamc@160 617
adamc@160 618 where "E1 ==>* E2" := (MultiStep E1 E2).
adamc@160 619
adamc@160 620 Hint Constructors MultiStep.
adamc@160 621
adamc@254 622 (** A few basic properties of evaluation and values admit easy proofs. *)
adamc@254 623
adamc@160 624 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
adamc@160 625 E1 ==>* E2
adamc@160 626 -> E2 ==>* E3
adamc@160 627 -> E1 ==>* E3.
adamc@160 628 induction 1; eauto.
adamc@160 629 Qed.
adamc@160 630
adamc@160 631 Theorem Big_Val : forall t (E V : Exp t),
adamc@160 632 E ===> V
adamc@160 633 -> Val V.
adamc@160 634 induction 1; crush.
adamc@160 635 Qed.
adamc@160 636
adamc@160 637 Theorem Val_Big : forall t (V : Exp t),
adamc@160 638 Val V
adamc@160 639 -> V ===> V.
adamc@160 640 destruct 1; crush.
adamc@160 641 Qed.
adamc@160 642
adamc@160 643 Hint Resolve Big_Val Val_Big.
adamc@160 644
adamc@254 645 (** Another useful property deals with pushing multi-step evaluation inside of contexts. *)
adamc@254 646
adamc@162 647 Lemma Multi_Cong : forall t t' (C : Ctx t t'),
adamc@162 648 isCtx C
adamc@162 649 -> forall E E', E ==>* E'
adamc@162 650 -> C @ E ==>* C @ E'.
adamc@160 651 induction 2; crush; eauto.
adamc@160 652 Qed.
adamc@160 653
adamc@162 654 Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
adamc@162 655 isCtx C
adamc@162 656 -> E1 = C @ E
adamc@162 657 -> E2 = C @ E'
adamc@162 658 -> E ==>* E'
adamc@162 659 -> E1 ==>* E2.
adamc@162 660 crush; apply Multi_Cong; auto.
adamc@162 661 Qed.
adamc@162 662
adamc@162 663 Hint Resolve Multi_Cong'.
adamc@162 664
adamc@254 665 (** 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 666
adamc@162 667 Ltac mtrans E :=
adamc@162 668 match goal with
adamc@162 669 | [ |- E ==>* _ ] => fail 1
adamc@162 670 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
adamc@162 671 end.
adamc@160 672
adamc@254 673 (** 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 674
adamc@160 675 Theorem Big_Multi : forall t (E V : Exp t),
adamc@160 676 E ===> V
adamc@160 677 -> E ==>* V.
adamc@162 678 induction 1; crush; eauto;
adamc@162 679 repeat match goal with
adamc@162 680 | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
adamc@162 681 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
adamc@162 682 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
adamc@162 683 end.
adamc@160 684 Qed.
adamc@160 685
adamc@254 686 (** 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 687
adamc@160 688 Lemma Big_Val' : forall t (V1 V2 : Exp t),
adamc@160 689 Val V2
adamc@160 690 -> V1 = V2
adamc@160 691 -> V1 ===> V2.
adamc@160 692 crush.
adamc@160 693 Qed.
adamc@160 694
adamc@160 695 Hint Resolve Big_Val'.
adamc@160 696
adamc@254 697 (** 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 698
adamc@167 699 Ltac equate_conj F G :=
adamc@167 700 match constr:(F, G) with
adamc@167 701 | (_ ?x1, _ ?x2) => constr:(x1 = x2)
adamc@167 702 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
adamc@167 703 | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
adamc@222 704 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) =>
adamc@222 705 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
adamc@222 706 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) =>
adamc@222 707 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
adamc@167 708 end.
adamc@167 709
adamc@254 710 (** 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 711
adamc@167 712 Ltac my_crush :=
adamc@167 713 my_crush';
adamc@167 714 repeat (match goal with
adamc@167 715 | [ H : ?F = ?G |- _ ] =>
adamc@167 716 (let H' := fresh "H'" in
adamc@167 717 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
adamc@167 718 | discriminate || injection H'; clear H' ];
adamc@167 719 my_crush';
adamc@167 720 repeat match goal with
adamc@167 721 | [ H : context[fun _ => unit] |- _ ] => clear H
adamc@167 722 end;
adamc@167 723 match type of H with
adamc@167 724 | ?F = ?G =>
adamc@167 725 let ec := equate_conj F G in
adamc@167 726 let var := fresh "var" in
adamc@167 727 assert ec; [ intuition; unfold Exp; apply ext_eq; intro var;
adamc@167 728 assert (H' : F var = G var); try congruence;
adamc@167 729 match type of H' with
adamc@167 730 | ?X = ?Y =>
adamc@167 731 let X := eval hnf in X in
adamc@167 732 let Y := eval hnf in Y in
adamc@167 733 change (X = Y) in H'
adamc@167 734 end; injection H'; my_crush'; tauto
adamc@167 735 | intuition; subst ]
adamc@167 736 end);
adamc@167 737 clear H
adamc@167 738 end; my_crush');
adamc@167 739 my_crush'.
adamc@167 740
adamc@254 741 (** With that complicated tactic available, the proof of the main lemma is straightforward. *)
adamc@254 742
adamc@160 743 Lemma Multi_Big' : forall t (E E' : Exp t),
adamc@160 744 E ==> E'
adamc@160 745 -> forall E'', E' ===> E''
adamc@160 746 -> E ===> E''.
adamc@160 747 induction 1; crush; eauto;
adamc@160 748 match goal with
adamc@160 749 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
adamc@162 750 end;
adamc@162 751 match goal with
adamc@162 752 | [ H : isCtx _ |- _ ] => inversion H; my_crush; eauto
adamc@160 753 end.
adamc@160 754 Qed.
adamc@160 755
adamc@160 756 Hint Resolve Multi_Big'.
adamc@160 757
adamc@254 758 (** The other direction of the overall equivalence follows as an easy corollary. *)
adamc@254 759
adamc@160 760 Theorem Multi_Big : forall t (E V : Exp t),
adamc@160 761 E ==>* V
adamc@160 762 -> Val V
adamc@160 763 -> E ===> V.
adamc@160 764 induction 1; crush; eauto.
adamc@160 765 Qed.
adamc@169 766 (* end thide *)
adamc@254 767
adamc@254 768 (** 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. *)