A proof in Coq/Ssreflect (with classical axioms) that all bijections on a type form a group, without assuming finiteness

Bijections_group.v

From mathcomp Require Import ssreflect ssrfun ssrbool.
Require Import FunctionalExtensionality.
Require Import ClassicalEpsilon.
Require Import PropExtensionality.
Require Import ZArith.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Require Import Utf8.

Section Transformations.

Variable T: Type.

Let I := @id T.

Lemma id_cancel: cancel I I.
Proof.
  exact.
Qed.

Let bij_id_witness := Bijective id_cancel id_cancel: bijective I.

Lemma bij_id: bijective I.
Proof.
  exact: bij_id_witness.
Qed.

Let has_invimg (f: T → T) (y: T) := ∃ x: T, f x = y.

Lemma img_has_invimg: ∀ f: T → T, ∀ x: T, has_invimg f (f x).
Proof.
  rewrite /has_invimg => f x; exists x; reflexivity.
Qed.

Let is_preimg (f: T → T) (y: T) := λ x: T, has_invimg f y → f x = y.

Let eps_preimg (f: T → T) (y: T) := epsilon (inhabits y) (is_preimg f y).

Lemma has_preimg: ∀ f: T → T, ∀ y: T, ∃ x: T, is_preimg f y x.
Proof.
  move => f y; set INVfy := has_invimg f y.
  have: {INVfy} + {¬ INVfy} by apply: excluded_middle_informative.
  case; [firstorder ..].
Qed.

Lemma inj_eps_is_preimg: ∀ f: T → T, ∀ y: T, injective f → is_preimg f y (eps_preimg f y).
Proof.
  move => f y INJf; apply: epsilon_spec; exact: has_preimg.
Qed.

Lemma inj_preimg_cancels: ∀ f: T → T, injective f → cancel f (eps_preimg f).
Proof.
  move => f INJf x; set y := f x; set x' := eps_preimg f y.
  have: is_preimg f y x' by apply: inj_eps_is_preimg.
  rewrite /is_preimg.
  have: has_invimg f y by apply: img_has_invimg.
  firstorder.
Qed.

Lemma inj_r_inv: ∀ f: T → T, injective f → ∃ f', cancel f f'.
Proof.
  move => f INJf; exists (eps_preimg f); apply: inj_preimg_cancels INJf.
Qed.

Lemma bij_r_inv: ∀ f: T → T, bijective f → ∃ f', cancel f f'.
Proof.
  move => f BJf; have: injective f by [apply: bij_inj BJf]; apply inj_r_inv.
Qed.

Lemma bij_r_inv_unique: ∀ f f' f'': T → T, bijective f  → cancel f f' → cancel f f'' → f' = f''.
Proof.
  move => f f' f'' BJf Cf' Cf''; extensionality y; move: BJf f' f'' Cf' Cf'' y.
  exact: bij_can_eq.
Qed.

Proposition bij_r_inv_l_inv: ∀ f f': T → T, bijective f → cancel f f' → cancel f' f.
Proof.
  move => f f' BJf.
  have: ∀ g, cancel f f' → cancel f g → f' = g.
  - move => g CANff' CANfg; apply: bij_r_inv_unique BJf CANff' CANfg.
  case: BJf => g CANfg CANgf UNIQf' CANff'.
  have: f' = g by apply: UNIQf' g CANff' CANfg.
  move => EQgf'; subst g; exact: CANgf.
Qed.

Lemma bij_can_bij: ∀ f f': T → T, bijective f → cancel f f' → bijective f'.
Proof.
  move => f f' BJf CANff'; have: cancel f' f by apply: bij_r_inv_l_inv BJf CANff'.
  move => CANf'f; exact: (Bijective CANf'f CANff').
Qed.

Definition fun_inv (f: T → T) := epsilon (inhabits f) (λ g, cancel f g).

Lemma bij_fun_inv_cancels: ∀ f: T → T, bijective f → cancel f (fun_inv f).
Proof.
  move => f BJf; case: BJf => g CANfg CANgf; rewrite /fun_inv; apply: epsilon_spec.
  exists g; exact: CANfg.
Qed.

Proposition bij_fun_inv_bij: ∀ f: T → T, bijective f → bijective (fun_inv f).
Proof.
  move => f BJf; have: cancel f (fun_inv f) by apply: bij_fun_inv_cancels.
  move => CANfIf; have: cancel (fun_inv f) f by apply: bij_r_inv_l_inv.
  move => CANIff; exact: (Bijective CANIff CANfIf).
Qed.

Fact comp_assoc: associative (λ f g: T → T, f \o g).
Proof.
  by [].
Qed.

Fact can_comp_id: ∀ f f': T → T, cancel f f' → f' \o f = id.
Proof.
  move => f f'; rewrite /cancel => F'Fxx; extensionality y; apply: F'Fxx.
Qed.

Proposition fun_inv_comp_id: ∀ f: T → T, bijective f → f \o (fun_inv f) = id ∧ (fun_inv f) \o f = id.
Proof.
  move => f BJf.
  have: cancel f (fun_inv f) by [apply: bij_fun_inv_cancels] => CfIf.
  have: cancel (fun_inv f) f by [apply: bij_r_inv_l_inv CfIf] => CIff.
  split; [apply: can_comp_id CIff | apply: can_comp_id CfIf].
Qed.

End Transformations.

Section Group_spec.

Record group_op (A: Type): Type := Group_op {
  op: A → A → A;
  e: A;
  inv: A → A;
}.

Class group (A: Type) (g: group_op A) := Group {
  group_assoc_prop: let: Group_op o _ _ := g in associative o;
  group_neutral_l_prop: let: Group_op o e _ := g in left_id e o;
  group_neutral_r_prop: let: Group_op o e _ := g in right_id e o;
  group_inverse_l_prop: let: Group_op o e i := g in left_inverse e i o;
  group_inverse_r_prop: let: Group_op o e i := g in right_inverse e i o;
}.

End Group_spec.

Section Z_group.

Open Scope Z_scope.

Instance z_group: group (Group_op Zplus 0 (λ x: Z, -x)).
Proof.
  constructor; 
  [ (move => x y z; omega) 
  | (move => x; omega)
  ..
  ].
Qed.

End Z_group.

Section Perm_group.

Variable T: Type.

Let perm_sig := {f: T → T | bijective f}.

Fact bij_proof_irrelevant: ∀ fb gb: perm_sig, proj1_sig fb = proj1_sig gb → fb = gb.
Proof.
  move => fb gb; case: fb => f; case: gb => g gp fp.
  rewrite /sval => fEQg; subst f.
  have: gp = fp by [apply: proof_irrelevance] => gpEQfp; subst fp; reflexivity.
Qed.

Let perm_group_op (fb: perm_sig) (gb: perm_sig) : perm_sig := 
  match fb with exist f fp =>
    match gb with exist g gp =>
      @exist (T → T) _ (f \o g) (bij_comp fp gp)
    end
  end.
  
Lemma perm_group_op_assoc: associative perm_group_op.
Proof.
  rewrite /associative /perm_group_op => fb gb hb.
  case: fb; case: gb; case: hb => h hp g gp f fp.
  set fgh := (f \o (g \o h)); have: ((f \o g) \o h) = fgh by [apply: comp_assoc] => fghCOMP.
  apply: bij_proof_irrelevant; rewrite /sval; exact: fghCOMP.
Qed.

Let perm_group_e: perm_sig := @exist (T → T) _ id (bij_id T).

Lemma perm_group_left_id: left_id perm_group_e perm_group_op.
Proof.
  rewrite /left_id /perm_group_e /perm_group_op => gb.
  case: gb => g gp. 
  have: g = id \o g by [firstorder] => IDg.
  apply: bij_proof_irrelevant; rewrite /sval; exact: IDg.
Qed.

Lemma perm_group_right_id: right_id perm_group_e perm_group_op.
Proof.
  rewrite /right_id /perm_group_e /perm_group_op => fb.
  case fb => f fp.
  have: f = f \o id by [firstorder] => IDf.
  apply: bij_proof_irrelevant; rewrite /sval; exact: IDf.
Qed.

Let perm_group_inv (fb: perm_sig): perm_sig := 
  match fb with exist f fp =>
    @exist (T → T) _ (fun_inv f) (bij_fun_inv_bij fp)
  end.
  
Lemma perm_group_left_inv: left_inverse perm_group_e perm_group_inv perm_group_op.
Proof.
  rewrite /left_inverse /perm_group_e /perm_group_inv /perm_group_op => hb.
  case: hb => h hp.
  have: cancel h (fun_inv h) by [apply: bij_fun_inv_cancels] => ChIh.
  have: fun_inv h \o h = id by [apply: can_comp_id] => hIhID.
  apply: bij_proof_irrelevant; rewrite /sval; exact: hIhID.
Qed.

Lemma perm_group_right_inv: right_inverse perm_group_e perm_group_inv perm_group_op.
Proof.
  rewrite /right_inverse /perm_group_e /perm_group_inv /perm_group_op => hb.
  case: hb => h hp.
  have: cancel h (fun_inv h) by [apply: bij_fun_inv_cancels] => ChIh.
  have: cancel (fun_inv h) h by [apply: bij_r_inv_l_inv] => CIhh.
  have: h \o fun_inv h = id by [apply: can_comp_id] => hIhID.
  apply: bij_proof_irrelevant; rewrite /sval; exact: hIhID.
Qed.

Instance perm_group (T: Type):  group (Group_op perm_group_op perm_group_e perm_group_inv).
Proof.
  constructor;
  [ exact: perm_group_op_assoc
  | exact: perm_group_left_id
  | exact: perm_group_right_id
  | exact: perm_group_left_inv
  | exact: perm_group_right_inv
  ].
Qed.

End Perm_group.