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:

$S\; \subseteq \; C\; .\; S\; \; \Leftarrow \; \; R\; \subseteq \; C\; .\; R\; \; \wedge \; \; S\; \subseteq \; R$

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

Well, the proof goes:

$\; C\; .\; S\; =\{\; since\mathrm{C\; .\; C\; =\; C}\} \; C\; .\; C\; .\; S\; \supseteq \{\; since\mathrm{X\; \supseteq \; X\; \cap \; Y}\} \; \; C\; .\; ((C\; .\; S)\; \cap \; R)\; \supseteq \{\; modular\; law\mathrm{X\; \cap \; (Y.Z)\; \subseteq \; Y\; .\; ((Y˘.X)\; \cap \; Z)},\; and\mathrm{C˘\; =\; C}\} \; \; S\; \cap \; (C\; .\; R)\; \supseteq \{\; given:\mathrm{R\; \subseteq \; C\; .\; R}\} \; \; S\; \cap \; R\; =\{\; given:\mathrm{S\; \subseteq \; 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:

$(b\; S\; a\; \Rightarrow \; C\; b\; \wedge \; b\; S\; a)\; \; \Leftarrow \; \; (b\; R\; a\; \Rightarrow \; C\; b\; \wedge \; b\; R\; a)\; \; \wedge \; \; b\; S\; a\; \Rightarrow \; b\; R\; a$

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:

$\; C\; b\; \wedge \; b\; S\; a\; \Leftarrow \{\; strengthening\; \} \; C\; b\; \wedge \; b\; S\; a\; \wedge \; b\; R\; a\; \Leftarrow \{\; since\mathrm{b\; R\; a\; \Rightarrow \; C\; b\; \wedge \; b\; R\; a}\} \; b\; S\; a\; \wedge \; b\; R\; a\; \Leftarrow \{\; since\mathrm{b\; S\; a\; \Rightarrow \; 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.