I noticed, that auto
is ignoring biconditionals. Here is a simplified example:
Parameter A B : Prop.
Parameter A_iff_B : A <-> B.
Theorem foo1: A -> B.
Proof.
intros H. apply A_iff_B. assumption.
Qed.
Theorem bar1: B -> A.
Proof.
intros H. apply A_iff_B. assumption.
Qed.
Theorem foo2_failing: A -> B.
Proof.
intros H. auto using A_iff_B.
Abort.
Theorem bar2_failing: B -> A.
Proof.
intros H. auto using A_iff_B.
Abort.
Now, I know that A <-> B
is a syntactic sugar for A -> B /\ B -> A
so I wrote two theorems to extract one or the other:
Theorem iff_forward : forall {P Q : Prop},
(P <-> Q) -> P -> Q.
Proof.
intros P Q H. apply H.
Qed.
Theorem iff_backward : forall {P Q : Prop},
(P <-> Q) -> Q -> P.
Proof.
intros P Q H. apply H.
Qed.
Theorem foo3: A -> B.
Proof.
intros H.
auto using (iff_forward A_iff_B).
Qed.
Theorem bar3: B -> A.
Proof.
intros H.
auto using (iff_backward A_iff_B).
Qed.
How come apply A_iff_B
works and auto using A_iff_B
does not? I
thought that auto n
is performing an exhaustive search of all
possible sequences of apply
of length <= n using the hypotheses
and all theorems in a given database.
Is there a standard trick for working with biconditionals or are those two projection functions the usual solution?
Are such projection functions somewhere in the standard library? I could not found them.
- How come
apply A_iff_B works
andauto using A_iff_B
does not?
auto
generally uses simple apply
instead of apply
and this restricted version of apply
does not handle biconditionals.
- Is there a standard trick for working with biconditionals or are those two projection functions the usual solution?
You can use Hint Resolve -> (<-)
feature for that:
Hint Resolve -> A_iff_B.
Hint Resolve <- A_iff_B. (* if you remove this one, then `auto` won't be able to prove the `bar3` theorem *)
Theorem foo3: A -> B.
Proof. info_auto. Qed. (* look at the output *)
- Are such projection functions somewhere in the standard library?
Yes, they are called: proj1
and proj2
. Here is how you can find them:
Search (?A /\ ?B -> ?A).
Or a bit easier to type, but finds a tad more stuff than we need:
Search (_ /\ _ -> _).