Mercurial > cpdt > repo

annotate src/Interps.v @ 297:b441010125d4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Everything compiles in Coq 8.3pl1
author Adam Chlipala <adam@chlipala.net>
date Fri, 14 Jan 2011 14:39:12 -0500
parents 2c88fc1dbe33
children 7b38729be069
rev   line source
adam@297 1 (* Copyright (c) 2008-2011, 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 *)
adam@297 11 Require Import String List FunctionalExtensionality.
adamc@170 12
adam@297 13 Require Import 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
adam@292 67 (** printing ^ $\dag$ *)
adamc@170 68 Notation "^ n" := (Const n) (at level 70).
adam@292 69 (** printing +^ $\hat{+}$ *)
adamc@171 70 Infix "+^" := Plus (left associativity, at level 79).
adamc@170 71
adamc@170 72 Infix "@" := App (left associativity, at level 77).
adamc@170 73 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@170 74 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@170 75
adamc@255 76 (** A few examples will be useful for testing the functions we will write. *)
adamc@255 77
adamc@255 78 Example zero : Exp Nat := fun _ => ^0.
adamc@255 79 Example one : Exp Nat := fun _ => ^1.
adamc@255 80 Example zpo : Exp Nat := fun _ => zero _ +^ one _.
adamc@255 81 Example ident : Exp (Nat --> Nat) := fun _ => \x, #x.
adamc@255 82 Example app_ident : Exp Nat := fun _ => ident _ @ zpo _.
adamc@255 83 Example app : Exp ((Nat --> Nat) --> Nat --> Nat) := fun _ => \f, \x, #f @ #x.
adamc@255 84 Example app_ident' : Exp Nat := fun _ => app _ @ ident _ @ zpo _.
adamc@172 85
adamc@174 86 (* EX: Define an interpreter for [Exp]s. *)
adamc@174 87
adamc@174 88 (* begin thide *)
adamc@255 89 (** To write our interpreter, we must first interpret object language types as meta language types. *)
adamc@255 90
adamc@170 91 Fixpoint typeDenote (t : type) : Set :=
adamc@170 92 match t with
adamc@170 93 | Nat => nat
adamc@170 94 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@170 95 end.
adamc@170 96
adamc@255 97 (** 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 98
adamc@223 99 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@223 100 match e with
adamc@170 101 | Var _ v => v
adamc@170 102
adamc@170 103 | Const n => n
adamc@170 104 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@170 105
adamc@170 106 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@170 107 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@170 108 end.
adamc@170 109
adamc@170 110 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174 111 (* end thide *)
adamc@170 112
adamc@255 113 (** Some tests establish that [ExpDenote] produces Gallina terms like we might write manually. *)
adamc@255 114
adamc@172 115 Eval compute in ExpDenote zero.
adamc@255 116 (** %\vspace{-.15in}% [[
adamc@255 117 = 0
adamc@255 118 : typeDenote Nat
adamc@255 119 ]] *)
adamc@255 120
adamc@172 121 Eval compute in ExpDenote one.
adamc@255 122 (** %\vspace{-.15in}% [[
adamc@255 123 = 1
adamc@255 124 : typeDenote Nat
adamc@255 125 ]] *)
adamc@255 126
adamc@172 127 Eval compute in ExpDenote zpo.
adamc@255 128 (** %\vspace{-.15in}% [[
adamc@255 129 = 1
adamc@255 130 : typeDenote Nat
adamc@255 131 ]] *)
adamc@255 132
adamc@172 133 Eval compute in ExpDenote ident.
adamc@255 134 (** %\vspace{-.15in}% [[
adamc@255 135 = fun x : nat => x
adamc@255 136 : typeDenote (Nat --> Nat)
adamc@255 137 ]] *)
adamc@255 138
adamc@172 139 Eval compute in ExpDenote app_ident.
adamc@255 140 (** %\vspace{-.15in}% [[
adamc@255 141 = 1
adamc@255 142 : typeDenote Nat
adamc@255 143 ]] *)
adamc@255 144
adamc@172 145 Eval compute in ExpDenote app.
adamc@255 146 (** %\vspace{-.15in}% [[
adamc@255 147 = fun (x : nat -> nat) (x0 : nat) => x x0
adamc@255 148 : typeDenote ((Nat --> Nat) --> Nat --> Nat)
adamc@255 149 ]] *)
adamc@255 150
adamc@172 151 Eval compute in ExpDenote app_ident'.
adamc@255 152 (** %\vspace{-.15in}% [[
adamc@255 153 = 1
adamc@255 154 : typeDenote Nat
adamc@255 155 ]] *)
adamc@255 156
adamc@172 157
adamc@174 158 (* EX: Define a constant-folding function for [Exp]s. *)
adamc@174 159
adamc@255 160 (** 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 161
adamc@174 162 (* begin thide *)
adamc@170 163 Section cfold.
adamc@170 164 Variable var : type -> Type.
adamc@170 165
adamc@223 166 Fixpoint cfold t (e : exp var t) : exp var t :=
adamc@223 167 match e with
adamc@170 168 | Var _ v => #v
adamc@170 169
adamc@170 170 | Const n => ^n
adamc@170 171 | Plus e1 e2 =>
adamc@170 172 let e1' := cfold e1 in
adamc@170 173 let e2' := cfold e2 in
adamc@204 174 match e1', e2' return _ with
adamc@170 175 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 176 | _, _ => e1' +^ e2'
adamc@170 177 end
adamc@170 178
adamc@170 179 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@255 180 | Abs _ _ e' => \x, cfold (e' x)
adamc@170 181 end.
adamc@170 182 End cfold.
adamc@170 183
adamc@170 184 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@174 185 (* end thide *)
adamc@170 186
adamc@174 187 (* EX: Prove the correctness of constant-folding. *)
adamc@174 188
adamc@255 189 (** Now we would like to prove the correctness of [Cfold], which follows from a simple inductive lemma about [cfold]. *)
adamc@255 190
adamc@174 191 (* begin thide *)
adamc@170 192 Lemma cfold_correct : forall t (e : exp _ t),
adamc@170 193 expDenote (cfold e) = expDenote e.
adam@297 194 induction e; crush; try (let x := fresh in extensionality x; crush);
adamc@170 195 repeat (match goal with
adamc@170 196 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@170 197 end; crush).
adamc@170 198 Qed.
adamc@170 199
adamc@170 200 Theorem Cfold_correct : forall t (E : Exp t),
adamc@170 201 ExpDenote (Cfold E) = ExpDenote E.
adamc@170 202 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@170 203 Qed.
adamc@174 204 (* end thide *)
adamc@170 205 End STLC.
adamc@171 206
adamc@171 207
adamc@171 208 (** * Adding Products and Sums *)
adamc@171 209
adamc@255 210 (** The example is easily adapted to support products and sums, the basis of non-recursive datatypes in ML and Haskell. *)
adamc@255 211
adamc@171 212 Module PSLC.
adamc@174 213 (* EX: Extend the development with products and sums. *)
adamc@174 214
adamc@174 215 (* begin thide *)
adamc@171 216 Inductive type : Type :=
adamc@171 217 | Nat : type
adamc@171 218 | Arrow : type -> type -> type
adamc@171 219 | Prod : type -> type -> type
adamc@171 220 | Sum : type -> type -> type.
adamc@174 221 (* end thide *)
adamc@171 222
adamc@171 223 Infix "-->" := Arrow (right associativity, at level 62).
adamc@171 224 Infix "**" := Prod (right associativity, at level 61).
adamc@171 225 Infix "++" := Sum (right associativity, at level 60).
adamc@171 226
adamc@174 227 (* begin thide *)
adamc@171 228 Section vars.
adamc@171 229 Variable var : type -> Type.
adamc@171 230
adamc@171 231 Inductive exp : type -> Type :=
adamc@171 232 | Var : forall t,
adamc@171 233 var t
adamc@171 234 -> exp t
adamc@171 235
adamc@171 236 | Const : nat -> exp Nat
adamc@171 237 | Plus : exp Nat -> exp Nat -> exp Nat
adamc@171 238
adamc@171 239 | App : forall t1 t2,
adamc@171 240 exp (t1 --> t2)
adamc@171 241 -> exp t1
adamc@171 242 -> exp t2
adamc@171 243 | Abs : forall t1 t2,
adamc@171 244 (var t1 -> exp t2)
adamc@171 245 -> exp (t1 --> t2)
adamc@171 246
adamc@171 247 | Pair : forall t1 t2,
adamc@171 248 exp t1
adamc@171 249 -> exp t2
adamc@171 250 -> exp (t1 ** t2)
adamc@171 251 | Fst : forall t1 t2,
adamc@171 252 exp (t1 ** t2)
adamc@171 253 -> exp t1
adamc@171 254 | Snd : forall t1 t2,
adamc@171 255 exp (t1 ** t2)
adamc@171 256 -> exp t2
adamc@171 257
adamc@171 258 | Inl : forall t1 t2,
adamc@171 259 exp t1
adamc@171 260 -> exp (t1 ++ t2)
adamc@171 261 | Inr : forall t1 t2,
adamc@171 262 exp t2
adamc@171 263 -> exp (t1 ++ t2)
adamc@171 264 | SumCase : forall t1 t2 t,
adamc@171 265 exp (t1 ++ t2)
adamc@171 266 -> (var t1 -> exp t)
adamc@171 267 -> (var t2 -> exp t)
adamc@171 268 -> exp t.
adamc@171 269 End vars.
adamc@171 270
adamc@171 271 Definition Exp t := forall var, exp var t.
adamc@174 272 (* end thide *)
adamc@171 273
adamc@171 274 Implicit Arguments Var [var t].
adamc@171 275 Implicit Arguments Const [var].
adamc@171 276 Implicit Arguments Abs [var t1 t2].
adamc@171 277 Implicit Arguments Inl [var t1 t2].
adamc@171 278 Implicit Arguments Inr [var t1 t2].
adamc@171 279
adamc@171 280 Notation "# v" := (Var v) (at level 70).
adamc@171 281
adamc@171 282 Notation "^ n" := (Const n) (at level 70).
adamc@172 283 Infix "+^" := Plus (left associativity, at level 78).
adamc@171 284
adamc@171 285 Infix "@" := App (left associativity, at level 77).
adamc@171 286 Notation "\ x , e" := (Abs (fun x => e)) (at level 78).
adamc@171 287 Notation "\ ! , e" := (Abs (fun _ => e)) (at level 78).
adamc@171 288
adamc@171 289 Notation "[ e1 , e2 ]" := (Pair e1 e2).
adamc@171 290 Notation "#1 e" := (Fst e) (at level 75).
adamc@171 291 Notation "#2 e" := (Snd e) (at level 75).
adamc@171 292
adamc@171 293 Notation "'case' e 'of' x => e1 | y => e2" := (SumCase e (fun x => e1) (fun y => e2))
adamc@171 294 (at level 79).
adamc@171 295
adamc@255 296 (** A few examples can be defined easily, using the notations above. *)
adamc@172 297
adamc@255 298 Example swap : Exp (Nat ** Nat --> Nat ** Nat) := fun _ => \p, [#2 #p, #1 #p].
adamc@255 299 Example zo : Exp (Nat ** Nat) := fun _ => [^0, ^1].
adamc@255 300 Example swap_zo : Exp (Nat ** Nat) := fun _ => swap _ @ zo _.
adamc@255 301
adamc@255 302 Example natOut : Exp (Nat ++ Nat --> Nat) := fun _ =>
adamc@172 303 \s, case #s of x => #x | y => #y +^ #y.
adamc@255 304 Example ns1 : Exp (Nat ++ Nat) := fun _ => Inl (^3).
adamc@255 305 Example ns2 : Exp (Nat ++ Nat) := fun _ => Inr (^5).
adamc@255 306 Example natOut_ns1 : Exp Nat := fun _ => natOut _ @ ns1 _.
adamc@255 307 Example natOut_ns2 : Exp Nat := fun _ => natOut _ @ ns2 _.
adamc@255 308
adamc@255 309 (** The semantics adapts without incident. *)
adamc@172 310
adamc@174 311 (* begin thide *)
adamc@171 312 Fixpoint typeDenote (t : type) : Set :=
adamc@171 313 match t with
adamc@171 314 | Nat => nat
adamc@171 315 | t1 --> t2 => typeDenote t1 -> typeDenote t2
adamc@171 316 | t1 ** t2 => typeDenote t1 * typeDenote t2
adamc@171 317 | t1 ++ t2 => typeDenote t1 + typeDenote t2
adamc@171 318 end%type.
adamc@171 319
adamc@223 320 Fixpoint expDenote t (e : exp typeDenote t) : typeDenote t :=
adamc@223 321 match e with
adamc@171 322 | Var _ v => v
adamc@171 323
adamc@171 324 | Const n => n
adamc@171 325 | Plus e1 e2 => expDenote e1 + expDenote e2
adamc@171 326
adamc@171 327 | App _ _ e1 e2 => (expDenote e1) (expDenote e2)
adamc@171 328 | Abs _ _ e' => fun x => expDenote (e' x)
adamc@171 329
adamc@171 330 | Pair _ _ e1 e2 => (expDenote e1, expDenote e2)
adamc@171 331 | Fst _ _ e' => fst (expDenote e')
adamc@171 332 | Snd _ _ e' => snd (expDenote e')
adamc@171 333
adamc@171 334 | Inl _ _ e' => inl _ (expDenote e')
adamc@171 335 | Inr _ _ e' => inr _ (expDenote e')
adamc@171 336 | SumCase _ _ _ e' e1 e2 =>
adamc@171 337 match expDenote e' with
adamc@171 338 | inl v => expDenote (e1 v)
adamc@171 339 | inr v => expDenote (e2 v)
adamc@171 340 end
adamc@171 341 end.
adamc@171 342
adamc@171 343 Definition ExpDenote t (e : Exp t) := expDenote (e _).
adamc@174 344 (* end thide *)
adamc@171 345
adamc@172 346 Eval compute in ExpDenote swap.
adamc@255 347 (** %\vspace{-.15in}% [[
adamc@255 348 = fun x : nat * nat => (let (_, y) := x in y, let (x0, _) := x in x0)
adamc@255 349 : typeDenote (Nat ** Nat --> Nat ** Nat)
adamc@255 350 ]] *)
adamc@255 351
adamc@172 352 Eval compute in ExpDenote zo.
adamc@255 353 (** %\vspace{-.15in}% [[
adamc@255 354 = (0, 1)
adamc@255 355 : typeDenote (Nat ** Nat)
adamc@255 356 ]] *)
adamc@255 357
adamc@172 358 Eval compute in ExpDenote swap_zo.
adamc@255 359 (** %\vspace{-.15in}% [[
adamc@255 360 = (1, 0)
adamc@255 361 : typeDenote (Nat ** Nat)
adamc@255 362 ]] *)
adamc@172 363
adamc@255 364 Eval cbv beta iota delta -[plus] in ExpDenote natOut.
adamc@255 365 (** %\vspace{-.15in}% [[
adamc@255 366 = fun x : nat + nat => match x with
adamc@255 367 | inl v => v
adamc@255 368 | inr v => v + v
adamc@255 369 end
adamc@255 370 : typeDenote (Nat ++ Nat --> Nat)
adamc@255 371 ]] *)
adamc@255 372
adamc@172 373 Eval compute in ExpDenote ns1.
adamc@255 374 (** %\vspace{-.15in}% [[
adamc@255 375 = inl nat 3
adamc@255 376 : typeDenote (Nat ++ Nat)
adamc@255 377 ]] *)
adamc@255 378
adamc@172 379 Eval compute in ExpDenote ns2.
adamc@255 380 (** %\vspace{-.15in}% [[
adamc@255 381 = inr nat 5
adamc@255 382 : typeDenote (Nat ++ Nat)
adamc@255 383 ]] *)
adamc@255 384
adamc@172 385 Eval compute in ExpDenote natOut_ns1.
adamc@255 386 (** %\vspace{-.15in}% [[
adamc@255 387 = 3
adamc@255 388 : typeDenote Nat
adamc@255 389 ]] *)
adamc@255 390
adamc@172 391 Eval compute in ExpDenote natOut_ns2.
adamc@255 392 (** %\vspace{-.15in}% [[
adamc@255 393 = 10
adamc@255 394 : typeDenote Nat
adamc@255 395 ]] *)
adamc@255 396
adamc@255 397 (** 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 398
adamc@174 399 (* begin thide *)
adamc@171 400 Section cfold.
adamc@171 401 Variable var : type -> Type.
adamc@171 402
adamc@172 403 Definition pairOutType t :=
adamc@204 404 match t return Type with
adamc@172 405 | t1 ** t2 => option (exp var t1 * exp var t2)
adamc@172 406 | _ => unit
adamc@172 407 end.
adamc@172 408
adamc@172 409 Definition pairOutDefault (t : type) : pairOutType t :=
adamc@255 410 match t with
adamc@172 411 | _ ** _ => None
adamc@172 412 | _ => tt
adamc@172 413 end.
adamc@172 414
adamc@223 415 Definition pairOut t1 t2 (e : exp var (t1 ** t2))
adamc@223 416 : option (exp var t1 * exp var t2) :=
adamc@172 417 match e in exp _ t return pairOutType t with
adamc@172 418 | Pair _ _ e1 e2 => Some (e1, e2)
adamc@172 419 | _ => pairOutDefault _
adamc@172 420 end.
adamc@172 421
adamc@223 422 Fixpoint cfold t (e : exp var t) : exp var t :=
adamc@223 423 match e with
adamc@171 424 | Var _ v => #v
adamc@171 425
adamc@171 426 | Const n => ^n
adamc@171 427 | Plus e1 e2 =>
adamc@171 428 let e1' := cfold e1 in
adamc@171 429 let e2' := cfold e2 in
adamc@204 430 match e1', e2' return _ with
adamc@171 431 | Const n1, Const n2 => ^(n1 + n2)
adamc@171 432 | _, _ => e1' +^ e2'
adamc@171 433 end
adamc@171 434
adamc@171 435 | App _ _ e1 e2 => cfold e1 @ cfold e2
adamc@255 436 | Abs _ _ e' => \x, cfold (e' x)
adamc@171 437
adamc@171 438 | Pair _ _ e1 e2 => [cfold e1, cfold e2]
adamc@172 439 | Fst t1 _ e' =>
adamc@172 440 let e'' := cfold e' in
adamc@172 441 match pairOut e'' with
adamc@172 442 | None => #1 e''
adamc@172 443 | Some (e1, _) => e1
adamc@172 444 end
adamc@172 445 | Snd _ _ e' =>
adamc@172 446 let e'' := cfold e' in
adamc@172 447 match pairOut e'' with
adamc@172 448 | None => #2 e''
adamc@172 449 | Some (_, e2) => e2
adamc@172 450 end
adamc@171 451
adamc@171 452 | Inl _ _ e' => Inl (cfold e')
adamc@171 453 | Inr _ _ e' => Inr (cfold e')
adamc@171 454 | SumCase _ _ _ e' e1 e2 =>
adamc@171 455 case cfold e' of
adamc@171 456 x => cfold (e1 x)
adamc@171 457 | y => cfold (e2 y)
adamc@171 458 end.
adamc@171 459 End cfold.
adamc@171 460
adamc@171 461 Definition Cfold t (E : Exp t) : Exp t := fun _ => cfold (E _).
adamc@171 462
adamc@255 463 (** The proofs are almost as straightforward as before. We first establish two simple theorems about pairs and their projections. *)
adamc@255 464
adamc@172 465 Section pairs.
adamc@172 466 Variables A B : Type.
adamc@172 467
adamc@172 468 Variable v1 : A.
adamc@172 469 Variable v2 : B.
adamc@172 470 Variable v : A * B.
adamc@172 471
adamc@172 472 Theorem pair_eta1 : (v1, v2) = v -> v1 = fst v.
adamc@172 473 destruct v; crush.
adamc@172 474 Qed.
adamc@172 475
adamc@172 476 Theorem pair_eta2 : (v1, v2) = v -> v2 = snd v.
adamc@172 477 destruct v; crush.
adamc@172 478 Qed.
adamc@172 479 End pairs.
adamc@172 480
adamc@172 481 Hint Resolve pair_eta1 pair_eta2.
adamc@172 482
adamc@255 483 (** 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 484
adamc@171 485 Lemma cfold_correct : forall t (e : exp _ t),
adamc@171 486 expDenote (cfold e) = expDenote e.
adam@297 487 induction e; crush; try (let x := fresh in extensionality x; crush);
adamc@171 488 repeat (match goal with
adamc@171 489 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
adamc@171 490 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
adamc@172 491 end; crush); eauto.
adamc@171 492 Qed.
adamc@171 493
adamc@171 494 Theorem Cfold_correct : forall t (E : Exp t),
adamc@171 495 ExpDenote (Cfold E) = ExpDenote E.
adamc@171 496 unfold ExpDenote, Cfold; intros; apply cfold_correct.
adamc@171 497 Qed.
adamc@174 498 (* end thide *)
adamc@171 499 End PSLC.