Mercurial > cpdt > repo

annotate src/Interps.v @ 319:6838c7be18fa

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