Mercurial > cpdt > repo
changeset 500:8303abe4a61f
Unnecessary eauto
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 04 Feb 2013 09:57:06 -0500 |
parents | 2d7ce9e011f4 |
children | 28c2fa8af4eb |
files | src/Predicates.v |
diffstat | 1 files changed, 4 insertions(+), 6 deletions(-) [+] |
line wrap: on
line diff
--- a/src/Predicates.v Fri Feb 01 17:19:15 2013 -0500 +++ b/src/Predicates.v Mon Feb 04 09:57:06 2013 -0500 @@ -808,14 +808,12 @@ induction 1; crush; match goal with | [ H : S ?N = ?N0 + ?N0 |- _ ] => destruct N; destruct N0 - end; crush; eauto. + end; crush. Qed. -(** We write the proof in a way that avoids the use of local variable or hypothesis names, using the %\index{tactics!match}%[match] tactic form to do pattern-matching on the goal. We use unification variables prefixed by question marks in the pattern, and we take advantage of the possibility to mention a unification variable twice in one pattern, to enforce equality between occurrences. The hint to rewrite with [plus_n_Sm] in a particular direction saves us from having to figure out the right place to apply that theorem, and we also take critical advantage of a new tactic, %\index{tactics!eauto}%[eauto]. +(** We write the proof in a way that avoids the use of local variable or hypothesis names, using the %\index{tactics!match}%[match] tactic form to do pattern-matching on the goal. We use unification variables prefixed by question marks in the pattern, and we take advantage of the possibility to mention a unification variable twice in one pattern, to enforce equality between occurrences. The hint to rewrite with [plus_n_Sm] in a particular direction saves us from having to figure out the right place to apply that theorem. -The [crush] tactic uses the tactic [intuition], which, when it runs out of tricks to try using only propositional logic, by default tries the tactic [auto], which we saw in an earlier example. For now, think of [eauto] as a potentially more expensive version of [auto] that considers more possible proofs; see Chapter 13 for more detail. The quick summary is that [eauto] considers applying a lemma even when the form of the current goal doesn not uniquely determine the values of all of the lemma's quantified variables. - -The original theorem now follows trivially from our lemma. *) +The original theorem now follows trivially from our lemma, using a new tactic %\index{tactics!eauto}%[eauto], a fancier version of [auto] whose explanation we postpone to Chapter 13. *) Theorem even_contra : forall n, even (S (n + n)) -> False. intros; eapply even_contra'; eauto. @@ -829,7 +827,7 @@ induction 1; crush; match goal with | [ H : S ?N = ?N0 + ?N0 |- _ ] => destruct N; destruct N0 - end; crush; eauto. + end; crush. (** One subgoal remains: