Stream: Coq users

Topic: Groups in coq

Julin S (Jul 14 2022 at 04:43):

How are groups (as in group theory) usually represented in Coq?

Saw a way like

Structure my_group := My_Group {
  (* domain *)
  dom: Type;

  (* symbols: constants and operators *)
  e: dom;                  (* Identity element *)
  inv: dom -> dom;         (* Inverse element *)
  op: dom -> dom -> dom;   (* Operation *)

  (* axioms: properties on the symbols *)
  opE: forall x:dom, op x e = x;
  opInv: forall x, op x (inv x) = e;
  opComm: forall x y:dom, op x y = op y x;
  opAssoc: forall x y z:dom, op (op x y) z = op x (op y z);
}.

Is it how it's usually done?

I suppose mathcomp would have more stuff related to groups?

Enrico Tassi (Jul 14 2022 at 05:09):

Mathcomp has a lot of results about finite groups. They key choice is to have a groupType, not unlike yours, and then (finite) sets inside this type which are groups and are the main object of your theorems. These "sub groups" share the operation, because of the common group type, so intersecting them makes sense. You move to another groupType when that changes, eg when you quotient.

Enrico Tassi (Jul 14 2022 at 05:38):

There is a stream dedicated to math comp, if you want to know more, that would be the right place.

Julin S (Jul 14 2022 at 05:55):

I don't know much about group theory actually. Was trying to learn its basics. Been reading a book, but thought it would be more exciting to actually try out the stuff in coq.

Julin S (Jul 14 2022 at 05:56):

Does anyone know of a 'learn group theory with coq' tutorial or something along those lines?

Alexander Gryzlov (Jul 14 2022 at 10:19):

There's https://github.com/UniMath/SymmetryBook which uses informal homotopy type theory

James Wood (Jul 14 2022 at 14:31):

If you use this representation, you'll eventually have to axiomatise quotienting of Types and function extensionality. This is probably the best way to go (as opposed to setoids) if your aim is to learn group theory.

Last updated: Oct 13 2024 at 01:02 UTC