Mercurial > cpdt > repo

comparison src/Large.v @ 574:1dc1d41620b6

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Builds with Coq 8.15.2
author Adam Chlipala <adam@chlipala.net>
date Sun, 31 Jul 2022 14:48:22 -0400
parents f874c163f5e0
children
comparison
equal deleted inserted replaced
573:c3d77f2bb92c 574:1dc1d41620b6
256 IHe2 : eval e3 * eval e4 = eval e2 256 IHe2 : eval e3 * eval e4 = eval e2
257 ============================ 257 ============================
258 eval e1 * eval e3 * eval e4 = eval e1 * eval e2 258 eval e1 * eval e3 * eval e4 = eval e1 * eval e2
259 ]] 259 ]]
260 260
261 The [crush] tactic does not know how to finish this goal. We could finish the proof manually. *) 261 The [crush] tactic does not know how to finish this goal. We could finish the proof manually. Just kidding, the standard library got smarter, and the following is now redundant! *)
262 262
263 rewrite <- IHe2; crush. 263 (*rewrite <- IHe2; crush.*)
264 264
265 (** However, the proof would be easier to understand and maintain if we separated this insight into a separate lemma. *) 265 (** However, the proof would be easier to understand and maintain if we separated this insight into a separate lemma. *)
266 266
267 Abort. 267 Abort.
268 268
458 t. 458 t.
459 459
460 (** What is [t] doing to get us to this point? The %\index{tactics!info}%[info] command can help us answer this kind of question. (As of this writing, [info] is no longer functioning in the most recent Coq release, but I hope it returns.) *) 460 (** What is [t] doing to get us to this point? The %\index{tactics!info}%[info] command can help us answer this kind of question. (As of this writing, [info] is no longer functioning in the most recent Coq release, but I hope it returns.) *)
461 461
462 Undo. 462 Undo.
463 info t. 463 (*info*) t.
464 (* Too bad: recent Coq versions removed [info]. *)
464 465
465 (* begin hide *) 466 (* begin hide *)
466 (* begin thide *) 467 (* begin thide *)
467 Definition eir := eq_ind_r. 468 Definition eir := eq_ind_r.
468 (* end thide *) 469 (* end thide *)
513 514
514 (** 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. *) 515 (** 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. *)
515 516
516 Undo. 517 Undo.
517 518
518 info autorewrite with core in *. 519 (*info*) autorewrite with core in *.
519 (** %\vspace{-.15in}%[[ 520 (** %\vspace{-.15in}%[[
520 == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _ 521 == refine (eq_ind_r (fun n : nat => n = eval e1 * eval e2) _
521 (confounder (reassoc e1) e3 e4)). 522 (confounder (reassoc e1) e3 e4)).
522 ]] 523 ]]
523 524
564 >> 565 >>
565 %\vspace{-.15in}%Why has the search time gone up so much? The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *) 566 %\vspace{-.15in}%Why has the search time gone up so much? The [info] command is not much help, since it only shows the result of search, not all of the paths that turned out to be worthless. *)
566 567
567 (* begin thide *) 568 (* begin thide *)
568 Restart. 569 Restart.
569 info eauto 6. 570 (*info*) eauto 6.
570 (** %\vspace{-.15in}%[[ 571 (** %\vspace{-.15in}%[[
571 == intro x; intro y; intro H; intro H0; intro H4; 572 == intro x; intro y; intro H; intro H0; intro H4;
572 simple eapply trans_eq. 573 simple eapply trans_eq.
573 simple apply eq_refl. 574 simple apply eq_refl.
574 575