# A Simple Exercise using the Modular Law

Josh needs a property for which there is an obvious pointwise proof. He wonders whether it is possible to prove it in point-free style. I haven’t practised point-free proofs for a while, so I’d give it a try.

The actual property he needs is that FT . C ⊆ C . FT . C where C is a coreflexive, given T ⊆ ⦇S⦈ and F⦇S⦈ . C ⊆ C . F⦇S⦈ . C. It is sufficient to prove this generalised property:

Intuitively speaking, if C covers the range of R and S ⊆ R, then C covers the range of S too.

Well, the proof goes:

= { since C . C = C }
C . C . S
{ since X ⊇ X ∩ Y }
C . ((C . S) ∩ R)
{ modular law X ∩ (Y.Z) ⊆ Y . ((Y˘.X) ∩ Z), and C˘ = C }
S ∩ (C . R)
{ given: R ⊆ C . R }
S ∩ R
= { given: S ⊆ R }
S

It is hard to explain the intuition behind the use of modular law. If we take C as a predicate, the property can be written pointwisely as:

where a and b are both universally quantified. We may simplify b S a ⇒ C b ∧ b S a to b S a ⇒ C b, but that makes it more difficult to see the connection. Essentially, I was mimicking the following obvious proof:

{ strengthening }
C b ∧ b S a ∧ b R a
{ since b R a ⇒ C b ∧ b R a }
b S a ∧ b R a
{ since b S a ⇒ b R a }
b S a

The strengthening step corresponds to the use of X ⊇ X ∩ Y, while the next two steps respectively correspond to the last two steps of the point-free proof. The modular law, implicit in the pointwise proof, was used to group C and R to the right places.