Solution to "Finite Cancellative Semigroups" problem

P3_finite_cancellative_semigroups.v

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

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 ded_fin(X : Set) := forall f : X -> X, inj f -> surj f.

Section df_inh_cancel_sgroups.

Variable X : Set.
Variable x0 : X.
Variable m : X -> X -> X.

Infix "*" := m.

Hypothesis X_df : ded_fin X.
Hypothesis assoc : forall x y z, x * (y * z) = (x * y) * z.
Hypothesis l_cancel : forall x y z, x * y = x * z -> y = z.
Hypothesis r_cancel : forall x y z, y * x = z * x -> y = z.

Definition actl_inj x : inj (m x) := l_cancel x.
Definition actr_inj x : inj (fun x' => m x' x) := r_cancel x.

Definition e_eq : {e : X | e * e = e}.
  destruct (X_df _ (actl_inj x0) x0) as [e H].
  exists e. now apply (l_cancel x0); rewrite assoc, H.
Defined.

Definition e : X := proj1_sig e_eq.

Definition e_squared : e * e = e := proj2_sig e_eq.

Theorem l_id x : e * x = x.
Proof. apply (l_cancel e). now rewrite assoc, e_squared. Qed.

Theorem r_id x : x * e = x.
Proof. apply (r_cancel e). now rewrite <-assoc, e_squared. Qed.

Definition inv_correct (x : X) : {inv : X | x * inv = e & inv * x = e}.
  destruct (X_df _ (actl_inj x) e) as [ir Hr].
  destruct (X_df _ (actr_inj x) e) as [il Hl].
  pose proof (assoc il x ir) as Heq.
  rewrite Hr, Hl, l_id, r_id in Heq.
  subst; eauto.
Defined.

(* the inverse operation *)
Definition inv (x : X) : X := proj1_sig (sig_of_sig2 (inv_correct x)).

Definition l_inv x : (inv x) * x = e := proj3_sig (inv_correct x).

Definition r_inv x : x * (inv x) = e := proj2_sig (sig_of_sig2 (inv_correct x)).

End df_inh_cancel_sgroups.