Mercurial > cpdt > repo

comparison 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
comparison
equal deleted inserted replaced
296:559ec7328410 297:b441010125d4
1 (* Copyright (c) 2008-2010, Adam Chlipala 1 (* Copyright (c) 2008-2011, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import String List. 11 Require Import String List FunctionalExtensionality.
12 12
13 Require Import Axioms Tactics. 13 Require Import Tactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 (* end hide *) 16 (* end hide *)
17 17
18 18
189 (** Now we would like to prove the correctness of [Cfold], which follows from a simple inductive lemma about [cfold]. *) 189 (** Now we would like to prove the correctness of [Cfold], which follows from a simple inductive lemma about [cfold]. *)
190 190
191 (* begin thide *) 191 (* begin thide *)
192 Lemma cfold_correct : forall t (e : exp _ t), 192 Lemma cfold_correct : forall t (e : exp _ t),
193 expDenote (cfold e) = expDenote e. 193 expDenote (cfold e) = expDenote e.
194 induction e; crush; try (ext_eq; crush); 194 induction e; crush; try (let x := fresh in extensionality x; crush);
195 repeat (match goal with 195 repeat (match goal with
196 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) 196 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
197 end; crush). 197 end; crush).
198 Qed. 198 Qed.
199 199
482 482
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. *) 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. *)
484 484
485 Lemma cfold_correct : forall t (e : exp _ t), 485 Lemma cfold_correct : forall t (e : exp _ t),
486 expDenote (cfold e) = expDenote e. 486 expDenote (cfold e) = expDenote e.
487 induction e; crush; try (ext_eq; crush); 487 induction e; crush; try (let x := fresh in extensionality x; crush);
488 repeat (match goal with 488 repeat (match goal with
489 | [ |- context[cfold ?E] ] => dep_destruct (cfold E) 489 | [ |- context[cfold ?E] ] => dep_destruct (cfold E)
490 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E 490 | [ |- match ?E with inl _ => _ | inr _ => _ end = _ ] => destruct E
491 end; crush); eauto. 491 end; crush); eauto.
492 Qed. 492 Qed.