Implementing/specifying permutation groups in coq

Question

I am trying to implement/specify the permutation groups (symmetric groups) in coq. This went well for a bit, until I tried to prove that the identity is actually the identity. My proof gets stuck on proving that the proposition "x is invertible" is exactly the same as the proposition "id * x is invertible".

Are these two propositions actually the same? Am I trying to prove something that is not true? Is there a better way of specifying the permutation group (as a type)?

(* The permutation group on X contains all functions between X and X that are bijective/invertible *)
Inductive G {X : Type} : Type :=
| function (f: X -> X) (H: exists g: X -> X, forall x : X, f (g x) = x /\ g (f x) = x).

(* Composing two functions preserves invertibility *)
Lemma invertible_composition {X : Type} (f g: X -> X) :
    (exists f' : X -> X, forall x : X, f (f' x) = x /\ f' (f x) = x) ->
    (exists g' : X -> X, forall x : X, g (g' x) = x /\ g' (g x) = x) ->
     exists h  : X -> X, forall x : X, (fun x => f (g x)) (h x) = x /\ h ((fun x => f (g x)) x) = x.
Admitted.

(* The group operation is composition *)
Definition op {X : Type} (a b : G) : G :=
    match a, b with
    | function f H, function g H' => function (fun x => f (g x)) (@invertible_composition X f g H H')
    end.

Definition id' {X : Type} (x : X) : X := x.

(* The identity function is invertible *)
Lemma id_invertible {X : Type} : exists g : X -> X, forall x : X, id' (g x) = x /\ g (id' x) = x.
Admitted.

Definition id {X : Type} : (@G X) := function id' id_invertible.

(* The part on which I get stuck: proving that composition with the identity does not change elements. *)
Lemma identity {X: Type} : forall x : G, op id x = x /\ @op X x id = x.
Proof.
    intros.
    split.
    - destruct x.
      simpl.
      apply f_equal.
      Abort.

Answer 1

I believe that your statement cannot be proved without assuming extra axioms:

proof_irrelevance:
  forall (P : Prop) (p q : P), p = q.

You need this axiom to show that two elements of G are equal when the underlying functions are:

Require Import Coq.Logic.ProofIrrelevance.

Inductive G X  : Type :=
| function (f: X -> X) (H: exists g: X -> X, forall x : X, f (g x) = x /\ g (f x) = x).

Arguments function {X} _ _.

Definition fun_of_G {X} (f : G X) : X -> X :=
  match f with function f _ => f end.

Lemma fun_of_G_inj {X} (f g : G X) : fun_of_G f = fun_of_G g -> f = g.
Proof.
destruct f as [f fP], g as [g gP].
simpl.
intros e.
destruct e.
f_equal.
apply proof_irrelevance.
Qed.

(As a side note, it is usually better to declare the X parameter of G explicitly, rather than implicitly. It is rarely the case that Coq can figure out what X should be on its own.)

With fun_of_G_inj, it should be possible to show identity simply by applying it to each equality, because fun a => (fun x => x) (g a) is equal to g for any g.

If you want to use this representation for groups, you'll probably also need the axiom of functional extensionality eventually:

functional_extensionality:
  forall X Y (f g : X -> Y), (forall x, f x = g x) -> f = g.

This axiom is available in the Coq.Logic.FunctionalExtensionality module.

If you want to define the inverse element as a function, you probably also need some form of the axiom of choice: it is necessary for extracting the inverse element g from the existence proof.

If you don't want to assume extra axioms, you have to place restrictions on your permutation group. For instance, you can restrict your attention to elements with finite support -- that is, permutation that fix all elements of X, except for a finite set. There are multiple libraries that allow you to work with permutations this way, including my own extensional structures.