Proving the Thinning Theorem by Fold Fusion

Algebra of Programming records two proofs of the greedy and the thinning theorems slightly shorter than proofs using fold fusion. Of course, one can still use fold fusion. In fact, proving them by fold fusion are exercises in Chapter 8 (PDF) of Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, of which I myself is listed among the authors.

A while ago when I needed to consider some variations of the thinning theorem I tried to do the proof again. And, horrifyingly, I could not do it anymore! Have my skills become rusty due to lack of practice in the past few years? In panic, I spent an entire afternoon fighting with it, until I realised that it was just a typical copying error from the very beginning: when I copied a property from the book I put in an extra Λ. Then I trapped myself in the maze of expanding ΛR into ∈\R ∩ (R\∈) and using modular law and ….

Having fixed the error, I get my trivial and easy proof back again. Anyway, I am going to record it below, in case I run into the same panic again.

Given a preorder Q, the relation thin Q is defined by:

$thin\; Q\; =\; \in \backslash \in \; \cap \; (\ni \; .\; Q)/\ni$

The definition induces the universal property:

$X\; \subseteq \; thin\; Q\; .\; \Lambda S \equiv \; \in \; .\; X\; \subseteq \; S\; \bigwedge \; X\; .\; S˘\; \subseteq \; \ni .Q$

And here are some basic properties we will make use of later:

$(R\; .\; S)˘\; =\; S˘\; .\; R˘,\; \; (R\backslash S)˘\; =\; S˘/R˘ \; (converse)$
∈ . ΛS = S       (power transpose)
ΛR . R˘ ⊆ ∋
R . R\S ⊆ S,       R/S . S ⊆ R       (division)

The Thinning Theorem

The thinning theorem says :
Theorem: if S is monotonic on preorder Q, that is, S . FQ˘⊆ Q˘. S, we have:

$fold\; (thin\; Q\; .\; \Lambda (S\; .\; F\in ))\; \subseteq \; thin\; Q\; .\; \Lambda (fold\; S)$

Proof. By fold fusion, the theorem holds if

$thin\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(thin\; Q)\; \subseteq \; thin\; Q\; .\; \Lambda (S\; .\; F\in )$

By the universal property of thin, the above inclusion is equivalent to

$\in \; .\; thin\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(thin\; Q)\; \subseteq \; S\; .\; F\in \bigwedge$
thin Q . Λ(S . F∈) . F(thin Q) . (S . F∈)˘ ⊆ ∋.Q

The first inclusion is proved by:

$\; \in \; .\; thin\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(thin\; Q)$
⊆ { since thin Q ⊆ ∈\∈ }
    ∈ . ∈\∈ . Λ(S . F∈) . F(thin Q)
⊆ { division }
    ∈ . Λ(S . F∈) . F(thin Q)
= { power transpose }
    S . F∈ . F(thin Q)
⊆ { since thin Q ⊆ ∈\∈ }
    S . F∈ . F(∈\∈)
⊆ { division }
    S . F∈

And the second by:

$\; thin\; Q\; .\; \Lambda (S\; .\; F\in )\; .\; F(thin\; Q)\; .\; (S\; .\; F\in )˘$
⊆ { since thin Q ⊆ (∋ . Q)/∋, converse }
    thin Q . Λ(S . F∈) . F((∋ . Q)/∋) . F∋ . S˘
⊆ { functor, division }
    thin Q . Λ(S . F∈) . F(∋ . Q) . S˘
⊆ { monotonicity: FQ . S˘ ⊆ S˘. Q }
    thin Q . Λ(S . F∈) . F∋ . S˘. Q
⊆ { since ΛR . R ⊆ ∋ }
    thin Q . ∋ . Q
⊆ { since thin Q ⊆ (∋.Q)/∋, division }
    ∋ . Q . Q
⊆ { since Q transitive }
    ∋ . Q

Endproof.

By the way, the variation of thinning theorem I need is “fold (thin Q . Λ(S . F∈)) ⊆ thin Q . Λ(fold S) if S . F(Q˘. ∈) ⊆ Q˘. S . F ∈ “, whose proof is, luckily, trivial once you write down the original proof.