Mercurial > cpdt > repo

comparison src/Large.v @ 375:d1276004eec9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finish pass over LogicProg; change [crush] to take advantage of new [Hint Rewrite] syntax that uses database [core] by default
author Adam Chlipala <adam@chlipala.net>
date Mon, 26 Mar 2012 16:55:59 -0400
parents 4550dedad73a
children d5112c099fbf
comparison
equal deleted inserted replaced
374:f3146d40c2a1 375:d1276004eec9
206 206
207 (** Now we are in a position to see how much nicer is the style of proof that we have followed in most of this book. *) 207 (** Now we are in a position to see how much nicer is the style of proof that we have followed in most of this book. *)
208 208
209 Reset eval_times. 209 Reset eval_times.
210 210
211 Hint Rewrite mult_plus_distr_l : cpdt. 211 Hint Rewrite mult_plus_distr_l.
212 212
213 Theorem eval_times : forall k e, 213 Theorem eval_times : forall k e,
214 eval (times k e) = k * eval e. 214 eval (times k e) = k * eval e.
215 induction e; crush. 215 induction e; crush.
216 Qed. 216 Qed.
419 Theorem confounder : forall e1 e2 e3, 419 Theorem confounder : forall e1 e2 e3,
420 eval e1 * eval e2 * eval e3 = eval e1 * (eval e2 + 1 - 1) * eval e3. 420 eval e1 * eval e2 * eval e3 = eval e1 * (eval e2 + 1 - 1) * eval e3.
421 crush. 421 crush.
422 Qed. 422 Qed.
423 423
424 Hint Rewrite confounder : cpdt. 424 Hint Rewrite confounder.
425 425
426 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e. 426 Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
427 (* begin thide *) 427 (* begin thide *)
428 induction e; crush; 428 induction e; crush;
429 match goal with 429 match goal with
466 466
467 (** remove printing * *) 467 (** remove printing * *)
468 Undo. 468 Undo.
469 info t. 469 info t.
470 (** %\vspace{-.15in}%[[ 470 (** %\vspace{-.15in}%[[
471 == simpl in *; intuition; subst; autorewrite with cpdt in *; 471 == simpl in *; intuition; subst; autorewrite with core in *;
472 simpl in *; intuition; subst; autorewrite with cpdt in *; 472 simpl in *; intuition; subst; autorewrite with core in *;
473 simpl in *; intuition; subst; destruct (reassoc e2). 473 simpl in *; intuition; subst; destruct (reassoc e2).
474 simpl in *; intuition. 474 simpl in *; intuition.
475 475
476 simpl in *; intuition. 476 simpl in *; intuition.
477 477
478 simpl in *; intuition; subst; autorewrite with cpdt in *; 478 simpl in *; intuition; subst; autorewrite with core in *;
479 refine (eq_ind_r 479 refine (eq_ind_r
480 (fun n : nat => 480 (fun n : nat =>
481 n * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2) _ IHe1); 481 n * (eval e3 + 1 - 1) * eval e4 = eval e1 * eval e2) _ IHe1);
482 autorewrite with cpdt in *; simpl in *; intuition; 482 autorewrite with core in *; simpl in *; intuition;
483 subst; autorewrite with cpdt in *; simpl in *; 483 subst; autorewrite with core in *; simpl in *;
484 intuition; subst. 484 intuition; subst.
485 485
486 ]] 486 ]]
487 487
488 A detailed trace of [t]'s execution appears. Since we are using the very general [crush] tactic, many of these steps have no effect and only occur as instances of a more general strategy. We can copy-and-paste the details to see where things go wrong. *) 488 A detailed trace of [t]'s execution appears. Since we are using the very general [crush] tactic, many of these steps have no effect and only occur as instances of a more general strategy. We can copy-and-paste the details to see where things go wrong. *)
489 489
490 Undo. 490 Undo.
491 491
492 (** We arbitrarily split the script into chunks. The first few seem not to do any harm. *) 492 (** We arbitrarily split the script into chunks. The first few seem not to do any harm. *)
493 493
494 simpl in *; intuition; subst; autorewrite with cpdt in *. 494 simpl in *; intuition; subst; autorewrite with core in *.
495 simpl in *; intuition; subst; autorewrite with cpdt in *. 495 simpl in *; intuition; subst; autorewrite with core in *.
496 simpl in *; intuition; subst; destruct (reassoc e2). 496 simpl in *; intuition; subst; destruct (reassoc e2).
497 simpl in *; intuition. 497 simpl in *; intuition.
498 simpl in *; intuition. 498 simpl in *; intuition.
499 499
500 (** The next step is revealed as the culprit, bringing us to the final unproved subgoal. *) 500 (** The next step is revealed as the culprit, bringing us to the final unproved subgoal. *)
501 501
502 simpl in *; intuition; subst; autorewrite with cpdt in *. 502 simpl in *; intuition; subst; autorewrite with core in *.
503 503
504 (** We can split the steps further to assign blame. *) 504 (** We can split the steps further to assign blame. *)
505 505
506 Undo. 506 Undo.
507 507
508 simpl in *. 508 simpl in *.
509 intuition. 509 intuition.
510 subst. 510 subst.
511 autorewrite with cpdt in *. 511 autorewrite with core in *.
512 512
513 (** It was the final of these four tactics that made the rewrite. We can find out exactly what happened. The [info] command presents hierarchical views of proof steps, and we can zoom down to a lower level of detail by applying [info] to one of the steps that appeared in the original trace. *) 513 (** It was the final of these four tactics that made the rewrite. We can find out exactly what happened. The [info] command presents hierarchical views of proof steps, and we can zoom down to a lower level of detail by applying [info] to one of the steps that appeared in the original trace. *)
514 514
515 Undo. 515 Undo.
516 516
517 info autorewrite with cpdt in *. 517 info autorewrite with core in *.
518 (** %\vspace{-.15in}%[[ 518 (** %\vspace{-.15in}%[[
519 == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _ 519 == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _
520 (confounder (reassoc e1) e3 e4)). 520 (confounder (reassoc e1) e3 e4)).
521 ]] 521 ]]
522 522