How to make an inverse function in coq

I have a following code. I didn't write the full code, but this should work.

Definition in_domain {X Y : Set} (f : X -> option Y) x := match (f x) with | Some y => True | None => False end.

Definition injective {X Y : Set} (f : X -> option Y) := forall x y z, f x = Some z -> f y = Some z -> x = y.
Definition surjective {X Y : Set} (f : X -> option Y) := forall y, exists x, f x = Some y.
Definition bijective {X Y : Set} (f : X -> option Y) := injective f /\ surjective f.

Definition compose {X Y Z : Set} (f : X -> option Y) (g : Y -> option Z) (H : forall x, in_domain f x -> in_domain g (f x)) := fun x => match (f x) with | Some y => g y | None => None end.

Now I am trying to write Definition inverse {X Y : Set} (f : X -> option Y) (H : bijective f) : Y -> option X. I couldn't make the function g that f x = Some y <-> g y = Some x.

If generating such function is possible, could you please demonstrate how to?

Solution

You need axioms to do this, because Coq does not allow you by default to extract the witness out of an existential proof. In this case, you only need functional extensionality and the principle of unique choice, a weaker variant of the axiom of choice. Here is one possibility for a simplified variant of your problem:

Require Import Coq.Logic.Description.
Require Import Coq.Logic.FunctionalExtensionality.

Definition injective {X Y : Set} (f : X -> Y) := forall x y, f x = f y -> x = y.
Definition surjective {X Y : Set} (f : X -> Y) := forall y, exists x, f x = y.
Definition bijective {X Y : Set} (f : X -> Y) := injective f /\ surjective f.

Lemma inverse {X Y : Set} (f : X -> Y) :
  bijective f -> {g : Y -> X | (forall x, g (f x) = x) /\
                               (forall y, f (g y) = y) }.
Proof.
intros [inj sur].
apply constructive_definite_description.
assert (H : forall y, exists! x, f x = y).
{ intros y.
  destruct (sur y) as [x xP].
  exists x; split; trivial.
  intros x' x'P.
  now apply inj; rewrite xP, x'P. }
exists (fun y => proj1_sig (constructive_definite_description _ (H y))).
split.
- split.
  + intros x.
    destruct (constructive_definite_description _ _).
    simpl.
    now apply inj.
  + intros y.
    now destruct (constructive_definite_description _ _).
- intros g' [H1 H2].
  apply functional_extensionality.
  intros y.
  destruct (constructive_definite_description _ _) as [x e].
  simpl.
  now rewrite <- e, H1.
Qed.