Mercurial > cpdt > repo

annotate src/Interps.v @ 290:758778c0468c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
PC comments for FirstOrder
author Adam Chlipala <adam@chlipala.net>
date Wed, 10 Nov 2010 15:37:01 -0500
parents 05250878e4ca
children 2c88fc1dbe33
rev   line source
adamc@223 1 (* Copyright (c) 2008-2009, Adam Chlipala
adamc@170 2 *
adamc@170 3 * This work is licensed under a
adamc@170 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
adamc@170 5 * Unported License.
adamc@170 6 * The license text is available at:
adamc@170 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
adamc@170 8 *)
adamc@170 9
adamc@170 10 (* begin hide *)
adamc@170 11 Require Import String List.
adamc@170 12
adamc@204 13 Require Import Axioms Tactics.
adamc@170 14
adamc@170 15 Set Implicit Arguments.
adamc@170 16 (* end hide *)
adamc@170 17
adamc@170 18
adamc@170 19 (** %\chapter{Type-Theoretic Interpreters}% *)
adamc@170 20
adamc@255 21 (** Throughout this book, we have given semantics for programming languages via executable interpreters written in Gallina. PHOAS is quite compatible with that model, when we want to formalize many of the wide variety of interesting non-Turing-complete programming languages. Most such languages have very straightforward elaborations into Gallina. In this chapter, we show how to extend our past approach to higher-order languages encoded with PHOAS, and we show how simple program transformations may be proved correct with respect to these elaborative semantics. *)
adamc@170 22
adamc@170 23
adamc@170 24 (** * Simply-Typed Lambda Calculus *)
adamc@170 25
adamc@255 26 (** We begin with a copy of last chapter's encoding of the syntax of simply-typed lambda calculus with natural numbers and addition. The primes at the ends of constructor names are gone, since here our primary subject is [exp]s instead of [Exp]s. *)
adamc@255 27
adamc@170 28 Module STLC.
adamc@170 29 Inductive type : Type :=
adamc@170 30 | Nat : type
adamc@170 31 | Arrow : type -> type -> type.
adamc@170 32
adamc@170 33 Infix "-->" := Arrow (right associativity, at level 60).
adamc@170 34
adamc@170 35 Section vars.
adamc@170 36 Variable var : type -> Type.
adamc@170 37
adamc@170 38 Inductive exp : type -> Type :=
adamc@170 39 | Var : forall t,
adamc@170 40 var t
adamc@170 41 -> exp t
adamc@170 42
adamc@170 43 | Const : nat -> exp Nat
adamc@170 44 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@170 45
adamc@170 46 | App : forall t1 t2,
adamc@170 47 exp (t1 --> t2)
adamc@170 48 -> exp t1
adamc@170 49 -> exp t2
adamc@170 50 | Abs : forall t1 t2,
adamc@170 51 (var t1 -> exp t2)
adamc@170 52 -> exp (t1 --> t2).
adamc@170 53 End vars.
adamc@170 54
adamc@170 55 Definition Exp t := forall var, exp var t.
adamc@170 56
adamc@170 57 Implicit Arguments Var [var t].
adamc@170 58 Implicit Arguments Const [var].
adamc@170 59 Implicit Arguments Plus [var].
adamc@170 60 Implicit Arguments App [var t1 t2].
adamc@170 61 Implicit Arguments Abs [var t1 t2].
adamc@170 62
adamc@255 63 (** The definitions that follow will be easier to read if we define some parsing notations for the constructors. *)
adamc@255 64
adamc@170 65 Notation "# v" := (Var v) (at level 70).
adamc@170 66
adamc@170 67 Notation "^ n" := (Const n) (at level 70).
adamc@171 68 Infix "+^" := Plus (left associativity, at level 79).
adamc@170 69
adamc@170 70 Infix "@" := App (left associativity, at level 77).
adamc@170 71 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@170 72 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@170 73
adamc@255 74 (** A few examples will be useful for testing the functions we will write. *)
adamc@255 75
adamc@255 76 Example zero : Exp Nat := fun _ => ^0.
adamc@255 77 Example one : Exp Nat := fun _ => ^1.
adamc@255 78 Example zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@255 79 Example ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@255 80 Example app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@255 81 Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => \f, \x, #f @ #x.
adamc@255 82 Example app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@172 83
adamc@174 84 (* EX: Define an interpreter for [Exp]s. *)
adamc@174 85
adamc@174 86 (* begin thide *)
adamc@255 87 (** To write our interpreter, we must first interpret object language types as meta language types. *)
adamc@255 88
adamc@170 89 Fixpoint typeDenote (t : type) : Set :=
adamc@170 90 match t with
adamc@170 91 | Nat => nat
adamc@170 92 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@170 93 end.
adamc@170 94
adamc@255 95 (** The crucial trick of the expression interpreter is to represent variables using the [typeDenote] function. Due to limitations in Coq's syntax extension system, we cannot take advantage of some of our notations when they appear in patterns, so, to be consistent, in patterns we avoid notations altogether. *)
adamc@255 96
adamc@223 97 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@223 98 match e with
adamc@170 99 | Var _ v => v
adamc@170 100
adamc@170 101 | Const n => n
adamc@170 102 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@170 103
adamc@170 104 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@170 105 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@170 106 end.
adamc@170 107
adamc@170 108 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174 109 (* end thide *)
adamc@170 110
adamc@255 111 (** Some tests establish that [ExpDenote] produces Gallina terms like we might write manually. *)
adamc@255 112
adamc@172 113 Eval compute in ExpDenote zero.
adamc@255 114 (** %\vspace{-.15in}% [[
adamc@255 115 = 0
adamc@255 116 : typeDenote Nat
adamc@255 117 ]] *)
adamc@255 118
adamc@172 119 Eval compute in ExpDenote one.
adamc@255 120 (** %\vspace{-.15in}% [[
adamc@255 121 = 1
adamc@255 122 : typeDenote Nat
adamc@255 123 ]] *)
adamc@255 124
adamc@172 125 Eval compute in ExpDenote zpo.
adamc@255 126 (** %\vspace{-.15in}% [[
adamc@255 127 = 1
adamc@255 128 : typeDenote Nat
adamc@255 129 ]] *)
adamc@255 130
adamc@172 131 Eval compute in ExpDenote ident.
adamc@255 132 (** %\vspace{-.15in}% [[
adamc@255 133 = fun x : nat => x
adamc@255 134 : typeDenote (Nat --> Nat)
adamc@255 135 ]] *)
adamc@255 136
adamc@172 137 Eval compute in ExpDenote app_ident.
adamc@255 138 (** %\vspace{-.15in}% [[
adamc@255 139 = 1
adamc@255 140 : typeDenote Nat
adamc@255 141 ]] *)
adamc@255 142
adamc@172 143 Eval compute in ExpDenote app.
adamc@255 144 (** %\vspace{-.15in}% [[
adamc@255 145 = fun (x : nat -> nat) (x0 : nat) => x x0
adamc@255 146 : typeDenote ((Nat --> Nat) --> Nat --> Nat)
adamc@255 147 ]] *)
adamc@255 148
adamc@172 149 Eval compute in ExpDenote app_ident'.
adamc@255 150 (** %\vspace{-.15in}% [[
adamc@255 151 = 1
adamc@255 152 : typeDenote Nat
adamc@255 153 ]] *)
adamc@255 154
adamc@172 155
adamc@174 156 (* EX: Define a constant-folding function for [Exp]s. *)
adamc@174 157
adamc@255 158 (** We can update to the higher-order case our common example of a constant folding function. The workhorse function [cfold] is parameterized to apply to an [exp] that uses any [var] type. An output of [cfold] uses the same [var] type as the input. As in the definition of [expDenote], we cannot use most of our notations in patterns, but we use them freely to make the bodies of [match] cases easier to read. *)
adamc@255 159
adamc@174 160 (* begin thide *)
adamc@170 161 Section cfold.
adamc@170 162 Variable var : type -> Type.
adamc@170 163
adamc@223 164 Fixpoint cfold t (e : exp var t) : exp var t :=
adamc@223 165 match e with
adamc@170 166 | Var _ v => #v
adamc@170 167
adamc@170 168 | Const n => ^n
adamc@170 169 | Plus e1 e2 =>
adamc@170 170 let e1' := cfold e1 in
adamc@170 171 let e2' := cfold e2 in
adamc@204 172 match e1', e2' return _ with
adamc@170 173 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 174 | _, _ => e1' +^ e2'
adamc@170 175 end
adamc@170 176
adamc@170 177 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@255 178 | Abs _ _ e' => \x, cfold (e' x)
adamc@170 179 end.
adamc@170 180 End cfold.
adamc@170 181
adamc@170 182 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@174 183 (* end thide *)
adamc@170 184
adamc@174 185 (* EX: Prove the correctness of constant-folding. *)
adamc@174 186
adamc@255 187 (** Now we would like to prove the correctness of [Cfold], which follows from a simple inductive lemma about [cfold]. *)
adamc@255 188
adamc@174 189 (* begin thide *)
adamc@170 190 Lemma cfold_correct : forall t (e : exp _ t),
adamc@170 191 expDenote (cfold e) = expDenote e.
adamc@170 192 induction e; crush; try (ext_eq; crush);
adamc@170 193 repeat (match goal with
adamc@170 194 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@170 195 end; crush).
adamc@170 196 Qed.
adamc@170 197
adamc@170 198 Theorem Cfold_correct : forall t (E : Exp t),
adamc@170 199 ExpDenote (Cfold E) = ExpDenote E.
adamc@170 200 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@170 201 Qed.
adamc@174 202 (* end thide *)
adamc@170 203 End STLC.
adamc@171 204
adamc@171 205
adamc@171 206 (** * Adding Products and Sums *)
adamc@171 207
adamc@255 208 (** The example is easily adapted to support products and sums, the basis of non-recursive datatypes in ML and Haskell. *)
adamc@255 209
adamc@171 210 Module PSLC.
adamc@174 211 (* EX: Extend the development with products and sums. *)
adamc@174 212
adamc@174 213 (* begin thide *)
adamc@171 214 Inductive type : Type :=
adamc@171 215 | Nat : type
adamc@171 216 | Arrow : type -> type -> type
adamc@171 217 | Prod : type -> type -> type
adamc@171 218 | Sum : type -> type -> type.
adamc@174 219 (* end thide *)
adamc@171 220
adamc@171 221 Infix "-->" := Arrow (right associativity, at level 62).
adamc@171 222 Infix "**" := Prod (right associativity, at level 61).
adamc@171 223 Infix "++" := Sum (right associativity, at level 60).
adamc@171 224
adamc@174 225 (* begin thide *)
adamc@171 226 Section vars.
adamc@171 227 Variable var : type -> Type.
adamc@171 228
adamc@171 229 Inductive exp : type -> Type :=
adamc@171 230 | Var : forall t,
adamc@171 231 var t
adamc@171 232 -> exp t
adamc@171 233
adamc@171 234 | Const : nat -> exp Nat
adamc@171 235 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@171 236
adamc@171 237 | App : forall t1 t2,
adamc@171 238 exp (t1 --> t2)
adamc@171 239 -> exp t1
adamc@171 240 -> exp t2
adamc@171 241 | Abs : forall t1 t2,
adamc@171 242 (var t1 -> exp t2)
adamc@171 243 -> exp (t1 --> t2)
adamc@171 244
adamc@171 245 | Pair : forall t1 t2,
adamc@171 246 exp t1
adamc@171 247 -> exp t2
adamc@171 248 -> exp (t1 ** t2)
adamc@171 249 | Fst : forall t1 t2,
adamc@171 250 exp (t1 ** t2)
adamc@171 251 -> exp t1
adamc@171 252 | Snd : forall t1 t2,
adamc@171 253 exp (t1 ** t2)
adamc@171 254 -> exp t2
adamc@171 255
adamc@171 256 | Inl : forall t1 t2,
adamc@171 257 exp t1
adamc@171 258 -> exp (t1 ++ t2)
adamc@171 259 | Inr : forall t1 t2,
adamc@171 260 exp t2
adamc@171 261 -> exp (t1 ++ t2)
adamc@171 262 | SumCase : forall t1 t2 t,
adamc@171 263 exp (t1 ++ t2)
adamc@171 264 -> (var t1 -> exp t)
adamc@171 265 -> (var t2 -> exp t)
adamc@171 266 -> exp t.
adamc@171 267 End vars.
adamc@171 268
adamc@171 269 Definition Exp t := forall var, exp var t.
adamc@174 270 (* end thide *)
adamc@171 271
adamc@171 272 Implicit Arguments Var [var t].
adamc@171 273 Implicit Arguments Const [var].
adamc@171 274 Implicit Arguments Abs [var t1 t2].
adamc@171 275 Implicit Arguments Inl [var t1 t2].
adamc@171 276 Implicit Arguments Inr [var t1 t2].
adamc@171 277
adamc@171 278 Notation "# v" := (Var v) (at level 70).
adamc@171 279
adamc@171 280 Notation "^ n" := (Const n) (at level 70).
adamc@172 281 Infix "+^" := Plus (left associativity, at level 78).
adamc@171 282
adamc@171 283 Infix "@" := App (left associativity, at level 77).
adamc@171 284 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@171 285 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@171 286
adamc@171 287 Notation "[ e1 , e2 ]" := (Pair e1 e2).
adamc@171 288 Notation "#1 e" := (Fst e) (at level 75).
adamc@171 289 Notation "#2 e" := (Snd e) (at level 75).
adamc@171 290
adamc@171 291 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
adamc@171 292 (at level 79).
adamc@171 293
adamc@255 294 (** A few examples can be defined easily, using the notations above. *)
adamc@172 295
adamc@255 296 Example swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ => \p, [#2 #p, #1 #p].
adamc@255 297 Example zo : Exp (Nat ** Nat) := fun _ => [^0, ^1].
adamc@255 298 Example swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _.
adamc@255 299
adamc@255 300 Example natOut : Exp (Nat ++ Nat --> Nat) := fun _ =>
adamc@172 301 \s, case #s of x => #x | y => #y +^ #y.
adamc@255 302 Example ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
adamc@255 303 Example ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
adamc@255 304 Example natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
adamc@255 305 Example natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.
adamc@255 306
adamc@255 307 (** The semantics adapts without incident. *)
adamc@172 308
adamc@174 309 (* begin thide *)
adamc@171 310 Fixpoint typeDenote (t : type) : Set :=
adamc@171 311 match t with
adamc@171 312 | Nat => nat
adamc@171 313 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@171 314 | t1 ** t2 => typeDenote t1 * typeDenote t2
adamc@171 315 | t1 ++ t2 => typeDenote t1 + typeDenote t2
adamc@171 316 end%type.
adamc@171 317
adamc@223 318 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@223 319 match e with
adamc@171 320 | Var _ v => v
adamc@171 321
adamc@171 322 | Const n => n
adamc@171 323 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@171 324
adamc@171 325 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@171 326 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@171 327
adamc@171 328 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@171 329 | Fst _ _ e' => fst (expDenote e')
adamc@171 330 | Snd _ _ e' => snd (expDenote e')
adamc@171 331
adamc@171 332 | Inl _ _ e' => inl _ (expDenote e')
adamc@171 333 | Inr _ _ e' => inr _ (expDenote e')
adamc@171 334 | SumCase _ _ _ e' e1 e2 =>
adamc@171 335 match expDenote e' with
adamc@171 336 | inl v => expDenote (e1 v)
adamc@171 337 | inr v => expDenote (e2 v)
adamc@171 338 end
adamc@171 339 end.
adamc@171 340
adamc@171 341 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174 342 (* end thide *)
adamc@171 343
adamc@172 344 Eval compute in ExpDenote swap.
adamc@255 345 (** %\vspace{-.15in}% [[
adamc@255 346 = fun x : nat * nat => (let (_, y) := x in y, let (x0, _) := x in x0)
adamc@255 347 : typeDenote (Nat ** Nat --> Nat ** Nat)
adamc@255 348 ]] *)
adamc@255 349
adamc@172 350 Eval compute in ExpDenote zo.
adamc@255 351 (** %\vspace{-.15in}% [[
adamc@255 352 = (0, 1)
adamc@255 353 : typeDenote (Nat ** Nat)
adamc@255 354 ]] *)
adamc@255 355
adamc@172 356 Eval compute in ExpDenote swap_zo.
adamc@255 357 (** %\vspace{-.15in}% [[
adamc@255 358 = (1, 0)
adamc@255 359 : typeDenote (Nat ** Nat)
adamc@255 360 ]] *)
adamc@172 361
adamc@255 362 Eval cbv beta iota delta -[plus] in ExpDenote natOut.
adamc@255 363 (** %\vspace{-.15in}% [[
adamc@255 364 = fun x : nat + nat => match x with
adamc@255 365 | inl v => v
adamc@255 366 | inr v => v + v
adamc@255 367 end
adamc@255 368 : typeDenote (Nat ++ Nat --> Nat)
adamc@255 369 ]] *)
adamc@255 370
adamc@172 371 Eval compute in ExpDenote ns1.
adamc@255 372 (** %\vspace{-.15in}% [[
adamc@255 373 = inl nat 3
adamc@255 374 : typeDenote (Nat ++ Nat)
adamc@255 375 ]] *)
adamc@255 376
adamc@172 377 Eval compute in ExpDenote ns2.
adamc@255 378 (** %\vspace{-.15in}% [[
adamc@255 379 = inr nat 5
adamc@255 380 : typeDenote (Nat ++ Nat)
adamc@255 381 ]] *)
adamc@255 382
adamc@172 383 Eval compute in ExpDenote natOut_ns1.
adamc@255 384 (** %\vspace{-.15in}% [[
adamc@255 385 = 3
adamc@255 386 : typeDenote Nat
adamc@255 387 ]] *)
adamc@255 388
adamc@172 389 Eval compute in ExpDenote natOut_ns2.
adamc@255 390 (** %\vspace{-.15in}% [[
adamc@255 391 = 10
adamc@255 392 : typeDenote Nat
adamc@255 393 ]] *)
adamc@255 394
adamc@255 395 (** We adapt the [cfold] function using the same basic dependent-types trick that we applied in an earlier chapter to a very similar function for a language without variables. *)
adamc@172 396
adamc@174 397 (* begin thide *)
adamc@171 398 Section cfold.
adamc@171 399 Variable var : type -> Type.
adamc@171 400
adamc@172 401 Definition pairOutType t :=
adamc@204 402 match t return Type with
adamc@172 403 | t1 ** t2 => option (exp var t1 * exp var t2)
adamc@172 404 | _ => unit
adamc@172 405 end.
adamc@172 406
adamc@172 407 Definition pairOutDefault (t : type) : pairOutType t :=
adamc@255 408 match t with
adamc@172 409 | _ ** _ => None
adamc@172 410 | _ => tt
adamc@172 411 end.
adamc@172 412
adamc@223 413 Definition pairOut t1 t2 (e : exp var (t1 ** t2))
adamc@223 414 : option (exp var t1 * exp var t2) :=
adamc@172 415 match e in exp _ t return pairOutType t with
adamc@172 416 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@172 417 | _ => pairOutDefault _
adamc@172 418 end.
adamc@172 419
adamc@223 420 Fixpoint cfold t (e : exp var t) : exp var t :=
adamc@223 421 match e with
adamc@171 422 | Var _ v => #v
adamc@171 423
adamc@171 424 | Const n => ^n
adamc@171 425 | Plus e1 e2 =>
adamc@171 426 let e1' := cfold e1 in
adamc@171 427 let e2' := cfold e2 in
adamc@204 428 match e1', e2' return _ with
adamc@171 429 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 430 | _, _ => e1' +^ e2'
adamc@171 431 end
adamc@171 432
adamc@171 433 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@255 434 | Abs _ _ e' => \x, cfold (e' x)
adamc@171 435
adamc@171 436 | Pair _ _ e1 e2 => [cfold e1, cfold e2]
adamc@172 437 | Fst t1 _ e' =>
adamc@172 438 let e'' := cfold e' in
adamc@172 439 match pairOut e'' with
adamc@172 440 | None => #1 e''
adamc@172 441 | Some (e1, _) => e1
adamc@172 442 end
adamc@172 443 | Snd _ _ e' =>
adamc@172 444 let e'' := cfold e' in
adamc@172 445 match pairOut e'' with
adamc@172 446 | None => #2 e''
adamc@172 447 | Some (_, e2) => e2
adamc@172 448 end
adamc@171 449
adamc@171 450 | Inl _ _ e' => Inl (cfold e')
adamc@171 451 | Inr _ _ e' => Inr (cfold e')
adamc@171 452 | SumCase _ _ _ e' e1 e2 =>
adamc@171 453 case cfold e' of
adamc@171 454 x => cfold (e1 x)
adamc@171 455 | y => cfold (e2 y)
adamc@171 456 end.
adamc@171 457 End cfold.
adamc@171 458
adamc@171 459 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@171 460
adamc@255 461 (** The proofs are almost as straightforward as before. We first establish two simple theorems about pairs and their projections. *)
adamc@255 462
adamc@172 463 Section pairs.
adamc@172 464 Variables A B : Type.
adamc@172 465
adamc@172 466 Variable v1 : A.
adamc@172 467 Variable v2 : B.
adamc@172 468 Variable v : A * B.
adamc@172 469
adamc@172 470 Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
adamc@172 471 destruct v; crush.
adamc@172 472 Qed.
adamc@172 473
adamc@172 474 Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
adamc@172 475 destruct v; crush.
adamc@172 476 Qed.
adamc@172 477 End pairs.
adamc@172 478
adamc@172 479 Hint Resolve pair_eta1 pair_eta2.
adamc@172 480
adamc@255 481 (** To the proof script for the main lemma, we add just one more [match] case, detecting when case analysis is appropriate on discriminees of matches over sum types. *)
adamc@255 482
adamc@171 483 Lemma cfold_correct : forall t (e : exp _ t),
adamc@171 484 expDenote (cfold e) = expDenote e.
adamc@171 485 induction e; crush; try (ext_eq; crush);
adamc@171 486 repeat (match goal with
adamc@171 487 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@171 488 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
adamc@172 489 end; crush); eauto.
adamc@171 490 Qed.
adamc@171 491
adamc@171 492 Theorem Cfold_correct : forall t (E : Exp t),
adamc@171 493 ExpDenote (Cfold E) = ExpDenote E.
adamc@171 494 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@171 495 Qed.
adamc@174 496 (* end thide *)
adamc@171 497 End PSLC.