How does auto interract with biconditional (iff)

Question

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.
A -> B
Proof.
A -> B
  intros H.
H: A
B apply A_iff_B.
H: A
A assumption.
Qed.

Theorem bar1: B -> A.
B -> A
Proof.
B -> A
  intros H.
H: B
A apply A_iff_B.
H: B
B assumption.
Qed.

Theorem foo2_failing: A -> B.
A -> B
Proof.
A -> B
  intros H.
H: A
B auto using A_iff_B.
H: A
B
Abort.

Theorem bar2_failing: B -> A.
B -> A
Proof.
B -> A
  intros H.
H: B
A auto using A_iff_B.
H: B
A
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.
forall P Q : Prop, P <-> Q -> P -> Q
Proof.
forall P Q : Prop, P <-> Q -> P -> Q
  intros P Q H.
P, Q: Prop
H: P <-> Q
P -> Q apply H.
Qed.

Theorem iff_backward : forall {P Q : Prop},
    (P <-> Q) -> Q -> P.
forall P Q : Prop, P <-> Q -> Q -> P
Proof.
forall P Q : Prop, P <-> Q -> Q -> P
  intros P Q H.
P, Q: Prop
H: P <-> Q
Q -> P apply H.
Qed.

Theorem foo3 : A -> B.
A -> B
Proof.
A -> B
  intros H.
H: A
B
  auto using (iff_forward A_iff_B).
Qed.

Theorem bar3 : B -> A.
B -> A
Proof.
B -> A
  intros H.
H: B
A
  auto using (iff_backward A_iff_B).
Qed.

1. 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.

2. Is there a standard trick for working with biconditionals or are those two projection functions the usual solution?

3. Are such projection functions somewhere in the standard library? I could not found them.

Answer

1. How come apply A_iff_B works and auto using A_iff_B does not?

auto generally uses simple apply instead of apply and this restricted version of apply does not handle biconditionals.

2. 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:

(* if you remove this one, then `auto` won't be able to prove the
   `bar3` theorem *)
Hint Resolve -> A_iff_B.
Adding and removing hints in the core database
implicitly is deprecated. Please specify a hint
database. [implicit-core-hint-db,deprecated]
The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]
Hint Resolve <- A_iff_B.
Adding and removing hints in the core database
implicitly is deprecated. Please specify a hint
database. [implicit-core-hint-db,deprecated]
The default value for hint locality is currently
"local" in a section and "global" otherwise, but is
scheduled to change in a future release. For the time
being, adding hints outside of sections without
specifying an explicit locality is therefore
deprecated. It is recommended to use "export" whenever
possible.
[deprecated-hint-without-locality,deprecated]

Theorem foo3 : A -> B.
A -> B
Proof.
A -> B info_auto.
(* info auto: *)
intro.
simple apply A_iff_B_proj_l2r (in core).
 assumption. Qed. (* look at the output *)

3. 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).
proj1: forall [A B : Prop], A /\ B -> A

Or a bit easier to type, but finds a tad more stuff than we need:

Search (_ /\ _ -> _).
proj2: forall [A B : Prop], A /\ B -> B
proj1: forall [A B : Prop], A /\ B -> A
and_sind:
  forall [A B : Prop] [P : SProp],
  (A -> B -> P) -> A /\ B -> P
and_rec:
  forall [A B : Prop] [P : Set],
  (A -> B -> P) -> A /\ B -> P
and_ind:
  forall [A B P : Prop], (A -> B -> P) -> A /\ B -> P
and_rect:
  forall [A B : Prop] [P : Type],
  (A -> B -> P) -> A /\ B -> P
andb_true_intro:
  forall [b1 b2 : bool],
  b1 = true /\ b2 = true -> (b1 && b2)%bool = true