diff options
| -rw-r--r-- | doc/newfaq/main.tex | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/doc/newfaq/main.tex b/doc/newfaq/main.tex index 3aabb98416..3141888f0e 100644 --- a/doc/newfaq/main.tex +++ b/doc/newfaq/main.tex @@ -479,6 +479,44 @@ Qed. \end{coq_example} +\Question[eapplyeauto]{My goal would be solvable using {\tt apply;assumption} if It would not create meta-variables, how can I prove it ?} + +You can use {\tt eapply yourtheorem;eauto} but it won't work in all cases ! (for example if more than one hypotheses match one of the sub goals generated by \eapply) so you should rather use {\tt try solve [eapply yourtheorem;eauto]}, otherwise some metavariables may be incorrectly instanciated. + +\begin{coq_example} +Lemma trans : forall x y z : nat, x=y -> y=z -> x=z. +intros. +transitivity y;assumption. +Qed. + +Goal forall x y z : nat, x=y -> y=z -> x=z. +intros. +eapply trans;eauto. +Qed. + +Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z. +intros. +eapply trans;eauto. +Undo. +eapply trans. +apply H. +auto. +Qed. + +Goal forall x y z t : nat, x=y -> x=t -> y=z -> x=z. +intros. +eapply trans;eauto. +Undo. +try solve [eapply trans;eauto]. +eapply trans. +apply H. +auto. +Qed. + +\end{coq_example} + + + \Question[autowith]{My goal is solvable by some lemma within a set of lemmas and I don't want to remember which one, how can I prove it ?} Use a base of Hints. @@ -725,6 +763,7 @@ that is still unknown. \Question[lemmasvstheorem]{What is difference between a lemma, a fact and a theorem ?} + \Question[organize]{How can I organize my proofs ?} \Question[dependanttype]{What is a dependent type ?} |