2

例子：

Require Import Basics.
Require Export Setoid.
Require Export Relation_Definitions.
Set Implicit Arguments.

Lemma simple1 (A B : Prop) (f : A -> B) (x : A) : B.
Proof.
  assert (f2: impl A B) by exact f.
  setoid_rewrite <- f2.
  exact x.
Qed.

Lemma simple2 (A B : Prop) (f : A -> B) (x : A) : B.
Proof.
  setoid_rewrite <- f.
  exact x.
Qed.

simple1有效，但simple2失败了

Ltac call to "setoid_rewrite (orient) (glob_constr_with_bindings)" failed.
Ltac call to "setoid_rewrite (orient) (glob_constr_with_bindings)" failed.
Cannot find a relation to rewrite.

我想使用rewrite_strat/Hint Rewrite的判别树来编写我自己的证明搜索，使用impl关系来模拟apply。但setoid_rewrite只有当我使用而不是impl重述引理时才有效，这很烦人。有没有办法接受类型的引理并使用关系？impl->setoid_rewriteA -> Bimpl

4

0 回答 0