Mercurial > cpdt > repo

comparison src/Large.v @ 534:ed829eaa91b2

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.5beta2
author Adam Chlipala <adam@chlipala.net>
date Wed, 05 Aug 2015 14:46:55 -0400
parents 21079e42b773
children dac7a2705b00
comparison
equal deleted inserted replaced
533:8921cfa2f503 534:ed829eaa91b2
1 (* Copyright (c) 2009-2012, Adam Chlipala 1 (* Copyright (c) 2009-2012, 2015, 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:
8 *) 8 *)
9 9
10 (* begin hide *) 10 (* begin hide *)
11 Require Import Arith. 11 Require Import Arith.
12 12
13 Require Import CpdtTactics. 13 Require Import Cpdt.CpdtTactics.
14 14
15 Set Implicit Arguments. 15 Set Implicit Arguments.
16 Set Asymmetric Patterns.
16 (* end hide *) 17 (* end hide *)
17 18
18 19
19 (** %\part{The Big Picture} 20 (** %\part{The Big Picture}
20 21
388 t''. 389 t''.
389 Qed. 390 Qed.
390 391
391 (** We can take the final tactic and move it into the initial part of the proof script, arriving at a nicely automated proof. *) 392 (** We can take the final tactic and move it into the initial part of the proof script, arriving at a nicely automated proof. *)
392 393
393 Reset t. 394 Reset cfold_correct.
394 395
395 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e). 396 Theorem cfold_correct : forall t (e : exp t), expDenote e = expDenote (cfold e).
396 induction e; crush; 397 induction e; crush;
397 repeat (match goal with 398 repeat (match goal with
398 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] => 399 | [ |- context[match ?E with NConst _ => _ | _ => _ end] ] =>