How to project (with `proj1` or `proj2`) a universally quantified biconditional (iff)?

Question

How to project (with proj1 or proj2) a universally quantified biconditional (iff) such as in the following example?

Parameter T : Set.
Parameter P Q R: T -> Prop.
Parameter H : forall (t : T), P t <-> Q t.

When I try to use proj1 H, it fails with the following error:

Error: The term "H" has type "forall t : T, P t <-> Q t" while it is expected to have type "?A /\ ?B".

While I would like to get forall (t : T), P t -> Q t.

Edit

Using the suggested solution, I have now two ways to project the biconditional:

Theorem proj1' : (forall t, P t <-> Q t) -> forall t, P t -> Q t.
Proof.
  intros H t.
  exact (proj1 (H t)).
Qed.

Theorem foo : forall (t1 t2 : T),
  (R t1 -> P t1) ->
  (R t2 -> P t2) ->
  R t1 /\ R t2 -> Q t1 /\ Q t2.
Proof.
  intros t1 t2 H1 H2 [H3 H4].

  (* Does not solve the goal, as expected. *)
  auto using H.

  (* Solves the goal, but is unnecessary explicit. *)
  (* auto using (proj1 (H t1)), (proj1 (H t2)). *)

  (* Solves the goal and instanciations are infered. *)
  auto using (proj1' H).
Qed.

Now, a function such as proj1' seems to be quite useful. If it is not offered in the standard library, is it because such situations are actually not happening often enough to justify it, or is it simply an historical accident?

I do realize that a distinct function would be require for two, three, etc. universal quantification (e.g. proj1'' : (forall t u, P t u <-> Q t u) -> forall t u, P t u -> Q t u). But wouldn't functions for up to three or four arguments be enough for most cases?

Related

How does `auto` interract with biconditional (iff)

Answer 1

Since a term of type forall (t : T), P t <-> Q t is a function, you need to apply it to a t of type T to get access to the body, which is a pair of proofs:

Goal (forall t, P t <-> Q t) -> forall t, P t -> Q t.
Proof.
  intros H t.
  exact (proj1 (H t)).
Qed.

The above is like the following (modulo transparency):

Definition proj1' : (forall t, P t <-> Q t) -> forall t, P t -> Q t :=
  fun H t => proj1 (H t).

Respond to Edit

One can suggest many proofs of the foo theorem. I wouldn't use proj1' in any of them:

Theorem foo t1 t2 : (R t1 -> P t1) -> (R t2 -> P t2) ->
  P t1 /\ P t2 -> Q t1 /\ Q t2.

Solution 1

apply is one smart tactic, it can handle biconditionals:

Proof. now split; apply H. Qed.

Solution 2

intros can apply lemmas when moving stuff to the context:

Proof. now intros _ _ [H3%H H4%H]. Qed.

It's like SSReflects's by move=> _ _ [/H H3 /H H4].

Solution 3

Coq can use biconditionals to do rewrites if you Require Import Setoid. first:

Proof. now rewrite !H. Qed.

! in front of a term means "rewrite as many times as you can, but at least once".