我对 Coq 的策略symmetry和transitivity实际工作方式很感兴趣。我已经阅读了 Coq 手册，但这仅描述了它们的工作，而不是它们如何对证明进行操作并更改证明状态。作为我正在寻找的示例，在Interactive Theorem Proving and Program Development中，作者指出“反身策略实际上是apply refl_equal”（第 124 页）的同义词。但是，作者请读者参考symmetry和的参考手册transitivity。我还没有找到对这两种策略以相同方式同义的事物的良好描述。
为了澄清起见，我问的原因是我已经定义了一个路径空间（就像在paths {A : UU} : A -> A -> UUUniMatha = b中一样），它就像一个等价关系，除了它a = b不是一个命题而是一个类型。出于这个原因，我无法将此关系添加为使用 的等价关系Add Parametric Relation。我正在尝试为这种路径空间关系制作 Ltac 的版本，symmetry但transitivity我不知道如何更改证明状态；了解如何symmetry以及transitivity实际工作可能会有所帮助。