使用Agda“重写”证明“地图的组合是组合的地图”

Question

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

（本课程中的练习）

相关定义：

_=$=_ : {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 说目标仍然是

(hx ,- vMap f (vMap g xs)) == (hx ,- 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。