Mercurial > cpdt > repo
comparison src/Predicates.v @ 500:8303abe4a61f
Unnecessary eauto
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Mon, 04 Feb 2013 09:57:06 -0500 |
| parents | 07f2fb4d9b36 |
| children | ed829eaa91b2 |
comparison
equal
deleted
inserted
replaced
| 499:2d7ce9e011f4 | 500:8303abe4a61f |
|---|---|
| 806 Hint Rewrite <- plus_n_Sm. | 806 Hint Rewrite <- plus_n_Sm. |
| 807 | 807 |
| 808 induction 1; crush; | 808 induction 1; crush; |
| 809 match goal with | 809 match goal with |
| 810 | [ H : S ?N = ?N0 + ?N0 |- _ ] => destruct N; destruct N0 | 810 | [ H : S ?N = ?N0 + ?N0 |- _ ] => destruct N; destruct N0 |
| 811 end; crush; eauto. | 811 end; crush. |
| 812 Qed. | 812 Qed. |
| 813 | 813 |
| 814 (** 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]. | 814 (** 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. |
| 815 | 815 |
| 816 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. | 816 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. *) |
| 817 | |
| 818 The original theorem now follows trivially from our lemma. *) | |
| 819 | 817 |
| 820 Theorem even_contra : forall n, even (S (n + n)) -> False. | 818 Theorem even_contra : forall n, even (S (n + n)) -> False. |
| 821 intros; eapply even_contra'; eauto. | 819 intros; eapply even_contra'; eauto. |
| 822 Qed. | 820 Qed. |
| 823 | 821 |
| 827 | 825 |
| 828 Lemma even_contra'' : forall n' n, even n' -> n' = S (n + n) -> False. | 826 Lemma even_contra'' : forall n' n, even n' -> n' = S (n + n) -> False. |
| 829 induction 1; crush; | 827 induction 1; crush; |
| 830 match goal with | 828 match goal with |
| 831 | [ H : S ?N = ?N0 + ?N0 |- _ ] => destruct N; destruct N0 | 829 | [ H : S ?N = ?N0 + ?N0 |- _ ] => destruct N; destruct N0 |
| 832 end; crush; eauto. | 830 end; crush. |
| 833 | 831 |
| 834 (** One subgoal remains: | 832 (** One subgoal remains: |
| 835 | 833 |
| 836 [[ | 834 [[ |
| 837 n : nat | 835 n : nat |