agda - 使用 Agda "rewrite"证明 "composition of maps is map of compositions"

Question

我对 Agda 很陌生，我正在尝试做一个简单的证明“ map 的组合就是组合的 map ”。

(来自 this course 的练习)

相关定义:

_=$=_ : {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 = {!!}

Agda 说目标仍然是

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

我想知道为什么要重写 vMapCpFact heq xs失败的？

Answer 1

仅仅因为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 类型的rhs完全推断:

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 的变量.