comparison src/Predicates.v @ 500:8303abe4a61f

Unnecessary eauto
author Adam Chlipala Mon, 04 Feb 2013 09:57:06 -0500 07f2fb4d9b36 ed829eaa91b2
comparison
equal 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