小编Cal*_*ill的帖子

对于我通过 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;
}.

这不是我有问题的证据本身，而是如何对其进行编码。我可以看到至少我需要一个进一步的函数来允许我对字符串进行操作而不仅仅是元素，但我不知道如何开始。任何指针？