A solution to https://coq-math-problems.github.io/Problem4/

P4_injections_surjections_on_finite_sets.v

(* https://coq-math-problems.github.io/Problem4/ *)

Definition inj {X Y} (f : X -> Y) := forall x x', f x = f x' -> x = x'.

Definition surj {X Y} (f : X -> Y) := forall y, {x : X | f x = y}.

Definition left_inv {X Y} (g : Y -> X) (f : X -> Y) := forall x, g (f x) = x.

Definition right_inv {X Y} (g : Y -> X) (f : X -> Y) := left_inv f g.

Fixpoint Fin (n : nat) : Set :=
  match n with
  | 0   => Empty_set
  | S m => unit + Fin m
  end.

Definition narrow {n} (f : Fin (S n) -> Fin (S n)) : Fin n -> Fin n :=
  fun x => match f (inr x) with
        | inl _ => match f (inl tt) with
                  | inl _ => (match n as n0 return (Fin n0 -> Fin n0) with
                             | 0 => fun x0 => x0
                             | S n0 => fun _ => inl tt
                             end) x
                  | inr ftt => ftt
                  end
        | inr fx => fx
        end.

Ltac immediate_x :=
  match goal with H : ?f ?x = ?y |- {x | ?f x = ?y } => eexists; apply H end.

Ltac solve_using_injectivity :=
  match goal with
    H1 : ?f _ = ?y, H2 : ?f _ = ?y, finj : inj ?f |- _ =>
      specialize (finj _ _ (eq_trans H1 (eq_sym H2))); congruence
  end.

Tactic Notation "destruct_fin" constr(x) := destruct x as [[] |] eqn:?.

Tactic Notation "destruct_fin" constr(x) "as" ident(a) := destruct x as [[] | a] eqn:?.

Ltac simpl_all_matches_with :=
  try (match goal with
      | _ : context [match ?f ?X with | inl _ => _ | inr _  => _ end] |- _ =>
              destruct_fin (f X); subst
      | |- context [match ?f ?X with | inl _ => _ | inr _  => _ end] =>
              destruct_fin (f X); subst
      end; simpl_all_matches_with).

Ltac solve_it :=
  try immediate_x;
  unfold narrow in *; fold Fin in *;
  simpl_all_matches_with; try immediate_x; try solve_using_injectivity.

Lemma narrow_inj {n} (f : Fin (S n) -> Fin (S n)) (finj : inj f) :
  inj (narrow f).
Proof. intros x x' En. solve_it. Qed.

Theorem inj_implies_surj {n} {f : Fin n -> Fin n} : inj f -> surj f.
Proof.
  intros finj y.
  induction n.
  - contradiction y.
  - specialize (IHn (narrow f) (narrow_inj f finj)).
    destruct_fin y as y'; [| specialize (IHn y') as [x En]].
    + destruct_fin (f (inl tt)) as fl; [| specialize (IHn fl) as [? ?]]; solve_it.
    + solve_it.
Qed.

Definition inv {X Y} (f : X -> Y) (fsurj : surj f) :
  {g : Y -> X & inj g & right_inv g f}.
  exists (fun y => let (x, _) := fsurj y in x).
  - intros y y' ?; destruct (fsurj y), (fsurj y'); congruence.
  - intros x; now destruct (fsurj x).
Defined.

Lemma right_inv_inj {X Y} {f : X -> Y} {g : Y -> X} :
  right_inv g f -> inj g.
Proof. intros rinv y y' Hg. rewrite <-(rinv y), <-(rinv y'). now f_equal. Qed.

Lemma surj_left_inv {X Y} {f : X -> Y} {g : Y -> X} :
  surj f -> left_inv g f -> right_inv g f.
Proof. intros fsurj glinv y. destruct (fsurj y); subst. now f_equal. Qed.

Theorem surj_implies_inj {n} {f : Fin n -> Fin n} (fsurj : surj f) : inj f.
Proof.
  destruct (inv f fsurj) as [g ginj flinv]; unfold right_inv in flinv.
  exact (right_inv_inj (surj_left_inv (inj_implies_surj ginj) flinv)).
Qed.