Proving General Associativity in Groups

Question

For a project I'm coding group theory through Coq, obviously associatvity of 3 elements is a given, however I'm struggling to prove it holds for a string of length n. That is, (x1 * ... * xn) is always the same regardless of how many brackets are in there, or there placement. The relevant group code is

Structure group :=
{
  e : G;
  Op : G -> G -> G;
  Inv : G -> G;

  Associativity : forall (x y z : G), Op x (Op y z) = Op (Op x y) z;
  LeftInverse : forall (x : G), Op (Inv x) x = e;
  LeftIdentity : forall (x : G), Op e x = x;
}.

It's not the proof itself I have the issue with but how to code it. I can see at the very least I'll need a further function that allows me to operate on strings rather than just elements, but i've no idea how to get started. Any pointers?

Arthur Azevedo De Amorim Arthur Azevedo De Amorim · Accepted Answer · 2020-02-20T15:01:25

Operating on strings directly is certainly possible, but cumbersome. When reasoning about languages, it is much more convenient to use abstract syntax trees instead. For your statement, we only want to consider combinations of elements with some binary operation, so a binary tree suffices:

Inductive tree T :=
| Leaf : T -> tree T
| Node : tree T -> tree T -> tree T.

For concreteness, I'll only consider the natural numbers under addition, but this generalizes to any other monoid (and thus any other group). We can write a function that sums all the elements of a tree:

Fixpoint sum_tree t : nat :=
  match t with
  | Leaf n => n
  | Node t1 t2 => sum_tree t1 + sum_tree t2
  end.

We can also write a function that flattens the tree, collecting all of its elements in a list

Fixpoint elements {T} (t : tree T) : list T :=
  match t with
  | Leaf x => [x]
  | Node t1 t2 => elements t1 ++ elements t2
  end.

With these ingredients, we can formulate the statement that you were looking for: if two trees (that is, two ways of putting parenthesis in an expression) have the same sequences of elements, then they must add up to the same number.

Lemma eq_sum_tree t1 t2 :
  elements t1 = elements t2 -> sum_tree t1 = sum_tree t2.

I'll leave the proof of this statement to you. ;)

Proving General Associativity in Groups

1 Answers