Mercurial > cpdt > repo

comparison src/LogicProg.v @ 334:386b7ad8849b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 *)