Странное поведение setoid_rewrite в Coq - PullRequest
Новая
       23

Странное поведение setoid_rewrite в Coq

4 голосов
/ 14 ноября 2011

У меня проблемы с переписыванием с использованием тактики 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 отлично работает.

1 Ответ

6 голосов
/ 15 ноября 2011

Это выстрел в темноте, не видящий всего развития, но иногда, когда вы не видите разницы, это означает, что есть различие в части, которую вы не видите.А именно, неявные аргументы.

Например, у вас может быть неявный аргумент где-то, который появляется одинаково в двух местах в попытке рабочего доказательства, и который появляется в двух разных, но взаимопревращаемых (или даже просто равных) в недоказательство попытки.Иногда для запуска тактики требуются одинаковые термины, тогда как взаимозаменяемых терминов будет достаточно для одного и того же дерева доказательств, а для разумного введения eq_refl будет достаточно равных терминов.Когда вы работаете с высокоуровневой тактикой, такой как сетоидная тактика, может быть трудно понять, что происходит под капотом.

Попробуйте сравнить ситуации в Set Printing Implicit или Set Printing All или работаетес No Strict Implicit или No Implicit Arguments для небольшой части доказательства.

...