Mercurial > cpdt > repo

annotate src/Hoas.v @ 252:3c4ed57c9907

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Hoas intro
author Adam Chlipala <adamc@hcoop.net>
date Wed, 16 Dec 2009 10:39:22 -0500
parents 13620dfd5f97
children 0d77577e5ac0
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@158 121 Inductive type : Type :=
adamc@159 122 | Nat : type
adamc@158 123 | Arrow : type -> type -> type.
adamc@158 124
adamc@158 125 Infix "-->" := Arrow (right associativity, at level 60).
adamc@158 126
adamc@158 127 Section exp.
adamc@158 128 Variable var : type -> Type.
adamc@158 129
adamc@158 130 Inductive exp : type -> Type :=
adamc@159 131 | Const' : nat -> exp Nat
adamc@159 132 | Plus' : exp Nat -> exp Nat -> exp Nat
adamc@159 133
adamc@158 134 | Var : forall t, var t -> exp t
adamc@158 135 | App' : forall dom ran, exp (dom --> ran) -> exp dom -> exp ran
adamc@158 136 | Abs' : forall dom ran, (var dom -> exp ran) -> exp (dom --> ran).
adamc@158 137 End exp.
adamc@158 138
adamc@158 139 Implicit Arguments Const' [var].
adamc@158 140 Implicit Arguments Var [var t].
adamc@158 141 Implicit Arguments Abs' [var dom ran].
adamc@158 142
adamc@158 143 Definition Exp t := forall var, exp var t.
adamc@169 144 (* begin thide *)
adamc@158 145 Definition Exp1 t1 t2 := forall var, var t1 -> exp var t2.
adamc@158 146
adamc@159 147 Definition Const (n : nat) : Exp Nat :=
adamc@159 148 fun _ => Const' n.
adamc@159 149 Definition Plus (E1 E2 : Exp Nat) : Exp Nat :=
adamc@159 150 fun _ => Plus' (E1 _) (E2 _).
adamc@158 151 Definition App dom ran (F : Exp (dom --> ran)) (X : Exp dom) : Exp ran :=
adamc@158 152 fun _ => App' (F _) (X _).
adamc@158 153 Definition Abs dom ran (B : Exp1 dom ran) : Exp (dom --> ran) :=
adamc@158 154 fun _ => Abs' (B _).
adamc@169 155 (* end thide *)
adamc@169 156
adamc@169 157 (* EX: Define appropriate shorthands, so that these definitions type-check. *)
adamc@158 158
adamc@166 159 Definition zero := Const 0.
adamc@166 160 Definition one := Const 1.
adamc@166 161 Definition one_again := Plus zero one.
adamc@166 162 Definition ident : Exp (Nat --> Nat) := Abs (fun _ X => Var X).
adamc@166 163 Definition app_ident := App ident one_again.
adamc@166 164 Definition app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ =>
adamc@166 165 Abs' (fun f => Abs' (fun x => App' (Var f) (Var x))).
adamc@166 166 Definition app_ident' := App (App app ident) one_again.
adamc@166 167
adamc@169 168 (* EX: Define a function to count the number of variable occurrences in an [Exp]. *)
adamc@169 169
adamc@169 170 (* begin thide *)
adamc@222 171 Fixpoint countVars t (e : exp (fun _ => unit) t) : nat :=
adamc@166 172 match e with
adamc@166 173 | Const' _ => 0
adamc@166 174 | Plus' e1 e2 => countVars e1 + countVars e2
adamc@166 175 | Var _ _ => 1
adamc@166 176 | App' _ _ e1 e2 => countVars e1 + countVars e2
adamc@166 177 | Abs' _ _ e' => countVars (e' tt)
adamc@166 178 end.
adamc@166 179
adamc@166 180 Definition CountVars t (E : Exp t) : nat := countVars (E _).
adamc@169 181 (* end thide *)
adamc@166 182
adamc@166 183 Eval compute in CountVars zero.
adamc@166 184 Eval compute in CountVars one.
adamc@166 185 Eval compute in CountVars one_again.
adamc@166 186 Eval compute in CountVars ident.
adamc@166 187 Eval compute in CountVars app_ident.
adamc@166 188 Eval compute in CountVars app.
adamc@166 189 Eval compute in CountVars app_ident'.
adamc@166 190
adamc@169 191 (* EX: Define a function to count the number of occurrences of a single distinguished variable. *)
adamc@169 192
adamc@169 193 (* begin thide *)
adamc@222 194 Fixpoint countOne t (e : exp (fun _ => bool) t) : nat :=
adamc@166 195 match e with
adamc@166 196 | Const' _ => 0
adamc@166 197 | Plus' e1 e2 => countOne e1 + countOne e2
adamc@166 198 | Var _ true => 1
adamc@166 199 | Var _ false => 0
adamc@166 200 | App' _ _ e1 e2 => countOne e1 + countOne e2
adamc@166 201 | Abs' _ _ e' => countOne (e' false)
adamc@166 202 end.
adamc@166 203
adamc@166 204 Definition CountOne t1 t2 (E : Exp1 t1 t2) : nat :=
adamc@166 205 countOne (E _ true).
adamc@169 206 (* end thide *)
adamc@166 207
adamc@166 208 Definition ident1 : Exp1 Nat Nat := fun _ X => Var X.
adamc@166 209 Definition add_self : Exp1 Nat Nat := fun _ X => Plus' (Var X) (Var X).
adamc@166 210 Definition app_zero : Exp1 (Nat --> Nat) Nat := fun _ X => App' (Var X) (Const' 0).
adamc@166 211 Definition app_ident1 : Exp1 Nat Nat := fun _ X => App' (Abs' (fun Y => Var Y)) (Var X).
adamc@166 212
adamc@166 213 Eval compute in CountOne ident1.
adamc@166 214 Eval compute in CountOne add_self.
adamc@166 215 Eval compute in CountOne app_zero.
adamc@166 216 Eval compute in CountOne app_ident1.
adamc@166 217
adamc@169 218 (* EX: Define a function to pretty-print [Exp]s as strings. *)
adamc@169 219
adamc@169 220 (* begin thide *)
adamc@166 221 Section ToString.
adamc@166 222 Open Scope string_scope.
adamc@166 223
adamc@166 224 Fixpoint natToString (n : nat) : string :=
adamc@166 225 match n with
adamc@166 226 | O => "O"
adamc@166 227 | S n' => "S(" ++ natToString n' ++ ")"
adamc@166 228 end.
adamc@166 229
adamc@222 230 Fixpoint toString t (e : exp (fun _ => string) t) (cur : string) : string * string :=
adamc@166 231 match e with
adamc@166 232 | Const' n => (cur, natToString n)
adamc@166 233 | Plus' e1 e2 =>
adamc@166 234 let (cur', s1) := toString e1 cur in
adamc@166 235 let (cur'', s2) := toString e2 cur' in
adamc@166 236 (cur'', "(" ++ s1 ++ ") + (" ++ s2 ++ ")")
adamc@166 237 | Var _ s => (cur, s)
adamc@166 238 | App' _ _ e1 e2 =>
adamc@166 239 let (cur', s1) := toString e1 cur in
adamc@166 240 let (cur'', s2) := toString e2 cur' in
adamc@166 241 (cur'', "(" ++ s1 ++ ") (" ++ s2 ++ ")")
adamc@166 242 | Abs' _ _ e' =>
adamc@166 243 let (cur', s) := toString (e' cur) (cur ++ "'") in
adamc@166 244 (cur', "(\" ++ cur ++ ", " ++ s ++ ")")
adamc@166 245 end.
adamc@166 246
adamc@166 247 Definition ToString t (E : Exp t) : string := snd (toString (E _) "x").
adamc@166 248 End ToString.
adamc@169 249 (* end thide *)
adamc@166 250
adamc@166 251 Eval compute in ToString zero.
adamc@166 252 Eval compute in ToString one.
adamc@166 253 Eval compute in ToString one_again.
adamc@166 254 Eval compute in ToString ident.
adamc@166 255 Eval compute in ToString app_ident.
adamc@166 256 Eval compute in ToString app.
adamc@166 257 Eval compute in ToString app_ident'.
adamc@166 258
adamc@169 259 (* EX: Define a substitution function. *)
adamc@169 260
adamc@169 261 (* begin thide *)
adamc@158 262 Section flatten.
adamc@158 263 Variable var : type -> Type.
adamc@158 264
adamc@222 265 Fixpoint flatten t (e : exp (exp var) t) : exp var t :=
adamc@222 266 match e with
adamc@159 267 | Const' n => Const' n
adamc@159 268 | Plus' e1 e2 => Plus' (flatten e1) (flatten e2)
adamc@158 269 | Var _ e' => e'
adamc@158 270 | App' _ _ e1 e2 => App' (flatten e1) (flatten e2)
adamc@158 271 | Abs' _ _ e' => Abs' (fun x => flatten (e' (Var x)))
adamc@158 272 end.
adamc@158 273 End flatten.
adamc@158 274
adamc@158 275 Definition Subst t1 t2 (E1 : Exp t1) (E2 : Exp1 t1 t2) : Exp t2 := fun _ =>
adamc@158 276 flatten (E2 _ (E1 _)).
adamc@169 277 (* end thide *)
adamc@158 278
adamc@166 279 Eval compute in Subst one ident1.
adamc@166 280 Eval compute in Subst one add_self.
adamc@166 281 Eval compute in Subst ident app_zero.
adamc@166 282 Eval compute in Subst one app_ident1.
adamc@166 283
adamc@158 284
adamc@158 285 (** * A Type Soundness Proof *)
adamc@158 286
adamc@158 287 Reserved Notation "E1 ==> E2" (no associativity, at level 90).
adamc@158 288
adamc@158 289 Inductive Val : forall t, Exp t -> Prop :=
adamc@159 290 | VConst : forall n, Val (Const n)
adamc@158 291 | VAbs : forall dom ran (B : Exp1 dom ran), Val (Abs B).
adamc@158 292
adamc@158 293 Hint Constructors Val.
adamc@158 294
adamc@162 295 Inductive Ctx : type -> type -> Type :=
adamc@162 296 | AppCong1 : forall (dom ran : type),
adamc@162 297 Exp dom -> Ctx (dom --> ran) ran
adamc@162 298 | AppCong2 : forall (dom ran : type),
adamc@162 299 Exp (dom --> ran) -> Ctx dom ran
adamc@162 300 | PlusCong1 : Exp Nat -> Ctx Nat Nat
adamc@162 301 | PlusCong2 : Exp Nat -> Ctx Nat Nat.
adamc@162 302
adamc@162 303 Inductive isCtx : forall t1 t2, Ctx t1 t2 -> Prop :=
adamc@162 304 | IsApp1 : forall dom ran (X : Exp dom), isCtx (AppCong1 ran X)
adamc@162 305 | IsApp2 : forall dom ran (F : Exp (dom --> ran)), Val F -> isCtx (AppCong2 F)
adamc@162 306 | IsPlus1 : forall E2, isCtx (PlusCong1 E2)
adamc@162 307 | IsPlus2 : forall E1, Val E1 -> isCtx (PlusCong2 E1).
adamc@162 308
adamc@162 309 Definition plug t1 t2 (C : Ctx t1 t2) : Exp t1 -> Exp t2 :=
adamc@222 310 match C with
adamc@162 311 | AppCong1 _ _ X => fun F => App F X
adamc@162 312 | AppCong2 _ _ F => fun X => App F X
adamc@162 313 | PlusCong1 E2 => fun E1 => Plus E1 E2
adamc@162 314 | PlusCong2 E1 => fun E2 => Plus E1 E2
adamc@162 315 end.
adamc@162 316
adamc@162 317 Infix "@" := plug (no associativity, at level 60).
adamc@162 318
adamc@158 319 Inductive Step : forall t, Exp t -> Exp t -> Prop :=
adamc@158 320 | Beta : forall dom ran (B : Exp1 dom ran) (X : Exp dom),
adamc@160 321 Val X
adamc@160 322 -> App (Abs B) X ==> Subst X B
adamc@159 323 | Sum : forall n1 n2,
adamc@159 324 Plus (Const n1) (Const n2) ==> Const (n1 + n2)
adamc@162 325 | Cong : forall t t' (C : Ctx t t') E E' E1,
adamc@162 326 isCtx C
adamc@162 327 -> E1 = C @ E
adamc@162 328 -> E ==> E'
adamc@162 329 -> E1 ==> C @ E'
adamc@159 330
adamc@158 331 where "E1 ==> E2" := (Step E1 E2).
adamc@158 332
adamc@162 333 Hint Constructors isCtx Step.
adamc@158 334
adamc@169 335 (* EX: Prove type soundness. *)
adamc@169 336
adamc@169 337 (* begin thide *)
adamc@158 338 Inductive Closed : forall t, Exp t -> Prop :=
adamc@164 339 | CConst : forall n,
adamc@164 340 Closed (Const n)
adamc@159 341 | CPlus : forall E1 E2,
adamc@159 342 Closed E1
adamc@159 343 -> Closed E2
adamc@159 344 -> Closed (Plus E1 E2)
adamc@158 345 | CApp : forall dom ran (E1 : Exp (dom --> ran)) E2,
adamc@158 346 Closed E1
adamc@158 347 -> Closed E2
adamc@158 348 -> Closed (App E1 E2)
adamc@158 349 | CAbs : forall dom ran (E1 : Exp1 dom ran),
adamc@158 350 Closed (Abs E1).
adamc@158 351
adamc@158 352 Axiom closed : forall t (E : Exp t), Closed E.
adamc@158 353
adamc@160 354 Ltac my_crush' :=
adamc@167 355 crush;
adamc@158 356 repeat (match goal with
adamc@158 357 | [ H : _ |- _ ] => generalize (inj_pairT2 _ _ _ _ _ H); clear H
adamc@167 358 end; crush).
adamc@160 359
adamc@162 360 Hint Extern 1 (_ = _ @ _) => simpl.
adamc@162 361
adamc@158 362 Lemma progress' : forall t (E : Exp t),
adamc@158 363 Closed E
adamc@158 364 -> Val E \/ exists E', E ==> E'.
adamc@158 365 induction 1; crush;
adamc@159 366 repeat match goal with
adamc@167 367 | [ H : Val _ |- _ ] => inversion H; []; clear H; my_crush'
adamc@162 368 end; eauto 6.
adamc@158 369 Qed.
adamc@158 370
adamc@158 371 Theorem progress : forall t (E : Exp t),
adamc@158 372 Val E \/ exists E', E ==> E'.
adamc@158 373 intros; apply progress'; apply closed.
adamc@158 374 Qed.
adamc@169 375 (* end thide *)
adamc@158 376
adamc@160 377
adamc@160 378 (** * Big-Step Semantics *)
adamc@160 379
adamc@160 380 Reserved Notation "E1 ===> E2" (no associativity, at level 90).
adamc@160 381
adamc@160 382 Inductive BigStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 383 | SConst : forall n,
adamc@160 384 Const n ===> Const n
adamc@160 385 | SPlus : forall E1 E2 n1 n2,
adamc@160 386 E1 ===> Const n1
adamc@160 387 -> E2 ===> Const n2
adamc@160 388 -> Plus E1 E2 ===> Const (n1 + n2)
adamc@160 389
adamc@160 390 | SApp : forall dom ran (E1 : Exp (dom --> ran)) E2 B V2 V,
adamc@160 391 E1 ===> Abs B
adamc@160 392 -> E2 ===> V2
adamc@160 393 -> Subst V2 B ===> V
adamc@160 394 -> App E1 E2 ===> V
adamc@160 395 | SAbs : forall dom ran (B : Exp1 dom ran),
adamc@160 396 Abs B ===> Abs B
adamc@160 397
adamc@160 398 where "E1 ===> E2" := (BigStep E1 E2).
adamc@160 399
adamc@160 400 Hint Constructors BigStep.
adamc@160 401
adamc@169 402 (* EX: Prove the equivalence of the small- and big-step semantics. *)
adamc@169 403
adamc@169 404 (* begin thide *)
adamc@160 405 Reserved Notation "E1 ==>* E2" (no associativity, at level 90).
adamc@160 406
adamc@160 407 Inductive MultiStep : forall t, Exp t -> Exp t -> Prop :=
adamc@160 408 | Done : forall t (E : Exp t), E ==>* E
adamc@160 409 | OneStep : forall t (E E' E'' : Exp t),
adamc@160 410 E ==> E'
adamc@160 411 -> E' ==>* E''
adamc@160 412 -> E ==>* E''
adamc@160 413
adamc@160 414 where "E1 ==>* E2" := (MultiStep E1 E2).
adamc@160 415
adamc@160 416 Hint Constructors MultiStep.
adamc@160 417
adamc@160 418 Theorem MultiStep_trans : forall t (E1 E2 E3 : Exp t),
adamc@160 419 E1 ==>* E2
adamc@160 420 -> E2 ==>* E3
adamc@160 421 -> E1 ==>* E3.
adamc@160 422 induction 1; eauto.
adamc@160 423 Qed.
adamc@160 424
adamc@160 425 Theorem Big_Val : forall t (E V : Exp t),
adamc@160 426 E ===> V
adamc@160 427 -> Val V.
adamc@160 428 induction 1; crush.
adamc@160 429 Qed.
adamc@160 430
adamc@160 431 Theorem Val_Big : forall t (V : Exp t),
adamc@160 432 Val V
adamc@160 433 -> V ===> V.
adamc@160 434 destruct 1; crush.
adamc@160 435 Qed.
adamc@160 436
adamc@160 437 Hint Resolve Big_Val Val_Big.
adamc@160 438
adamc@162 439 Lemma Multi_Cong : forall t t' (C : Ctx t t'),
adamc@162 440 isCtx C
adamc@162 441 -> forall E E', E ==>* E'
adamc@162 442 -> C @ E ==>* C @ E'.
adamc@160 443 induction 2; crush; eauto.
adamc@160 444 Qed.
adamc@160 445
adamc@162 446 Lemma Multi_Cong' : forall t t' (C : Ctx t t') E1 E2 E E',
adamc@162 447 isCtx C
adamc@162 448 -> E1 = C @ E
adamc@162 449 -> E2 = C @ E'
adamc@162 450 -> E ==>* E'
adamc@162 451 -> E1 ==>* E2.
adamc@162 452 crush; apply Multi_Cong; auto.
adamc@162 453 Qed.
adamc@162 454
adamc@162 455 Hint Resolve Multi_Cong'.
adamc@162 456
adamc@162 457 Ltac mtrans E :=
adamc@162 458 match goal with
adamc@162 459 | [ |- E ==>* _ ] => fail 1
adamc@162 460 | _ => apply MultiStep_trans with E; [ solve [ eauto ] | eauto ]
adamc@162 461 end.
adamc@160 462
adamc@160 463 Theorem Big_Multi : forall t (E V : Exp t),
adamc@160 464 E ===> V
adamc@160 465 -> E ==>* V.
adamc@162 466 induction 1; crush; eauto;
adamc@162 467 repeat match goal with
adamc@162 468 | [ n1 : _, E2 : _ |- _ ] => mtrans (Plus (Const n1) E2)
adamc@162 469 | [ n1 : _, n2 : _ |- _ ] => mtrans (Plus (Const n1) (Const n2))
adamc@162 470 | [ B : _, E2 : _ |- _ ] => mtrans (App (Abs B) E2)
adamc@162 471 end.
adamc@160 472 Qed.
adamc@160 473
adamc@160 474 Lemma Big_Val' : forall t (V1 V2 : Exp t),
adamc@160 475 Val V2
adamc@160 476 -> V1 = V2
adamc@160 477 -> V1 ===> V2.
adamc@160 478 crush.
adamc@160 479 Qed.
adamc@160 480
adamc@160 481 Hint Resolve Big_Val'.
adamc@160 482
adamc@167 483 Ltac equate_conj F G :=
adamc@167 484 match constr:(F, G) with
adamc@167 485 | (_ ?x1, _ ?x2) => constr:(x1 = x2)
adamc@167 486 | (_ ?x1 ?y1, _ ?x2 ?y2) => constr:(x1 = x2 /\ y1 = y2)
adamc@167 487 | (_ ?x1 ?y1 ?z1, _ ?x2 ?y2 ?z2) => constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2)
adamc@222 488 | (_ ?x1 ?y1 ?z1 ?u1, _ ?x2 ?y2 ?z2 ?u2) =>
adamc@222 489 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2)
adamc@222 490 | (_ ?x1 ?y1 ?z1 ?u1 ?v1, _ ?x2 ?y2 ?z2 ?u2 ?v2) =>
adamc@222 491 constr:(x1 = x2 /\ y1 = y2 /\ z1 = z2 /\ u1 = u2 /\ v1 = v2)
adamc@167 492 end.
adamc@167 493
adamc@167 494 Ltac my_crush :=
adamc@167 495 my_crush';
adamc@167 496 repeat (match goal with
adamc@167 497 | [ H : ?F = ?G |- _ ] =>
adamc@167 498 (let H' := fresh "H'" in
adamc@167 499 assert (H' : F (fun _ => unit) = G (fun _ => unit)); [ congruence
adamc@167 500 | discriminate || injection H'; clear H' ];
adamc@167 501 my_crush';
adamc@167 502 repeat match goal with
adamc@167 503 | [ H : context[fun _ => unit] |- _ ] => clear H
adamc@167 504 end;
adamc@167 505 match type of H with
adamc@167 506 | ?F = ?G =>
adamc@167 507 let ec := equate_conj F G in
adamc@167 508 let var := fresh "var" in
adamc@167 509 assert ec; [ intuition; unfold Exp; apply ext_eq; intro var;
adamc@167 510 assert (H' : F var = G var); try congruence;
adamc@167 511 match type of H' with
adamc@167 512 | ?X = ?Y =>
adamc@167 513 let X := eval hnf in X in
adamc@167 514 let Y := eval hnf in Y in
adamc@167 515 change (X = Y) in H'
adamc@167 516 end; injection H'; my_crush'; tauto
adamc@167 517 | intuition; subst ]
adamc@167 518 end);
adamc@167 519 clear H
adamc@167 520 end; my_crush');
adamc@167 521 my_crush'.
adamc@167 522
adamc@160 523 Lemma Multi_Big' : forall t (E E' : Exp t),
adamc@160 524 E ==> E'
adamc@160 525 -> forall E'', E' ===> E''
adamc@160 526 -> E ===> E''.
adamc@160 527 induction 1; crush; eauto;
adamc@160 528 match goal with
adamc@160 529 | [ H : _ ===> _ |- _ ] => inversion H; my_crush; eauto
adamc@162 530 end;
adamc@162 531 match goal with
adamc@162 532 | [ H : isCtx _ |- _ ] => inversion H; my_crush; eauto
adamc@160 533 end.
adamc@160 534 Qed.
adamc@160 535
adamc@160 536 Hint Resolve Multi_Big'.
adamc@160 537
adamc@160 538 Theorem Multi_Big : forall t (E V : Exp t),
adamc@160 539 E ==>* V
adamc@160 540 -> Val V
adamc@160 541 -> E ===> V.
adamc@160 542 induction 1; crush; eauto.
adamc@160 543 Qed.
adamc@169 544 (* end thide *)