Mercurial > cpdt > repo

annotate src/Hoas.v @ 253:0d77577e5ac0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PHOAS intro section
author Adam Chlipala <adamc@hcoop.net>
date Wed, 16 Dec 2009 11:33:53 -0500
parents 3c4ed57c9907
children e3c3b7ef5901
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@158 463 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
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@162 471 Inductive Ctx : type -> type -> Type :=
adamc@162 472 | AppCong1 : forall (dom ran : type),
adamc@162 473 Exp dom -> Ctx (dom --> ran) ran
adamc@162 474 | AppCong2 : forall (dom ran : type),
adamc@162 475 Exp (dom --> ran) -> Ctx dom ran
adamc@162 476 | PlusCong1 : Exp Nat -> Ctx Nat Nat
adamc@162 477 | PlusCong2 : Exp Nat -> Ctx Nat Nat.
adamc@162 478
adamc@162 479 Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop :=
adamc@162 480 | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X)
adamc@162 481 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F)
adamc@162 482 | IsPlus1 : forall E2, isCtx (PlusCong1 E2)
adamc@162 483 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).
adamc@162 484
adamc@162 485 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
adamc@222 486 match C with
adamc@162 487 | AppCong1 _ _ X => fun F => App F X
adamc@162 488 | AppCong2 _ _ F => fun X => App F X
adamc@162 489 | PlusCong1 E2 => fun E1 => Plus E1 E2
adamc@162 490 | PlusCong2 E1 => fun E2 => Plus E1 E2
adamc@162 491 end.
adamc@162 492
adamc@162 493 Infix "@" := plug (no associativity, at level 60).
adamc@162 494
adamc@158 495 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
adamc@158 496 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
adamc@160 497 Val X
adamc@160 498 -> App (Abs B) X ==> Subst X B
adamc@159 499 | Sum : forall n1 n2,
adamc@159 500 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
adamc@162 501 | Cong : forall t t' (C : Ctx t t') E E' E1,
adamc@162 502 isCtx C
adamc@162 503 -> E1 = C @ E
adamc@162 504 -> E ==> E'
adamc@162 505 -> E1 ==> C @ E'
adamc@159 506
adamc@158 507 where "E1 ==> E2" := (Step E1 E2).
adamc@158 508
adamc@162 509 Hint Constructors isCtx Step.
adamc@158 510
adamc@169 511 (* EX: Prove type soundness. *)
adamc@169 512
adamc@169 513 (* begin thide *)
adamc@158 514 Inductive Closed : forall t, Exp t -> Prop :=
adamc@164 515 | CConst : forall n,
adamc@164 516 Closed (Const n)
adamc@159 517 | CPlus : forall E1 E2,
adamc@159 518 Closed E1
adamc@159 519 -> Closed E2
adamc@159 520 -> Closed (Plus E1 E2)
adamc@158 521 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
adamc@158 522 Closed E1
adamc@158 523 -> Closed E2
adamc@158 524 -> Closed (App E1 E2)
adamc@158 525 | CAbs : forall dom ran (E1 : Exp1 dom ran),
adamc@158 526 Closed (Abs E1).
adamc@158 527
adamc@158 528 Axiom closed : forall t (E : Exp t), Closed E.
adamc@158 529
adamc@160 530 Ltac my_crush' :=
adamc@167 531 crush;
adamc@158 532 repeat (match goal with
adamc@158 533 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
adamc@167 534 end; crush).
adamc@160 535
adamc@162 536 Hint Extern 1 (_ = _ @ _) => simpl.
adamc@162 537
adamc@158 538 Lemma progress' : forall t (E : Exp t),
adamc@158 539 Closed E
adamc@158 540 -> Val E \/ exists E', E ==> E'.
adamc@158 541 induction 1; crush;
adamc@159 542 repeat match goal with
adamc@167 543 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush'
adamc@162 544 end; eauto 6.
adamc@158 545 Qed.
adamc@158 546
adamc@158 547 Theorem progress : forall t (E : Exp t),
adamc@158 548 Val E \/ exists E', E ==> E'.
adamc@158 549 intros; apply progress'; apply closed.
adamc@158 550 Qed.
adamc@169 551 (* end thide *)
adamc@158 552
adamc@160 553
adamc@160 554 (** * Big-Step Semantics *)
adamc@160 555
adamc@160 556 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
adamc@160 557
adamc@160 558 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 559 | SConst : forall n,
adamc@160 560 Const n ===> Const n
adamc@160 561 | SPlus : forall E1 E2 n1 n2,
adamc@160 562 E1 ===> Const n1
adamc@160 563 -> E2 ===> Const n2
adamc@160 564 -> Plus E1 E2 ===> Const (n1 + n2)
adamc@160 565
adamc@160 566 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
adamc@160 567 E1 ===> Abs B
adamc@160 568 -> E2 ===> V2
adamc@160 569 -> Subst V2 B ===> V
adamc@160 570 -> App E1 E2 ===> V
adamc@160 571 | SAbs : forall dom ran (B : Exp1 dom ran),
adamc@160 572 Abs B ===> Abs B
adamc@160 573
adamc@160 574 where "E1 ===> E2" := (BigStep E1 E2).
adamc@160 575
adamc@160 576 Hint Constructors BigStep.
adamc@160 577
adamc@169 578 (* EX: Prove the equivalence of the small- and big-step semantics. *)
adamc@169 579
adamc@169 580 (* begin thide *)
adamc@160 581 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
adamc@160 582
adamc@160 583 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 584 | Done : forall t (E : Exp t), E ==>* E
adamc@160 585 | OneStep : forall t (E E' E'' : Exp t),
adamc@160 586 E ==> E'
adamc@160 587 -> E' ==>* E''
adamc@160 588 -> E ==>* E''
adamc@160 589
adamc@160 590 where "E1 ==>* E2" := (MultiStep E1 E2).
adamc@160 591
adamc@160 592 Hint Constructors MultiStep.
adamc@160 593
adamc@160 594 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
adamc@160 595 E1 ==>* E2
adamc@160 596 -> E2 ==>* E3
adamc@160 597 -> E1 ==>* E3.
adamc@160 598 induction 1; eauto.
adamc@160 599 Qed.
adamc@160 600
adamc@160 601 Theorem Big_Val : forall t (E V : Exp t),
adamc@160 602 E ===> V
adamc@160 603 -> Val V.
adamc@160 604 induction 1; crush.
adamc@160 605 Qed.
adamc@160 606
adamc@160 607 Theorem Val_Big : forall t (V : Exp t),
adamc@160 608 Val V
adamc@160 609 -> V ===> V.
adamc@160 610 destruct 1; crush.
adamc@160 611 Qed.
adamc@160 612
adamc@160 613 Hint Resolve Big_Val Val_Big.
adamc@160 614
adamc@162 615 Lemma Multi_Cong : forall t t' (C : Ctx t t'),
adamc@162 616 isCtx C
adamc@162 617 -> forall E E', E ==>* E'
adamc@162 618 -> C @ E ==>* C @ E'.
adamc@160 619 induction 2; crush; eauto.
adamc@160 620 Qed.
adamc@160 621
adamc@162 622 Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
adamc@162 623 isCtx C
adamc@162 624 -> E1 = C @ E
adamc@162 625 -> E2 = C @ E'
adamc@162 626 -> E ==>* E'
adamc@162 627 -> E1 ==>* E2.
adamc@162 628 crush; apply Multi_Cong; auto.
adamc@162 629 Qed.
adamc@162 630
adamc@162 631 Hint Resolve Multi_Cong'.
adamc@162 632
adamc@162 633 Ltac mtrans E :=
adamc@162 634 match goal with
adamc@162 635 | [ |- E ==>* _ ] => fail 1
adamc@162 636 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
adamc@162 637 end.
adamc@160 638
adamc@160 639 Theorem Big_Multi : forall t (E V : Exp t),
adamc@160 640 E ===> V
adamc@160 641 -> E ==>* V.
adamc@162 642 induction 1; crush; eauto;
adamc@162 643 repeat match goal with
adamc@162 644 | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
adamc@162 645 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
adamc@162 646 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
adamc@162 647 end.
adamc@160 648 Qed.
adamc@160 649
adamc@160 650 Lemma Big_Val' : forall t (V1 V2 : Exp t),
adamc@160 651 Val V2
adamc@160 652 -> V1 = V2
adamc@160 653 -> V1 ===> V2.
adamc@160 654 crush.
adamc@160 655 Qed.
adamc@160 656
adamc@160 657 Hint Resolve Big_Val'.
adamc@160 658
adamc@167 659 Ltac equate_conj F G :=
adamc@167 660 match constr:(F, G) with
adamc@167 661 | (_ ?x1, _ ?x2) => constr:(x1 = x2)
adamc@167 662 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
adamc@167 663 | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
adamc@222 664 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) =>
adamc@222 665 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
adamc@222 666 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) =>
adamc@222 667 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
adamc@167 668 end.
adamc@167 669
adamc@167 670 Ltac my_crush :=
adamc@167 671 my_crush';
adamc@167 672 repeat (match goal with
adamc@167 673 | [ H : ?F = ?G |- _ ] =>
adamc@167 674 (let H' := fresh "H'" in
adamc@167 675 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
adamc@167 676 | discriminate || injection H'; clear H' ];
adamc@167 677 my_crush';
adamc@167 678 repeat match goal with
adamc@167 679 | [ H : context[fun _ => unit] |- _ ] => clear H
adamc@167 680 end;
adamc@167 681 match type of H with
adamc@167 682 | ?F = ?G =>
adamc@167 683 let ec := equate_conj F G in
adamc@167 684 let var := fresh "var" in
adamc@167 685 assert ec; [ intuition; unfold Exp; apply ext_eq; intro var;
adamc@167 686 assert (H' : F var = G var); try congruence;
adamc@167 687 match type of H' with
adamc@167 688 | ?X = ?Y =>
adamc@167 689 let X := eval hnf in X in
adamc@167 690 let Y := eval hnf in Y in
adamc@167 691 change (X = Y) in H'
adamc@167 692 end; injection H'; my_crush'; tauto
adamc@167 693 | intuition; subst ]
adamc@167 694 end);
adamc@167 695 clear H
adamc@167 696 end; my_crush');
adamc@167 697 my_crush'.
adamc@167 698
adamc@160 699 Lemma Multi_Big' : forall t (E E' : Exp t),
adamc@160 700 E ==> E'
adamc@160 701 -> forall E'', E' ===> E''
adamc@160 702 -> E ===> E''.
adamc@160 703 induction 1; crush; eauto;
adamc@160 704 match goal with
adamc@160 705 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
adamc@162 706 end;
adamc@162 707 match goal with
adamc@162 708 | [ H : isCtx _ |- _ ] => inversion H; my_crush; eauto
adamc@160 709 end.
adamc@160 710 Qed.
adamc@160 711
adamc@160 712 Hint Resolve Multi_Big'.
adamc@160 713
adamc@160 714 Theorem Multi_Big : forall t (E V : Exp t),
adamc@160 715 E ==>* V
adamc@160 716 -> Val V
adamc@160 717 -> E ===> V.
adamc@160 718 induction 1; crush; eauto.
adamc@160 719 Qed.
adamc@169 720 (* end thide *)