Mercurial > cpdt > repo

comparison src/Predicates.v @ 394:cc8d0503619f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Citations for continuations and unification
author Adam Chlipala <adam@chlipala.net>
date Sun, 22 Apr 2012 15:51:03 -0400
parents d1276004eec9
children 05efde66559d
comparison
equal deleted inserted replaced
393:d40b05266306 394:cc8d0503619f
1 (* Copyright (c) 2008-2011, Adam Chlipala 1 (* Copyright (c) 2008-2012, Adam Chlipala
2 * 2 *
3 * This work is licensed under a 3 * This work is licensed under a
4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0 4 * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
5 * Unported License. 5 * Unported License.
6 * The license text is available at: 6 * The license text is available at:
890 890
891 Theorem even_contra : forall n, even (S (n + n)) -> False. 891 Theorem even_contra : forall n, even (S (n + n)) -> False.
892 intros; eapply even_contra'; eauto. 892 intros; eapply even_contra'; eauto.
893 Qed. 893 Qed.
894 894
895 (** We use a variant %\index{tactics!apply}%[eapply] of [apply] which has the same relationship to [apply] as [eauto] has to [auto]. An invocation of [apply] only succeeds if all arguments to the rule being used can be determined from the form of the goal, whereas [eapply] will introduce unification variables for undetermined arguments. In this case, [eauto] is able to determine the right values for those unification variables. 895 (** We use a variant %\index{tactics!apply}%[eapply] of [apply] which has the same relationship to [apply] as [eauto] has to [auto]. An invocation of [apply] only succeeds if all arguments to the rule being used can be determined from the form of the goal, whereas [eapply] will introduce unification variables for undetermined arguments. In this case, [eauto] is able to determine the right values for those unification variables, using (unsurprisingly) a variant of the classic algorithm for %\emph{%#<i>#unification#</i>#%}~\cite{unification}%.
896 896
897 By considering an alternate attempt at proving the lemma, we can see another common pitfall of inductive proofs in Coq. Imagine that we had tried to prove [even_contra'] with all of the [forall] quantifiers moved to the front of the lemma statement. *) 897 By considering an alternate attempt at proving the lemma, we can see another common pitfall of inductive proofs in Coq. Imagine that we had tried to prove [even_contra'] with all of the [forall] quantifiers moved to the front of the lemma statement. *)
898 898
899 Lemma even_contra'' : forall n' n, even n' -> n' = S (n + n) -> False. 899 Lemma even_contra'' : forall n' n, even n' -> n' = S (n + n) -> False.
900 induction 1; crush; 900 induction 1; crush;