Использование Agda "переписать", чтобы доказать "композиция карт является карта композиций" - PullRequest
Новая
       31

Использование Agda "переписать", чтобы доказать "композиция карт является карта композиций"

4 голосов
/ 28 апреля 2020

Я очень новичок в Агде, и я пытаюсь сделать простое доказательство "композиция карт - это карта композиций".

(упражнение взято из этого курса )

Соответствующее определение: 

_=$=_ : {X Y : Set}{f f' : X -> Y}{x x' : X} ->
        f == f' -> x == x' -> f x == f' x'
refl f =$= refl x = refl (f x)

и 

data Vec (X : Set) : Nat -> Set where
  []   :                              Vec X zero
  _,-_ : {n : Nat} -> X -> Vec X n -> Vec X (suc n)
infixr 4 _,-_

Я хочу для доказательства: 

vMapCpFact : {X Y Z : Set}{f : Y -> Z}{g : X -> Y}{h : X -> Z} ->
             (heq : (x : X) -> f (g x) == h x) ->
             {n : Nat} (xs : Vec X n) ->
             vMap f (vMap g xs) == vMap h xs

Я уже разобрался с доказательством, используя =$=

vMapCpFact heq [] = refl []
vMapCpFact heq (x ,- xs) = refl _,-_ =$= heq x =$= vMapCpFact heq xs

Но когда я попытался сделать доказательство, используя rewrite, я застрял на этом шаге: 

vMapCpFact heq [] = refl []
vMapCpFact heq (x ,- xs) rewrite heq x | vMapCpFact heq xs = {!!}

Агда говорит, что цель все еще

(hx, - vMap f (vMap g xs)) == (hx, - vMap h xs)

Интересно, почему перезапись vMapCpFact heq xs не удалась?

1 Ответ

4 голосов
/ 04 мая 2020

Просто потому что vMapCpFact heq xs вообще не стрелял. Тип этого выражения, как сообщает Agda, равен 

vMap _f_73 (vMap _g_74 xs) == vMap (λ z → h z) xs

, т. Е. Agda не может вывести f и g (эти _f_73 и _g_74 являются неразрешенными мета-переменными) и поэтому не могу понять, что именно переписать.

Вы можете исправить это, явно указав f: 

vMapCpFact {f = f} heq (x ,- xs) rewrite heq x | vMapCpFact {f = f} heq xs = {!!}

Теперь тип цели 

(h x ,- vMap h xs) == (h x ,- vMap h xs)

как и ожидалось.

Или вы можете переписать справа налево, так как права типа vMapCpFact heq xs полностью выведены: 

vMap (λ z → h z) xs

Для перезаписи справа налево вы только нужно использовать sym. Затем весь тип объекта проверяет: 

vMapCpFact heq (x ,- xs) rewrite heq x | sym (vMapCpFact heq xs) = refl _

, поскольку метавариабельные переменные _f_73 и _g_74 вынуждены объединяться с действительными переменными f и g с помощью refl.

...