# Bijections on Coq

In the ssr.ssrfun library we have the following definition:

Variant bijective : Prop := Bijective g of cancel f g & cancel g f.

At first glance it was what I would expect. But then I realized that, while it is trivial to show

Definition bijection {A B : Type} (f : B → A) :=
∀ y, exists! x, f x = y.

Lemma bijective_bijection {A B : Type} (f : B → A) :
bijective f → bijection f.


I was not able to show that a bijective function has an inverse, that is to define

Definition inverse_of_bijective {A B : Type} (f : B → A)
(P : bijective f) (x : A) : B.


The problem is that "Inversion would require case analysis on sort Type which is not allowed". Is it possible to give such a definition of inverse_of_bijective? Otherwise, if we have the viewpoint that a bijective function is a function that comes with its inverse (I wanted to use the inverse of a bijection to show some result that seems first trivial), is it really the definition we want? For instance, should we not have instead something like

Definition bijection_pair {A B : Type} (f : B → A) (g : A → B) :=
cancel f g /\ cancel g f.


? Or is it possible to really work with the current definition of bijective?

This is a case of abstract vs. concrete existence. First-order logic only supports the former, pure Martin-Löf type theory only the later, but mathematicians use both (and don't know it because they're taught only first-order logic).

In Coq we have both:

• Abstract existence exists (x : A), P x is used when we want to express the fact that a thing exists abstractly, i.e., it is there but we do not have access to a concrete one in proofs. Consequently, every proof that uses such existence has to be content with any possible witness x.

• Concrete existence { x : A | P x} is used when we want to express the fact that a concrete thing is available, i.e., it is a particular one that we may rely on in future constructions.

In general, concrete existence is more informative and allows us to get our hands on the thing that exists. Consequently, you should consider using concrete definitions

Definition cancel {A B : Type} (f : A -> B) g :=
forall x, g (f x) = x.

(* Note: we put this one in Type, not in Prop. *)
Variant bijective {A B : Type} (f : B -> A) : Type :=
Bijective : forall g, cancel f g -> cancel g f -> bijective f.

Definition bijection {A B : Type} (f : B -> A) :=
forall y, { x : B | f x = y /\ (forall z, f z = y -> x = z) }.


Now you can extract inverses:

Definition inverse_of_bijective {A B : Type} (f : A -> B) :
bijective f -> { g : B -> A | cancel f g /\ cancel g f }.
Proof.
intros [g cancel_fg cancel_gf].
now exists g.
Defined.

Definition inverse_of_bijection {A B : Type} (f : A -> B) :
bijection f -> { g : B -> A | cancel f g /\ cancel g f }.
Proof.
intros bij_f.
exists (fun y => proj1_sig (bij_f y)).
split.
- intro x.
exact (proj2 (proj2_sig (bij_f (f x))) x eq_refl).
- intro y.
apply (proj2_sig (bij_f y)).
Defined.


With abstract existence we can get our hands on the inverse of a function f only when we are proving a proposition, i.e., something that lives in Prop, but not when we try to construct a thing of type X where X : Type. This is of course annoying, and is not how mathematical practice operates.

• That doesn't capture unique existence, does it? You'd need something like ∀ y, sig (unique (fun x => f x = y)). Commented Jun 3 at 7:44
• Ah yes, sorry! Will fix it. Commented Jun 3 at 9:36
• The definition of bijection has a typo; we need x : B. Your answer text refers to the "definition of bijective" but your actual definition is of bijection. Did you mean to redefine bijective? Also, of course this raises the question, if concrete existence is preferred, then why does the library use abstract existence in the definition?
– djao
Commented Jun 4 at 9:22
• @djao: Yes, I wasn't careful enough in reading the question. I tried to improve the answer. Commented Jun 4 at 13:35
• It was meant to be Defined. Commented Jun 4 at 19:29

As Naïm Favier mentioned, you need an axiom in general. If you are willing to accept an axiom, constructive_definite_description suffices.

From Coq Require Import Utf8 ssrbool ssrfun ssreflect ClassicalDescription.

Definition bijection {A B : Type} (f : B → A) := ∀ y, exists! x, f x = y.

Lemma bijective_bijection {A B : Type} (f : B → A) : bijective f → bijection f.
Proof.
move=> [???] ?.
(repeat esplit) => // ? <- //.
Qed.

Definition inverse_of_bijective {A B : Type} (f : B → A)
(P : bijective f) (x : A) : B.
Proof.
elim (constructive_definite_description _ (bijective_bijection _ P x)) => y ?.
exact y.
Defined.

Theorem inverse_is_inverse : ∀ {A B : Type} (f : A → B) (P : bijective f),
cancel f (inverse_of_bijective f P) ∧ cancel (inverse_of_bijective f P) f.
Proof.
split => ?; rewrite /inverse_of_bijective /sig_rect;
elim constructive_definite_description => ? //.
elim P => g /[swap] _ /[swap] /(f_equal g) /[swap] /[dup] -> -> //.
Qed.