问:等式、战术、对称性和传递性是如何定义的？

Question

我对Coq战术symmetry和transitivity的实际工作方式很感兴趣。我看过Coq手册，但这只描述了他们做什么，而不是他们如何操作一个证明和改变证明状态。作为我正在寻找的例子，在交互定理证明和程序开发中，作者指出“反身策略实际上是apply refl_equal的同义词”(第124页)。但是，作者请读者参考symmetry和transitivity的参考手册。我还没有找到一个很好的描述，这两个策略是同义词，以同样的方式。

为了澄清起见，我问的原因是我定义了一个路径空间paths {A : UU} : A -> A -> UU标记的a = b (类似于UniMath)，除了a = b不是一个命题而是一种类型之外，它的作用就像一个等价关系。由于这个原因，我无法使用Add Parametric Relation将此关系添加为等效关系。我正试图用Ltac为这种路径空间关系编写一个symmetry和transitivity版本，但我不知道如何更改证明状态；了解symmetry和transitivity的实际工作方式可能会有帮助。

Answer 1

这些策略只适用于它在目标中发现的关系的对称性和传递性对应的引理。这些都是使用类型类机制找到的。

例如，您可以声明

From Coq Require Import RelationClasses.

Instance trans : Transitive R.

这将要求你证明R是传递性的，然后你就可以用策略transitivity来证明R x y。