Comportement impair de setoid_rewrite dans Coq

Question

J'ai des problèmes de réécriture en utilisant la tactique setoid_rewrite. Dans la déclaration de l'instance suivante, je m'attends à ce que setoid_rewrite fmapComp réécrive fmap iso ∘ fmap inv à fmap (iso ∘ inv). Cependant, Coq rapporte que « aucun progrès n'a été fait » au cours de réécriture:

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) 

Je ne comprends pas pourquoi setoid_rewrite échoue. Pour référence, la même commande fonctionne dans d'autres contextes utilisant les termes mêmes. Par exemple, il récrit part et d'autre de l'objectif suivant à l'autre:

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) 

On ne sait pas pourquoi setoid_rewrite œuvres dans le second cas, mais pas la première. Pour référence, ≡ est equiv et fmap est Proper. Autre que cela ≅, Functor et Cat sont des classes, je ne vois pas d'autres faits pertinents. En outre, setoid_replace fonctionne très bien.

Answer 1

Ceci est un tir dans l'obscurité sans voir le développement entier, mais parfois, quand vous ne pouvez pas voir une différence, cela signifie qu'il y a une différence dans une partie que vous ne voyez pas. A savoir, des arguments implicites. Par exemple, vous pouvez avoir un argument implicite quelque part qui apparaît de manière identique à deux endroits dans la tentative de preuve de travail, et qui apparaît dans deux tentatives distinctes mais interconvertibles (ou même simplement égales) dans la tentative de preuve non active. Occasionnellement, les tactiques exigent que des termes identiques se déclenchent, alors que des termes interconvertibles suffiraient avec le même arbre de preuve, et des termes égaux suffiraient avec l'introduction judicieuse de eq_refl. Lorsque vous travaillez avec des tactiques de haut niveau telles que les tactiques de setoid, il peut être difficile de comprendre ce qui se passe sous le capot.

Essayez de comparer les situations sous Set Printing Implicit ou Set Printing All, ou de travailler avec No Strict Implicit ou No Implicit Arguments pour une petite partie de la preuve.