module Order.Lattice.Reasoning {o β„“} {P : Poset o β„“} (lat : is-lattice P) where

Reasoning in latticesπŸ”—

This module provides some basic reasoning combinators for lattices.

First, we show that we have half of a distributive law that states that meets distribute over joins. For the converse to hold, must be a distributive lattice.

  βˆͺ-∩-distribl-≀ : βˆ€ {x y z} β†’ (x ∩ y) βˆͺ (x ∩ z) ≀ x ∩ (y βˆͺ z)
  βˆͺ-∩-distribl-≀ = βˆͺ-universal _
    (∩-universal _ βˆ©β‰€l (≀-trans βˆ©β‰€r l≀βˆͺ))
    (∩-universal _ βˆ©β‰€l (≀-trans βˆ©β‰€r r≀βˆͺ))

We can prove a dual result for joins distributing over meets.

  ∩-βˆͺ-distribl-≀ : βˆ€ {x y z} β†’ x βˆͺ (y ∩ z) ≀ (x βˆͺ y) ∩ (x βˆͺ z)
  ∩-βˆͺ-distribl-≀ = βˆͺ-universal _
    (∩-universal _ l≀βˆͺ l≀βˆͺ)
    (∩-universal _ (≀-trans βˆ©β‰€l r≀βˆͺ) (≀-trans βˆ©β‰€r r≀βˆͺ))

We also have absorptive laws for meets over joins (and joins over meets).

  ∩-absorbr : βˆ€ {x y} β†’ (x βˆͺ y) ∩ x ≑ x
  ∩-absorbr = ≀-antisym βˆ©β‰€r (∩-universal _ l≀βˆͺ ≀-refl)

  ∩-absorbl : βˆ€ {x y} β†’ x ∩ (x βˆͺ y) ≑ x
  ∩-absorbl = ∩-comm βˆ™ ∩-absorbr

  βˆͺ-absorbr : βˆ€ {x y} β†’ (x ∩ y) βˆͺ x ≑ x
  βˆͺ-absorbr = ≀-antisym (βˆͺ-universal _ βˆ©β‰€l ≀-refl) r≀βˆͺ

  βˆͺ-absorbl : βˆ€ {x y} β†’ x βˆͺ (x ∩ y) ≑ x
  βˆͺ-absorbl = βˆͺ-comm βˆ™ βˆͺ-absorbr