4
setoid_rewrite戦術を使用した書き換えに問題があります。次のインスタンス宣言では、setoid_rewrite fmapCompがfmap iso ∘ fmap invをfmap (iso ∘ inv)に書き換えることを期待しています。しかし、コックは、書き換え時に「何も進展がなされなかった」ことを報告しますCoqのsetoid_rewriteの奇妙な振る舞い
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は正常に動作します。
暗闇の中で撮影する：何らかの戦術が同じであることが必要なときに変換可能な用語など、暗黙のうちに何か嫌なことが起こっている？ '暗黙の引数なし 'の2つの状況を比較してみてください。 – Gilles
「すべて印刷を設定する」という用語と文脈を見ても、何も明らかにされません。奇妙なのは、 'setoid_rewrite'と* then *を使って、希望の平等を使った書き換えがうまくいくのですが、式を構成する項は変更されていないようです。 – danportin
問題がどこで発生したのかわかりません。新鮮なものから始めて暗黙的な引数をより強く制御することは、インスタンスの必要な定義だけで問題を解決しました。だから私は何かが輸入されたモジュールのどこかに埋め込まれたと仮定します。 – danportin