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 失败。作为参考，same 命令在使用 same 术语的其他上下文中工作。例如，它将以下目标的任一侧重写为另一侧：

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 在第二种情况下有效，但在第一种情况下不起作用。作为参考，QI 是 equiv，fmap 是 Proper。除了 ≅、Functor 和 Cat 是类之外，我没有看到任何其他相关事实。另外，setoid_replace 工作正常。

Answer 1

这是在没有看到整个发展的情况下在黑暗中拍摄的，但有时，当你看不到差异时，这意味着你看不到的部分存在差异。即隐式参数。

例如，您可能在某处有一个隐式参数，该参数在工作证明尝试中的两个位置中相同地出现，并且在非工作证明尝试中出现在两个不同但可相互转换（甚至只是相等）的地方。有时，策略需要相同的项来启动，而可相互转换的项足以使用相同的证明树，而相等的项则足以通过明智地引入 eq_refl 来满足。当您使用高级策略（例如 setoid 策略）时，可能很难理解幕后发生的事情。

尝试比较设置隐式打印或设置打印全部下的情况，或使用无严格隐式或无隐式参数 > 证明的一小部分。