Mercurial > cpdt > repo
comparison src/Predicates.v @ 58:1946586b9da7
First two exercises
| author | Adam Chlipala <adamc@hcoop.net> |
|---|---|
| date | Mon, 29 Sep 2008 14:38:21 -0400 |
| parents | 8d7a97b3bb91 |
| children | 1a664ff9d2d1 |
comparison
equal
deleted
inserted
replaced
| 57:6f7142e082c0 | 58:1946586b9da7 |
|---|---|
| 853 intros; eapply propify_holds'; eauto. | 853 intros; eapply propify_holds'; eauto. |
| 854 Qed. | 854 Qed. |
| 855 (* end thide *) | 855 (* end thide *) |
| 856 | 856 |
| 857 (* end hide *) | 857 (* end hide *) |
| 858 | |
| 859 | |
| 860 (** * Exercises *) | |
| 861 | |
| 862 (** %\begin{enumerate}%#<ol># | |
| 863 | |
| 864 %\item%#<li># Prove these tautologies of propositional logic, using only the tactics [apply], [assumption], [constructor], [destruct], [intro], [intros], [left], [right], [split], and [unfold]. | |
| 865 %\begin{enumerate}%#<ol># | |
| 866 %\item%#<li># [(True \/ False) /\ (False \/ True)]#</li># | |
| 867 %\item%#<li># [P -> ~ ~P]#</li># | |
| 868 %\item%#<li># [P /\ (Q \/ R) -> (P /\ Q) \/ (P /\ R)]#</li># | |
| 869 #</ol> </li>#%\end{enumerate}% *) | |
| 870 | |
| 871 (** remove printing exists*) | |
| 872 (** %\item%#<li># Prove the following tautology of first-order logic, using only the tactics [apply], [assert], [assumption], [destruct], [eapply], [eassumption], and [exists]. You will probably find [assert] useful for stating and proving an intermediate lemma, enabling a kind of "forward reasoning," in contrast to the "backward reasoning" that is the default for Coq tactics. [eassumption] is a version of [assumption] that will do matching of unification variables. Let some variable [T] of type [Set] be the set of individuals. [x] is a constant symbol, [p] is a unary predicate symbol, [q] is a binary predicate symbol, and [f] is a unary function symbol. **) | |
| 873 (** printing exists $\exists$ *) | |
| 874 (** %\begin{enumerate}%#<ol># | |
| 875 %\item%#<li># [p x -> (forall x, p x -> exists y, q x y) -> (forall x y, q x y -> q y (f y)) -> exists z, q z (f z)]#</li># | |
| 876 #</ol> </li>#%\end{enumerate}% | |
| 877 | |
| 878 #</ol>#%\end{enumerate}% *) |