Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
Solution to "Finite Cancellative Semigroups" problem
(* 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment