Доказательство общей ассоциативности в группах

Question

Для проекта, в котором я кодирую теорию групп через Coq, очевидно, что ассоциативность 3 элементов - это данность, однако я изо всех сил пытаюсь доказать, что она справедлива для строки длины n. То есть (x1 * ... * xn) всегда одинаково, независимо от того, сколько скобок там или там. Соответствующий код группы:

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;
}.

Это не само доказательство, с которым у меня возникла проблема, а способ ее кодирования. Я вижу, по крайней мере, мне понадобится дополнительная функция, которая позволит мне работать со строками, а не только с элементами, но я не знаю, с чего начать. Есть указатели?

Answer 1

Работа со строками напрямую, конечно, возможна, но громоздка. Рассуждая о языках, гораздо удобнее использовать абстрактные синтаксические деревья. Для вашего утверждения мы хотим рассмотреть только комбинации элементов с некоторой двоичной операцией, поэтому достаточно двоичного дерева:

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

Для конкретности я рассмотрю только добавляемые натуральные числа, но это обобщает на любой другой моноид (и, следовательно, любая другая группа). Мы можем написать функцию, которая суммирует все элементы дерева:

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

Мы также можем написать функцию, которая выравнивает дерево, собирая все его элементы в список

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

С помощью этих ингредиентов мы можем сформулировать искомое утверждение: если два дерева (то есть два способа поставить скобки в выражении) имеют одинаковые последовательности элементов, то они должны складываться в одно и то же число.

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

Я оставлю доказательство этого утверждения вам. ;)