我对 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
失败的?
最佳答案
仅仅因为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
的变量.
关于agda - 使用 Agda "rewrite"证明 "composition of maps is map of compositions",我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/61472911/