Mercurial > cpdt > repo
comparison src/LogicProg.v @ 334:386b7ad8849b
Change some template annotations
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Tue, 04 Oct 2011 13:38:21 -0400 |
parents | 5cdfbf56afbe |
children | 549d604c3d16 |
comparison
equal
deleted
inserted
replaced
333:c27d97176c85 | 334:386b7ad8849b |
---|---|
574 Qed. | 574 Qed. |
575 | 575 |
576 End autorewrite. | 576 End autorewrite. |
577 | 577 |
578 | 578 |
579 (* begin thide *) | |
579 (** * Exercises *) | 580 (** * Exercises *) |
580 | 581 |
581 (** printing * $\cdot$ *) | 582 (** printing * $\cdot$ *) |
582 | 583 |
583 (** %\begin{enumerate}%#<ol># | 584 (** %\begin{enumerate}%#<ol># |
643 I recommend testing a few simple rules corresponding to common steps in algebraic proofs. You can apply them manually with any tactics you like (e.g., [apply] or [eapply]) to figure out what approaches work, and then switch to [eauto] once you have the full set of hints. | 644 I recommend testing a few simple rules corresponding to common steps in algebraic proofs. You can apply them manually with any tactics you like (e.g., [apply] or [eapply]) to figure out what approaches work, and then switch to [eauto] once you have the full set of hints. |
644 | 645 |
645 I also proved a few hint lemmas tailored to particular theorems, but which do not give common algebraic simplification rules. You will probably want to use some, too, in cases where [eauto] does not find a proof within a reasonable amount of time. In total, beside the main theorems to be proved, my sample solution includes 6 lemmas, with a mix of the two kinds of lemmas. You may use more in your solution, but I suggest trying to minimize the number. | 646 I also proved a few hint lemmas tailored to particular theorems, but which do not give common algebraic simplification rules. You will probably want to use some, too, in cases where [eauto] does not find a proof within a reasonable amount of time. In total, beside the main theorems to be proved, my sample solution includes 6 lemmas, with a mix of the two kinds of lemmas. You may use more in your solution, but I suggest trying to minimize the number. |
646 | 647 |
647 #</ol>#%\end{enumerate}% *) | 648 #</ol>#%\end{enumerate}% *) |
649 (* end thide *) |