3

我一直在冥想comonad，并且直觉认为非空列表（“完整列表”）是comonad。我在 Idris 中构建了一个似是而非的实现，并且一直致力于证明Comonad 定律，但未能证明其中一个定律的递归分支。我如何证明这一点（?i_do_not_know_how_to_prove_this_if_its_provable漏洞）——或者我错了我的实现是一个有效的comonad（我已经查看了Haskell的NonEmptycomonad实现，它似乎和我的一样）？

module FullList

%default total

data FullList : Type -> Type where
  Single : a -> FullList a
  Cons : a -> FullList a -> FullList a

extract : FullList a -> a
extract (Single x) = x
extract (Cons x _) = x

duplicate : FullList a -> FullList (FullList a)
duplicate = Single 

extend : (FullList a -> b) -> FullList a -> FullList b
extend f (Single x) = Single (f (Single x))
extend f (Cons x y) = Cons (f (Cons x y)) (extend f y)

extend_and_extract_are_inverse : (l : FullList a) -> extend FullList.extract l = l
extend_and_extract_are_inverse (Single x) = Refl
extend_and_extract_are_inverse (Cons x y) = rewrite extend_and_extract_are_inverse y in Refl

comonad_law_1 : (l : FullList a) -> extract (FullList.extend f l) = f l
comonad_law_1 (Single x) = Refl
comonad_law_1 (Cons x y) = Refl

nesting_extend : (l : FullList a) -> extend f (extend g l) = extend (\x => f (extend g x)) l
nesting_extend (Single x) = Refl
nesting_extend (Cons x y) = ?i_do_not_know_how_to_prove_this_if_its_provable
4

1 回答 1

3

请注意，您的目标具有以下形式：

Cons (f (Cons (g (Cons x y)) (extend g y))) (extend f (extend g y)) =
Cons (f (Cons (g (Cons x y)) (extend g y))) (extend (\x1 => f (extend g x1)) y)

你基本上需要证明尾部是相等的：

extend f (extend g y) = extend (\x1 => f (extend g x1)) y

但这正是归纳假设 ( nesting_extend y) 所说的！因此，证明非常简单：

nesting_extend : (l : FullList a) -> extend f (extend g l) = extend (f . extend g) l
nesting_extend (Single x) = Refl
nesting_extend (Cons x y) = cong $ nesting_extend y

我使用了同余引理cong：

cong : (a = b) -> f a = f b

这表示任何函数都f将等项映射为等项。

这里 Idris 推断，其中的inside指的f是's 参数。Cons (f (Cons (g (Cons x y)) (extend g y)))fConsnesting_extendf

于 2017-10-04T08:56:19.313 回答