Coq中symmetry与transitivity相等性策略的定义及工作原理

这两个策略和你已知的reflexivity逻辑完全一致，没有特殊的证明状态修改黑魔法，本质都是对对应关系的结构引理做apply封装，只是内置了自动匹配关系、补全参数的逻辑。

核心等价操作 #

symmetry 策略 #

当目标为R a b时，无参数调用symmetry的完整执行逻辑是：

• 识别目标头部的关系R，在当前环境中查找R的对称性引理：对Coq原生莱布尼茨等号=，该引理为eq_sym : forall {A} x y, x = y -> y = x
• 执行apply eq_sym，直接将目标从a = b转换为b = a

如果使用symmetry in H变体操作假设，本质就是执行apply eq_sym in H，将假设H : a = b转换为H : b = a。

transitivity 策略 #

当目标为R a c时，调用transitivity b的执行逻辑是：

• 识别目标头部的关系R，查找R的传递性引理：对原生等号，该引理为eq_trans : forall {A} x y z, x = y -> y = z -> x = z
• 执行apply eq_trans with (y := b)，将单个目标a = c拆分为两个子目标a = b和b = c

如果调用时不指定中间项b，策略会先触发中间项的推断/交互补全流程，核心的目标修改逻辑不变。

注：这两个策略并非硬编码仅支持原生等号，如果你通过Add Parametric Relation注册了自定义关系的对称、传递属性，策略会自动查找你注册时绑定的引理来执行apply，核心逻辑完全相同。

自定义路径类型的策略实现参考 #

针对你定义的UniMath风格路径类型paths（记为a = b），不需要走关系注册流程，只要先准备好两个基础引理：

• path_sym : forall {A : UU} {a b : A}, a = b -> b = a
• path_trans : forall {A : UU} {a b c : A}, a = b -> b = c -> a = c

即可直接写出和原生行为完全一致的自定义策略：

Ltac symmetry := apply path_sym.
Ltac symmetry_in H := apply path_sym in H.
Ltac transitivity y := apply path_trans with (y := y).

你可以通过Show Proof命令验证：在证明过程中调用上述自定义策略生成的证明项，和原生策略作用于普通等号的证明项结构完全一致，没有任何额外的状态修改操作。如果需要更贴近原生体验，你可以额外给transitivity加上中间项自动推断的Ltac逻辑，但核心功能这三行就已经完全覆盖。

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