open import Cat.Prelude

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

import Order.Semilattice.Join.Reasoning
import Order.Semilattice.Meet.Reasoning
import Order.Reasoning as Pos

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

open is-lattice lat public
open Pos P


# Reasoning in latticesπ

This module provides some basic reasoning combinators for lattices.

open Order.Semilattice.Meet.Reasoning has-meet-slat using (β©-idl; β©-idr; module β©) public
open Order.Semilattice.Join.Reasoning has-join-slat using (βͺ-idl; βͺ-idr; module βͺ) public


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.

abstract


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

  β©-βͺ-distribl-β€ : β {x y z} β x βͺ (y β© z) β€ (x βͺ y) β© (x βͺ z)

  βͺ-β©-distribr-β€ : β {x y z} β (x β© z) βͺ (y β© z) β€ (x βͺ y) β© z

β©-βͺ-distribr-β€ : β {x y z} β (x β© y) βͺ z β€ (x βͺ z) β© (y βͺ z)


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

  β©-absorbr : β {x y} β (x βͺ y) β© x β‘ x