## Mercurial > cpdt > repo

### comparison src/Predicates.v @ 500:8303abe4a61f

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

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 |