How to prove basic sequence properties

user_1477667 0
Viewed 183

As I understand it, one way to express that something is a free monoid is with a class like this:

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

and the following "universal construction" laws:

For any Monoid m and any function f :: a -> m,

  1. foldMap f . singleton = f
  2. foldMap f is a monoid morphism.
  3. foldMap f is the only function satisfying both 1 and 2.

Is this understanding correct?

If so, it would be nice to be able to use these laws to prove basic sequence properties. We can define

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)

How would I show the following?

  1. viewl s = EmptyL ==> s == mempty
  2. viewl s == a :< s' <==> s == singleton a <> s'

The converse of 1 follows immediately from foldMap f being a monoid morphism for all f, but I don't really know how to approach the above.

category-theory haskell
1 Answers

We will begin with a couple general lemmas about foldMap and singleton. The first lemma apparently follows from parametricity for any Foldable, but we can prove it directly for sequences using their laws.

Lemma (foldMap composition): Suppose Sequence s, Monoid m, and Monoid n. Let f :: a -> m be a function and let g :: m -> n be a monoid morphism. Then

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

Proof:

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

By the uniqueness of foldMap,

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

Lemma (rebuilding): For any Sequence s, foldMap @s (singleton @s) = id @s.

Proof: id @s . singleton @s = singleton @s. By the uniqueness of foldMap, id @s = foldMap @s (singleton @s).

Next, we will rewrite the Semigroup (ViewL s a) instance in a form that will prove easier to work with in the following. Just a bit of equational reasoning (using general case transformations and the monoid identity law) are sufficient to show that the following instance is equivalent (ignoring laziness, as I will throughout).

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

Lemma: unviewl is a monoid morphism.

Proof: We must show that unviewl mempty = mempty and that for any v1 and v2, unviewl v1 <> unviewl v2 = unviewl (v1 <> v2). The first is trivial.

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

For the second, we work by cases:

First case:

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

Second case:

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

Next, we show that viewl and unviewl are (full) inverses.

Lemma: unviewl . viewl = id

Proof:

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

Lemma (viewl of singleton): For any a, viewl (singleton a) = a :< mempty.

Proof:

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

Lemma: viewl . unviewl = id

Proof: Let v :: ViewL s a. We proceed by cases on v.

First case:

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

Second case:

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

Okay! Now we have all the pieces we need.

Corollary: If Sequence s, xs :: s a, and viewl xs = EmptyL, then xs = mempty.

Proof: By assumption, viewl xs = EmptyL. Thus unviewl (viewl xs) = unviewl EmptyL. Since unviewl . viewl = id and by the definition of unviewl, xs = mempty.

Corollary: If Sequence s, x :: a, and xs :: s a, then viewl (singleton x <> xs) = x :< xs.

Proof:

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

Corollary: If viewl xs = y :< ys, then xs = singleton y <> ys.

Proof: Applying unviewl to both sides of the premise, unviewl (viewl xs) = unviewl (y :< ys). Since unview l . viewl = id and by the definition of unviewl, the theorem holds.

I have proved all I set out to. On my way to discovering these proofs, I proved several other things about this formulation of Sequence. I have collected them in this gist.

user_14776670
Related