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
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
The definition induces the universal property:
And here are some basic properties we will make use of later:
The Thinning Theorem
The thinning theorem says :
Theorem: if
Proof. By fold fusion, the theorem holds if
By the universal property of thin, the above inclusion is equivalent to
The first inclusion is proved by:
And the second by:
Endproof.
By the way, the variation of thinning theorem I need is “