证明群中的广义结合性

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.

我会把这个陈述的证据留给你。;)