How do I prove an existential goal that asks for a certain function in Coq?

Question

Completely new to coq here.

I know about the exists tactic to prove an existential goal, but in this case it wants a function mapping from two sets. What is the syntax for demonstrating such a function?

And if there is no such function how would I disprove this? (I would suppose through a contradiction, but then how would I pose a contradictory hypothesis?)

Context: Trying to work out the proof that all surjective functions have a right inverse.

1 subgoal
A, B : Set
f : A → B
H : ∀ b : B, ∃ a : A, f a = b
______________________________________(1/1)
∃ g : B → A, ∀ b : B, f (g b) = b

Of course, whether or not a function g exists depends on accepting axiom of choice, so where does that come into coq?

I did find this solution:
https://gist.github.com/pedrominicz/0d9004b82713d9244b762eb250b9c808
and the associated reddit post
https://www.reddit.com/r/logic/comments/fxjypn/what_is_not_constructive_in_this_proof/

But I didn't understand it/didn't work for me.

So, what I want to know is:

1. How do you specify axiom of choice in coq (to prove/disprove this)?
2. In general, how would I construct a function to provide witness to an existential goal? (I also want to show that all injective functions have a left inverse)

Answer 1

There are several variants of the axiom of choice in the Coq type theory. You can look at the Coq.Logic.ChoiceFacts module for a reasonably comprehensive list of the various formulations and their relative power.

As far as I can tell, your example is equivalent to the axiom of functional choice. One elegant way to phrase and assume it is the following.

Axiom functional_choice : forall (A : Type) (B : A -> Type),
  (forall x : A, inhabited (B x)) -> inhabited (forall x : A, B x).

The inhabited type is an inductive box that hides the computational content of a proof in Type into a Prop value that can only be inspected to produce more Prop values. In particular, This axiom is pretty innocuous from the point of view of computation since it only produces values in Prop. There are much more violently non-computational examples of choice like global choice which can be stated as:

Axiom global_choice : forall (A : Type), inhabited A -> A.

This one allows to extract computational content out of thin air.

Answer 2

Here is an answer that is a complete script (tested with coq 8.13.2). Coq by default does not have the axiom of choice loaded, so you need to say explicitly that you are going to work with it.

Require Import ClassicalChoice.

Lemma question (A B : Set) (f : A -> B) :
   (forall b, exists a, f a = b) -> exists g, forall b, f (g b) = b.
Proof.
intros H.
apply (choice (fun y x => f x = y)).
exact H.
Qed.