haskell - 如何证明基本序列性质

Question

据我了解，表达某事物是自由幺半群的一种方法是使用这样的类:

class (Foldable s, forall a. Monoid (s a)) => Sequence s where
  singleton :: a -> s a

以及以下“通用建筑”法:
对于任何 Monoid m和任何功能 f :: a -> m ,

foldMap f . singleton = f

foldMap f是幺半群态射。

foldMap f是唯一同时满足 1 和 2 的函数。

这种理解正确吗？
如果是这样，那么能够使用这些定律来证明基本的序列属性会很好。我们可以定义

data ViewL s a
  = EmptyL
  | a :< s a

instance Sequence s => Semigroup (ViewL s a) where
  EmptyL <> y = y
  x <> EmptyL = x
  (x :< xs) <> (y :< ys) = x :< (xs <> singleton y <> ys)

instance Sequence s => Monoid (ViewL s a) where
  mempty = EmptyL

viewl :: Sequence s => s a -> ViewL s a
viewl = foldMap (:< mempty)

我将如何显示以下内容？

viewl s = EmptyL ==> s == mempty

viewl s == a :< s' <==> s == singleton a <> s'

1 的反义词紧跟在 foldMap f 之后。是所有 f 的幺半群态射，但我真的不知道如何处理上述问题。

Answer 1

我们将从几个关于 foldMap 的一般引理开始。和 singleton .第一个引理显然来自任何Foldable 的参数性。 ，但我们可以使用它们的定律直接证明它。
引理(foldMap 组成):假设 Sequence s , Monoid m , 和 Monoid n .让 f :: a -> m成为一个函数并让 g :: m -> n是一个幺半群态射。然后

g . foldMap @s f = foldMap @s (g . f)

证明:

g . foldMap @s f . singleton @s
= -- foldMap/singleton
g . f

通过 foldMap 的唯一性,

g . foldMap @s f = foldMap @s (g . f)

引理(重建):对于任何 Sequence s , foldMap @s (singleton @s) = id @s .
证明: id @s . singleton @s = singleton @s .通过 foldMap 的唯一性, id @s = foldMap @s (singleton @s) .

接下来，我们将重写 Semigroup (ViewL s a)以一种更容易在下面使用的形式进行实例化。只需一点等式推理(使用一般 case 变换和幺半群恒等式)就足以证明以下实例是等价的(忽略惰性，我将自始至终)。

instance Sequence s => Semigroup (ViewL s a) where
  EmptyL <> y = y
  (x :< xs) <> v = x :< (xs <> unviewl v)

unviewl :: Sequence s => ViewL s a -> s a
unviewl EmptyL = mempty
unviewl (x :< xs) = singleton x <> xs

引理: unviewl是幺半群态射。
证明:我们必须证明 unviewl mempty = mempty对于任何 v1和 v2 , unviewl v1 <> unviewl v2 = unviewl (v1 <> v2) .第一个是微不足道的。

unviewl @s mempty
= -- def of mempty for ViewL s
unviewl @s EmptyL
= -- def of unviewl
mempty

其次，我们按案例工作:
第一种情况:

unviewl (EmptyL <> v2)
= -- definition of <> (or the monoid law)
unviewl v2
= -- monoid law
mempty <> unviewl v2
= -- definition of unviewl
unviewl EmptyL <> unviewl v2

第二种情况:

unviewl ((x :< xs) <> v)
= -- definition of <>
unviewl (x :< (xs <> unviewl v))
= -- definition of unviewl
singleton x <> xs <> unviewl v
= -- definition of unviewl
unviewl (x :< xs) <> unviewl v

接下来，我们证明 viewl和 unviewl是(满)逆。
引理: unviewl . viewl = id证明:

unviewl . viewl
= -- definition of viewl
unviewl . foldMap (:< mempty)
= -- foldMap composition lemma and the fact that unviewl
  -- is a monoid morphism.
foldMap (unviewl . (:< mempty))
=
foldMap (\x -> unviewl (x :< mempty))
= -- definition of unviewl
foldMap (\x -> singleton x <> mempty)
= -- monoid law and eta reduction
foldMap singleton
= -- rebuilding lemma
id

引理( viewl 的 singleton ):对于任何 a , viewl (singleton a) = a :< mempty .
证明:

viewl (singleton a)
= -- definition of viewl
foldMap (:< mempty) (singleton a)
= -- foldMap/singleton law
a :< mempty

引理: viewl . unviewl = id证明:设 v :: ViewL s a .我们在 v 上按案例进行。 .
第一种情况:

viewl (unviewl EmptyL)
= -- definition of unviewl
viewl mempty
= -- viewl is a monoid morphism (because it is a fold)
mempty
= -- definition of mempty
EmptyL

第二种情况:

viewl (unviewl (x :< xs))
= -- definition of unviewl
viewl (singleton x <> xs)
= -- viewl is a monoid morphism
viewl (singleton x) <> viewl xs
= -- viewl of singleton lemma
(x :< mempty) <> viewl xs
= -- definition of <>
x :< (mempty <> unviewl (viewl xs))
= -- monoid law
x :< unviewl (viewl xs)
= -- by lemma above, unviewl . viewl = id
x :< xs

好的!现在我们拥有了我们需要的所有部件。
推论:如果 Sequence s , xs :: s a , 和 viewl xs = EmptyL ，然后 xs = mempty .
证明:假设， viewl xs = EmptyL .因此 unviewl (viewl xs) = unviewl EmptyL .由于 unviewl . viewl = id根据 unviewl 的定义, xs = mempty .
推论:如果 Sequence s , x :: a , 和 xs :: s a ，然后 viewl (singleton x <> xs) = x :< xs .
证明:

viewl (singleton x <> xs)
= -- viewl is a monoid morphism
viewl (singleton x) <> viewl xs
= -- lemma above
(x :< mempty) <> viewl xs
= -- definition of <>
x :< (mempty <> unviewl (viewl xs))
= -- monoid law and unviewl . viewl = id
x :< xs

推论:如果 viewl xs = y :< ys ，然后 xs = singleton y <> ys .
证明:申请 unviewl到前提两边， unviewl (viewl xs) = unviewl (y :< ys) .由于 unview l . viewl = id根据 unviewl 的定义，定理成立。

我已经证明了我所要做的一切。在我发现这些证明的过程中，我证明了 Sequence 的这个公式的其他几件事。 .我收集了 in this gist .