3

これは、問題の動作をキャプチャする、より大きな証明の簡略化されたスニペットです。

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.

coq で置き換えるrewrite prop2と、不可解なエラーで失敗します。ただし、私の意見では、書き換えステップの後にrewrite propcoq は譲歩する必要があります。forall e : t, True誰でもこれで私を助けることができますか？

4

1 に答える 1

2

リファレンスマニュアルに記載されているように：

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 は Setoidiffが setiod が等しいかどうかを確認する必要があります。

于 2011-11-18T11:08:28.257 に答える