Coq中setoid_rewrite的奇怪行为

Question

我在使用这种setoid_rewrite策略进行重写时遇到了问题.在下面的实例声明中,我希望setoid_rewrite fmapComp将重写fmap iso ? fmap inv为fmap (iso ? inv).然而,Coq报告称在重写过程中"没有取得任何进展":

Instance functorsPreserveIsomorphisms
 `{C : Cat o ?} `{D : Cat u ?}
   {a b : o} {? : o ? u} (F : Functor C D ?) (I : a ? b) : ? a ? ? b.
Proof.
  apply (Build_Isomorphism _ _ _ (? a) (? b) (fmap iso) (fmap inv)).

 o : Type
 ? : o ? o ? Type
 C : Cat o ?
 u : Type
 ? : u ? u ? Type
 D : Cat u ?
 a : o
 b : o
 ? : o ? u
 F : Functor C D ?
 I : a ? b
 ============================
  fmap iso ? fmap inv ? id (? a)

我不明白为什么setoid_rewrite失败.作为参考,相同的命令在其他上下文中使用相同的术语.例如,它将以下目标的任一侧重写为另一个:

Lemma worksotherwise
 `{C : Cat o ?} `{D : Cat u ?}
   {a b : o} {? : o ? u} (F : Functor C D ?) (I : a ? b) :
     fmap iso ? fmap inv ? fmap (iso ? inv)

 o : Type
 ? : o ? o ? Type
 C : Cat o ?
 u : Type
 ? : u ? u ? Type
 D : Cat u ?
 a : o
 b : o
 ? : o ? u
 F : Functor C D ?
 I : a ? b
 ============================
  fmap iso ? fmap inv ? fmap (iso ? inv)

目前还不清楚为什么setoid_rewrite在第二种情况下工作但不是第一种情况.供参考,?是equiv和fmap是Proper.除此之外?,Functor和Cat有课,我没有看到任何其他有关事实.还行,setoid_replace工作正常.

Answer 1

这是在黑暗中拍摄而没有看到整个发展,但有时,当你看不出差异时,这意味着你看不到的部分存在差异.即,隐式参数.

例如,您可能在工作证明尝试中的两个位置出现相同的隐式参数,并且在非工作证明尝试中以两个不同但可互换(或甚至仅仅相等)的形式出现.偶尔战术需要相同的术语才能启动,而相互转换的术语就足以使用相同的证明树,而平等的术语就足以明智地引入eq_refl.当你使用诸如setoid战术等高级策略时,可能很难理解幕后发生的事情.

尝试比较一下Set Printing Implicit或下面的情况Set Printing All,No Strict Implicit或者No Implicit Arguments对一小部分证据进行比较.