open import Cat.Prelude

open import Data.Sum.Base

open import Order.Diagram.Join
open import Order.Diagram.Meet
open import Order.Lattice
open import Order.Base

import Order.Lattice.Reasoning as Lat
import Order.Reasoning as Pos
module Order.Lattice.Distributive {o ℓ} {P : Poset o ℓ} (l : is-lattice P) where
open Pos P
open Lat l

Distributive lattices🔗

A distributive lattice, as the name implies, is a lattice where the operations of meet and join distribute over each other: that is, for any triple of elements

Rather remarkably, it turns out that either equation implies the other. We provide a pair of parametrised modules which quantifies over one of the equations and proves the other. For convenience, these modules also define distributivity on the right, too; this is a consequence of both meets and joins being commutative operators.

module Distributive where
  module from-∩ (∩-distribl : ∀ {x y z} → x ∩ (y ∪ z) ≡ (x ∩ y) ∪ (x ∩ z)) where abstract
    ∩-distribr : ∀ {x y z} → (y ∪ z) ∩ x ≡ (y ∩ x) ∪ (z ∩ x)
    ∩-distribr = ∩-comm ∙∙ ∩-distribl ∙∙ ap₂ _∪_ ∩-comm ∩-comm

    ∪-distribl : ∀ {x y z} → x ∪ (y ∩ z) ≡ (x ∪ y) ∩ (x ∪ z)
    ∪-distribl {x} {y} {z} = sym $
      (x ∪ y) ∩ (x ∪ z)             ≡⟨ ∩-distribl ⟩
      ((x ∪ y) ∩ x) ∪ ((x ∪ y) ∩ z) ≡⟨ ap₂ _∪_ ∩-absorbr refl ⟩
      x ∪ ((x ∪ y) ∩ z)             ≡⟨ ap₂ _∪_ refl ∩-distribr ⟩
      x ∪ (x ∩ z ∪ y ∩ z)           ≡⟨ ∪-assoc ⟩
      (x ∪ x ∩ z) ∪ (y ∩ z)         ≡⟨ ap₂ _∪_ ∪-absorbl refl ⟩
      x ∪ (y ∩ z)                   ∎

    ∪-distribr : ∀ {x y z} → (y ∩ z) ∪ x ≡ (y ∪ x) ∩ (z ∪ x)
    ∪-distribr = ∪-comm ∙∙ ∪-distribl ∙∙ ap₂ _∩_ ∪-comm ∪-comm
The construction assuming that join distributes over meet is formally dual. 
  module from-∪ (∪-distribl : ∀ {x y z} → x ∪ (y ∩ z) ≡ (x ∪ y) ∩ (x ∪ z)) where abstract
    ∪-distribr : ∀ {x y z} → (y ∩ z) ∪ x ≡ (y ∪ x) ∩ (z ∪ x)
    ∪-distribr = ∪-comm ∙∙ ∪-distribl ∙∙ ap₂ _∩_ ∪-comm ∪-comm

    ∩-distribl : ∀ {x y z} → x ∩ (y ∪ z) ≡ (x ∩ y) ∪ (x ∩ z)
    ∩-distribl {x} {y} {z} = sym $
      (x ∩ y) ∪ (x ∩ z)             ≡⟨ ∪-distribl ⟩
      ((x ∩ y) ∪ x) ∩ ((x ∩ y) ∪ z) ≡⟨ ap₂ _∩_ ∪-absorbr refl ⟩
      x ∩ ((x ∩ y) ∪ z)             ≡⟨ ap₂ _∩_ refl ∪-distribr ⟩
      x ∩ (x ∪ z) ∩ (y ∪ z)         ≡⟨ ∩-assoc ⟩
      (x ∩ (x ∪ z)) ∩ (y ∪ z)       ≡⟨ ap₂ _∩_ ∩-absorbl refl ⟩
      x ∩ (y ∪ z)                   ∎

    ∩-distribr : ∀ {x y z} → (y ∪ z) ∩ x ≡ (y ∩ x) ∪ (z ∩ x)
    ∩-distribr = ∩-comm ∙∙ ∩-distribl ∙∙ ap₂ _∪_ ∩-comm ∩-comm

As a further weakening of the preconditions, it turns out that it suffices for distributivity to hold as an inequality, in the direction

since the other direction always holds in a lattice.

distrib-le→∩-distribl
  : (∀ {x y z} → x ∩ (y ∪ z) ≤ (x ∩ y) ∪ (x ∩ z))
  → ∀ {x y z} → x ∩ (y ∪ z) ≡ (x ∩ y) ∪ (x ∩ z)
distrib-le→∩-distribl ∩-∪-distrib≤ = ≤-antisym ∩-∪-distrib≤ ∪-∩-distribl-≤