Suppose I am inside a Coq proof, and the current context includes a hypothesis of the form
H : forall a : A, P a -> exists b : B, Q a b
where
A B:Type
P : A -> Prop
Q : A -> B -> Prop
Then, I would like to add two new terms to the context:
f : A -> B
H' : forall a : A, P a -> Q a (f a)
How can I do this? I am happy to add nonconstructive axioms to achieve this.
In this generality, this is not possible. Look at the following:
Definition A : Type := True.
Definition B : Type := False.
Definition P : A -> Prop := (fun a : A => False).
Definition Q : A -> B -> Prop := (fun (a : A) (b : B) => True).
Example H_is_trivial: forall a : A, P a -> exists b : B, Q a b.
Proof.
intros a HP.
destruct HP.
Qed.
Example f_cannot_exist: (exists f : A -> B, forall a : A, P a -> Q a (f a)) -> False.
Proof.
intros.
destruct H as [f H].
apply f.
exact I.
Qed.
So there exist assignments for A, B, P and Q in which your H holds, but one can prove that your f cannot exist.
For the refined problem, you can define a simga type {a | P a} und prove with the axiom of choice:
Require Import ClassicalChoice.
Section Test.
Variable A B : Type.
Variable P : A -> Prop.
Variable Q : A -> B -> Prop.
Variable H : forall a : A, P a -> exists b : B, Q a b.
Definition AP := { a : A | P a }.
Definition QAP (a : AP) (b : B) := Q (proj1_sig a) b.
Lemma f_exists: exists f : AP -> B, (forall ap : AP, QAP ap (f ap)).
apply choice.
intros ap.
specialize (H (proj1_sig ap) (proj2_sig ap)).
destruct H as [b HQ].
exists b. exact HQ.
Qed.
It shouldn't be hard to take the sigma type apart again and get to your immediate question, but the sigma type might anyway be more convenient.