comparison src/LogicProg.v @ 370:549d604c3d16

Move exercises out of mainline book
author Adam Chlipala <adam@chlipala.net>
date Fri, 02 Mar 2012 09:58:00 -0500
parents 386b7ad8849b
children 3c039c72eb40
comparison
equal deleted inserted replaced
369:4550dedad73a 370:549d604c3d16
572 intros; autorewrite with my_db in *; assumption. 572 intros; autorewrite with my_db in *; assumption.
573 (* end thide *) 573 (* end thide *)
574 Qed. 574 Qed.
575 575
576 End autorewrite. 576 End autorewrite.
577
578
579 (* begin thide *)
580 (** * Exercises *)
581
582 (** printing * $\cdot$ *)
583
584 (** %\begin{enumerate}%#<ol>#
585
586 %\item%#<li># I did a Google search for group theory and found #<a href="http://dogschool.tripod.com/housekeeping.html">#a page that proves some standard theorems#</a>#%\footnote{\url{http://dogschool.tripod.com/housekeeping.html}}%. This exercise is about proving all of the theorems on that page automatically.
587
588 For the purposes of this exercise, a group is a set [G], a binary function [f] over [G], an identity element [e] of [G], and a unary inverse function [i] for [G]. The following laws define correct choices of these parameters. We follow standard practice in algebra, where all variables that we mention are quantified universally implicitly at the start of a fact. We write infix [*] for [f], and you can set up the same sort of notation in your code with a command like [Infix "*" := f.].
589
590 %\begin{itemize}%#<ul>#
591 %\item%#<li># %\textbf{%#<b>#Associativity#</b>#%}%: [(a * b) * c = a * (b * c)]#</li>#
592 %\item%#<li># %\textbf{%#<b>#Right Identity#</b>#%}%: [a * e = a]#</li>#
593 %\item%#<li># %\textbf{%#<b>#Right Inverse#</b>#%}%: [a * i a = e]#</li>#
594 #</ul> </li>#%\end{itemize}%
595
596 The task in this exercise is to prove each of the following theorems for all groups, where we define a group exactly as above. There is a wrinkle: every theorem or lemma must be proved by either a single call to [crush] or a single call to [eauto]! It is allowed to pass numeric arguments to [eauto], where appropriate. Recall that a numeric argument sets the depth of proof search, where 5 is the default. Lower values can speed up execution when a proof exists within the bound. Higher values may be necessary to find more involved proofs.
597
598 %\begin{itemize}%#<ul>#
599 %\item%#<li># %\textbf{%#<b>#Characterizing Identity#</b>#%}%: [a * a = a -> a = e]#</li>#
600 %\item%#<li># %\textbf{%#<b>#Left Inverse#</b>#%}%: [i a * a = e]#</li>#
601 %\item%#<li># %\textbf{%#<b>#Left Identity#</b>#%}%: [e * a = a]#</li>#
602 %\item%#<li># %\textbf{%#<b>#Uniqueness of Left Identity#</b>#%}%: [p * a = a -> p = e]#</li>#
603 %\item%#<li># %\textbf{%#<b>#Uniqueness of Right Inverse#</b>#%}%: [a * b = e -> b = i a]#</li>#
604 %\item%#<li># %\textbf{%#<b>#Uniqueness of Left Inverse#</b>#%}%: [a * b = e -> a = i b]#</li>#
605 %\item%#<li># %\textbf{%#<b>#Right Cancellation#</b>#%}%: [a * x = b * x -> a = b]#</li>#
606 %\item%#<li># %\textbf{%#<b>#Left Cancellation#</b>#%}%: [x * a = x * b -> a = b]#</li>#
607 %\item%#<li># %\textbf{%#<b>#Distributivity of Inverse#</b>#%}%: [i (a * b) = i b * i a]#</li>#
608 %\item%#<li># %\textbf{%#<b>#Double Inverse#</b>#%}%: [i (][i a) = a]#</li>#
609 %\item%#<li># %\textbf{%#<b>#Identity Inverse#</b>#%}%: [i e = e]#</li>#
610 #</ul> </li>#%\end{itemize}%
611
612 One more use of tactics is allowed in this problem. The following lemma captures one common pattern of reasoning in algebra proofs: *)
613
614 (* begin hide *)
615 Variable G : Set.
616 Variable f : G -> G -> G.
617 Infix "*" := f.
618 (* end hide *)
619
620 Lemma mult_both : forall a b c d1 d2,
621 a * c = d1
622 -> b * c = d2
623 -> a = b
624 -> d1 = d2.
625 crush.
626 Qed.
627
628 (** That is, we know some equality [a = b], which is the third hypothesis above. We derive a further equality by multiplying both sides by [c], to yield [a * c = b * c]. Next, we do algebraic simplification on both sides of this new equality, represented by the first two hypotheses above. The final result is a new theorem of algebra.
629
630 The next chapter introduces more details of programming in Ltac, but here is a quick teaser that will be useful in this problem. Include the following hint command before you start proving the main theorems of this exercise: *)
631
632 Hint Extern 100 (_ = _) =>
633 match goal with
634 | [ _ : True |- _ ] => fail 1
635 | _ => assert True by constructor; eapply mult_both
636 end.
637
638 (** This hint has the effect of applying [mult_both] %\emph{%#<i>#at most once#</i>#%}% during a proof. After the next chapter, it should be clear why the hint has that effect, but for now treat it as a useful black box. Simply using [Hint Resolve mult_both] would increase proof search time unacceptably, because there are just too many ways to use [mult_both] repeatedly within a proof.
639
640 The order of the theorems above is itself a meta-level hint, since I found that order to work well for allowing the use of earlier theorems as hints in the proofs of later theorems.
641
642 The key to this problem is coming up with further lemmas like [mult_both] that formalize common patterns of reasoning in algebraic proofs. These lemmas need to be more than sound: they must also fit well with the way that [eauto] does proof search. For instance, if we had given [mult_both] a traditional statement, we probably would have avoided %``%#"#pointless#"#%''% equalities like [a = b], which could be avoided simply by replacing all occurrences of [b] with [a]. However, the resulting theorem would not work as well with automated proof search! Every additional hint you come up with should be registered with [Hint Resolve], so that the lemma statement needs to be in a form that [eauto] understands %``%#"#natively.#"#%''%
643
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.
645
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.
647
648 #</ol>#%\end{enumerate}% *)
649 (* end thide *)