Сопоставление с образцом сложности на доказательстве равенства в утверждении - PullRequest
Новая
       75

Сопоставление с образцом сложности на доказательстве равенства в утверждении

0 голосов
/ 03 марта 2019

Я пытаюсь выучить Агду, написав библиотеку моноидов, но пытаюсь показать, что композиция из двух моноидных гомоморфизмов является моноидным гомоморфизмом.

Я определил моноиды как таковые 

record Monoid (a : Level) : Set (Level.suc a) where
  field
    Underlying : Set a 
    _◓_ : Underlying → Underlying → Underlying
    ? : Underlying
  field
    ◓-assoc : (a b c : Underlying) → ((a ◓ b) ◓ c) ≡ (a ◓ (b ◓ c))
    ?-left-neutral : {a : Underlying} → ? ◓ a ≡ a
    ?-right-neutral : {a : Underlying} → a ◓ ? ≡ a

и моноидные гомоморфизмы как 

record MonHom {L L'} (M : Monoid L) (M' : Monoid L') : Set ( L ⊔ L') where
  open Monoid M
  open Monoid M' renaming ( ? to ?'; _◓_ to _◓'_ ; Underlying to Underlying')
  field
    f : Underlying → Underlying'
    ?-preserved : f ? ≡ ?'
    ◓-preserved : (X Y : Underlying) → (f (X ◓ Y)) ≡ (f X ◓' f Y)

Попытка доказать, что моноидные гомоморфизмы сочетаются, требует показать, что операция моноидов сохраняется, что я попытался сделать здесь: 

id-pres-comp : ∀ {a b c} {M : Monoid a} {M' : Monoid b}
                 {M'' : Monoid c} {f : MonHom M M'} {g : MonHom M' M''}
                 (X Y : Monoid.Underlying M) →
               MonHom.f g (MonHom.f f ((M Monoid.◓ X) Y)) ≡
               (M'' Monoid.◓ MonHom.f g (MonHom.f f X))
               (MonHom.f g (MonHom.f f Y))
-- (g ∘ f) (X ◓ Y) ≡ ((g ∘ f) X) ◓' ((g ∘ f)
id-pres-comp {a} {b} {c} {M} {M'} {M''}
             {record { f = f1 ; ?-preserved = id-pres1 ; ◓-preserved = comp-pres1 }}
             {record { f = g2 ; ?-preserved = id-pres2 ; ◓-preserved = comp-pres2 }}
             X Y with (comp-pres1 X Y)
...| p = {!!}

Моя интуиция говорит мне, что сопоставление с образцом на доказательствах сохранения для обоих гомоморфизмов с использованием операторов with сделает доказательство тривиальным, однако я, кажется, не могу добиться прогрессапоскольку я не могу сопоставить refl по неизвестным причинам, как описано в ошибке: 

-- I'm not sure if there should be a case for the constructor refl,
-- because I get stuck when trying to solve the following unification
-- problems (inferred index ≟ expected index):
--   f1 ((M Monoid.◓ X) Y) ≟ (M' Monoid.◓ f1 X) (f1 Y)
-- when checking that the pattern refl has type
-- f1 ((M Monoid.◓ X) Y) ≡ (M' Monoid.◓ f1 X) (f1 Y)

Может ли кто-нибудь помочь мне понять эту ошибку и помочь мне добиться прогресса с этим доказательством?

Спасибо!

Полный смысл здесь .

...