coq - 由于未知原因，依赖类型表达式中的术语重写失败

Question

这是一个更大的证明的简化片段，它捕获了有问题的行为。

Section foo.
  Parameter t : Type.
  Parameter x : t.
  Parameter y : t.
  Parameter prop : x = y <-> True.
  Parameter prop2 : x = y.
  Lemma lemma : forall e : t, x = y.
    rewrite prop2.
    intro e; trivial.
    Qed.
End foo.

当您替换rewrite prop2为rewrite propcoq 时，会出现神秘错误。然而，在我看来，coq 应该forall e : t, True在重写步骤之后屈服。谁能帮我这个？

Answer 1

如参考手册中所述：

rewrite term
This tactic applies to any goal. The type of term must have the form
forall (x1:A1) … (xn:An)eq term1 term2.
where eq is the Leibniz equality or a registered setoid equality.

但prop不是具有莱布尼茨等式的形式：

Coq < Unset Printing Notations.
Coq < Print prop.
prop : iff (eq x y) True

所以 coq 需要 Setoid 来检查iffsetiod 是否相等。