How "auto" inserts using biconditional (iff)

Question

I noticed that autoignoring 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 what A <-> Bsyntax sugar is for A -> B /\ B -> A, so I wrote two theorems for extracting 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.

• Why apply A_iff_Bdoes it work, but auto using A_iff_Bno? I thought I was auto ndoing an exhaustive search of all possible sequences of applylength <= n, using hypotheses and all the theorems in this database.

• Is there a standard trick for working with biconditionals, or are these two projection functions the usual solution?

• Are such projection functions somewhere in the standard library? I could not find them.

Answer 1

• apply A_iff_B works auto using A_iff_B ?

auto simple apply apply, apply biconditionals.

2. biconditionals ?

Hint Resolve -> (<-) :

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 *)

3. - ?

, : proj1 proj2. :

Search (?A /\ ?B -> ?A).

, , :

Search (_ /\ _ -> _).