agda-spa/Lattice/Nat.agda

module Lattice.Nat where

open import Equivalence
open import Lattice
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; trans)
open import Data.Nat using (ℕ; _⊔_; _⊓_; _≤_)
open import Data.Nat.Properties using 
    ( ⊔-assoc; ⊔-comm; ⊔-idem
    ; ⊓-assoc; ⊓-comm; ⊓-idem
    ; ⊓-mono-≤; ⊔-mono-≤
    ; m≤n⇒m≤o⊔n; m≤n⇒m⊓o≤n; ≤-refl; ≤-antisym
    )

private
    ≡-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊔ a₃) ≡ (a₂ ⊔ a₄)
    ≡-⊔-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl

    ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
    ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl

isMaxSemilattice : IsSemilattice ℕ _≡_ _⊔_
isMaxSemilattice = record
    { ≈-equiv = record
        { ≈-refl = refl
        ; ≈-sym = sym
        ; ≈-trans = trans
        }
    ; ≈-⊔-cong = ≡-⊔-cong
    ; ⊔-assoc = ⊔-assoc
    ; ⊔-comm = ⊔-comm
    ; ⊔-idemp = ⊔-idem
    }

isMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
isMinSemilattice = record
    { ≈-equiv = record
        { ≈-refl = refl
        ; ≈-sym = sym
        ; ≈-trans = trans
        }
    ; ≈-⊔-cong = ≡-⊓-cong
    ; ⊔-assoc = ⊓-assoc
    ; ⊔-comm = ⊓-comm
    ; ⊔-idemp = ⊓-idem
    }

private
    max-bound₁ : {x y z : ℕ} → x ⊔ y ≡ z → x ≤ z
    max-bound₁ {x} {y} {z} x⊔y≡z
        rewrite sym x⊔y≡z
        rewrite ⊔-comm x y = m≤n⇒m≤o⊔n y (≤-refl)

    min-bound₁ : {x y z : ℕ} → x ⊓ y ≡ z → z ≤ x
    min-bound₁ {x} {y} {z} x⊓y≡z
        rewrite sym x⊓y≡z = m≤n⇒m⊓o≤n y (≤-refl)

    minmax-absorb : {x y : ℕ} → x ⊓ (x ⊔ y) ≡ x
    minmax-absorb {x} {y} = ≤-antisym x⊓x⊔y≤x (helper x⊓x≤x⊓x⊔y (⊓-idem x))
        where
            x⊓x⊔y≤x = min-bound₁ {x} {x ⊔ y} {x ⊓ (x ⊔ y)} refl
            x⊓x≤x⊓x⊔y = ⊓-mono-≤ {x} {x} ≤-refl (max-bound₁ {x} {y} {x ⊔ y} refl)

            -- >:(
            helper : x ⊓ x ≤ x ⊓ (x ⊔ y) → x ⊓ x ≡ x → x ≤ x ⊓ (x ⊔ y)
            helper x⊓x≤x⊓x⊔y x⊓x≡x rewrite x⊓x≡x = x⊓x≤x⊓x⊔y

    maxmin-absorb : {x y : ℕ} → x ⊔ (x ⊓ y) ≡ x
    maxmin-absorb {x} {y} = ≤-antisym (helper x⊔x⊓y≤x⊔x (⊔-idem x)) x≤x⊔x⊓y
        where
            x≤x⊔x⊓y = max-bound₁ {x} {x ⊓ y} {x ⊔ (x ⊓ y)} refl
            x⊔x⊓y≤x⊔x = ⊔-mono-≤ {x} {x} ≤-refl (min-bound₁ {x} {y} {x ⊓ y} refl)

            -- >:(
            helper : x ⊔ (x ⊓ y) ≤ x ⊔ x  → x ⊔ x ≡ x → x ⊔ (x ⊓ y) ≤ x
            helper x⊔x⊓y≤x⊔x x⊔x≡x rewrite x⊔x≡x = x⊔x⊓y≤x⊔x

isLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
isLattice = record
    { joinSemilattice = isMaxSemilattice
    ; meetSemilattice = isMinSemilattice
    ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
    ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
    }

lattice : Lattice ℕ
lattice = record
    { _≈_ = _≡_
    ; _⊔_ = _⊔_
    ; _⊓_ = _⊓_
    ; isLattice = isLattice
    }