Injection, surjection, and inverses in Coq.

Question.v

(* https://www.reddit.com/r/logic/comments/fxjypn/what_is_not_constructive_in_this_proof/ *)

Definition injective {A B} (f : A -> B) := forall a1 a2, f a1 = f a2 -> a1 = a2.

Definition injective' {A B} (f : A -> B) := forall a1 a2, a1 <> a2 -> f a1 <> f a2.

Theorem injective_injective' : forall {A B} (f : A -> B),
  injective f -> injective' f.
Proof. unfold injective, injective'. auto. Qed.

(*
`eq_dec` is derivable for any _pure_ algebraic data type, that is, for any
algebraic data type that do not containt any functions. For such data types an
`eq_dec` proof could be automatically derived by, for example, a machanism
similar to Haskell's `deriving`.

Given functional extensionality, `eq_dec` is derivable for functions with
finite domain and undecidable otherwise.
*)
Definition eq_dec A := forall (a1 a2 : A), a1 = a2 \/ a1 <> a2.

Lemma False_eq_dec : eq_dec False.
Proof. unfold eq_dec. contradiction. Qed.

Lemma nat_eq_dec : eq_dec nat.
Proof.
  unfold eq_dec.
  induction a1; destruct a2; auto.
  destruct (IHa1 a2); auto using f_equal.
Qed.

Theorem injective'_injective : forall {A B} (f : A -> B),
  eq_dec A -> injective' f -> injective f.
Proof.
  unfold injective, injective', not.
  intros A B f dec H a1 a2 eq.
  destruct (dec a1 a2).
  - assumption.
  - exfalso. apply (H a1 a2); assumption.
Qed.

Definition surjective {A B} (f : A -> B) := forall b, exists a, f a = b.

Definition bijective {A B} (f : A -> B) := injective f /\ surjective f.

Definition left_inverse {A B} (f : A -> B) g := forall a, g (f a) = a.

Definition right_inverse {A B} (f : A -> B) g := forall b, f (g b) = b.

Definition inverse {A B} (f : A -> B) g := left_inverse f g /\ right_inverse f g.

Theorem left_inverse_injective : forall {A B} (f : A -> B),
  (exists g, left_inverse f g) -> injective f.
Proof.
  unfold injective, left_inverse.
  intros A B f [g H] a1 a2 eq.
  apply f_equal with (f := g) in eq.
  repeat rewrite H in eq.
  assumption.
Qed.

(*
`im_dec` is automatically derivable for functions with finite domain.
*)
Definition im_dec {A} {B} (f : A -> B) := forall b, { a | f a = b } + ~(exists a, f a = b).

Lemma not_im_dec : forall {A} (P : ~A), im_dec P.
Proof. constructor. contradiction. Qed.

Theorem injective_left_inverse : forall {A B} (a : A) (f : A -> B),
  im_dec f -> injective f -> exists g, left_inverse f g.
Proof.
  unfold injective, left_inverse.
  intros A B a f dec H.
  exists (fun b => match dec b with inl (exist _ a _) => a | inr _ => a end).
  intros a'.
  destruct (dec (f a')).
  - destruct s. auto.
  - exfalso. apply n. exists a'. reflexivity.
Qed.

Theorem right_inverse_surjective : forall {A B} (f : A -> B),
  (exists g, right_inverse f g) -> surjective f.
Proof.
  unfold right_inverse, surjective.
  intros A B f [g H] b.
  exists (g b).
  apply H.
Qed.

Theorem surjective_right_inverse : forall {A B} (f : A -> B),
  (forall b, { a | f a = b }) -> exists g, right_inverse f g.
Proof.
  unfold right_inverse, surjective.
  intros A B f g.
  exists (fun b => proj1_sig (g b)).
  intros.
  destruct (g b) as [a H].
  assumption.
Qed.