setoid_rewrite с impl не работает с леммами типа `A -> B` - PullRequest
Новая
       73

setoid_rewrite с impl не работает с леммами типа `A -> B`

0 голосов
/ 19 октября 2018

Пример: 

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_rewrite принять леммы типа A -> B и использовать отношение impl?

...