Coq中定义满足结合律的三元关系的公理选型分析

你定义的三元关系C a b c语义为a = b @ c，目标是在不直接定义运算符@的前提下，形式化表述结合律(d @ e) @ f = d @ (e @ f)，以下是对两个候选公理的分析和选择建议。

候选公理代码 #

Parameter Entity: Set.
Parameter C : Entity -> Entity -> Entity -> Prop.

Axiom asso1 : forall a c d e,
  ((exists b, C a b c /\ C b d e) <-> (exists f, C a d f /\ C f e c)).

Axiom asso2 : forall s t u a b c d,
  (C a s t -> C b a u -> C d s c -> C c t u -> b = d).

正确性判断 #

• asso1 完全等价于结合律的标准语义
  按C的定义展开公理两侧：

  • 左侧exists b, C a b c /\ C b d e：存在中间值b满足b = d @ e且a = b @ c，即a = (d @ e) @ c，对应左侧结合的运算结果。
  • 右侧exists f, C a d f /\ C f e c：存在中间值f满足f = e @ c且a = d @ f，即a = d @ (e @ c)，对应右侧结合的运算结果。
    双向箭头<->保证了两个命题完全等价：只要一种加括号方式能得到结果a，另一种加括号方式也一定能得到同一个a，既覆盖了结果相等的要求，也覆盖了两种运算分解路径的存在性互通，不需要额外附加@是函数的前提，哪怕C刻画的是多值关系运算，该表述依然成立。

• asso2 仅刻画了结合律的部分性质，无法单独完整表述结合律
  按C的定义展开asso2的前提和结论：
  前提分别对应a = s @ t、b = a @ u = (s @ t) @ u、c = t @ u、d = s @ c = s @ (t @ u)，结论b = d仅说明：如果两种加括号方式的计算链都存在，那么最终结果一定相等。
  这个公理存在两个明显缺陷：

  1. 不保证存在性：如果仅知道(s @ t) @ u存在，无法通过asso2推出一定存在中间值c = t @ u使得s @ c和前者结果相等；反之如果仅知道s @ (t @ u)存在，也无法推出左侧结合路径的存在性，不符合结合律“两种加括号方式完全等价”的要求。
  2. 依赖隐含前提：只有当你额外添加公理保证C是函数关系（即任意两个运算数最多对应一个运算结果），asso2才能和存在性公理组合出完整的结合律约束，单独使用时强度不足。

方案选择建议 #

优先选择asso1，理由如下：

• 语义完整：不需要额外附加约束，就能完全覆盖结合律的全部要求，适配C作为关系的所有可能场景（不管@是全函数、偏函数还是多值关系）。
• 易用性强：双向等价的形式可以直接在证明中双向重写，不需要手动构造中间值的存在性证据，证明效率更高。
• 通用性高：这是关系形式化场景下表述运算结合律的标准写法，可读性强，其他形式化研究者可以直接识别出该公理的语义。

仅当你已经明确添加了C的函数性、全/偏性公理，且具体证明场景只需要约束结果唯一性时，才考虑使用asso2作为补充。

内容的提问来源于stack exchange，提问作者Lepticed