作者热门文章
- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
我在使用 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
工作正常。
最佳答案
这是在没有看到整个发展的情况下在黑暗中拍摄的,但有时,当你看不到差异时,这意味着你看不到的部分存在差异。即隐式参数。
例如,您可能在某处有一个隐式参数,该参数在工作证明尝试中的两个位置中相同地出现,并且在非工作证明尝试中出现在两个不同但可相互转换(甚至只是相等)的地方。有时,策略需要相同的项来启动,而可相互转换的项足以使用相同的证明树,而相等的项则足以通过明智地引入 eq_refl 来满足。当您使用高级策略(例如 setoid 策略)时,可能很难理解幕后发生的事情。尝试比较设置隐式打印
或设置打印全部
下的情况,或使用无严格隐式
或无隐式参数
证明的一小部分。
关于url-rewriting - Coq 中 setoid_rewrite 的奇怪行为,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/8120500/
我在使用 setoid_rewrite 策略重写时遇到问题。在下面的实例声明中,我希望 setoid_rewrite fmapComp 会将 fmap iso ∘ fmap inv 重写为 fmap
我是一名优秀的程序员,十分优秀!