module Lattice where

import Data.Nat.Properties as NatProps
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym)
open import Relation.Binary.Definitions
open import Data.Nat as Nat using (ℕ; _≤_)
open import Data.Product using (_×_; _,_)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Agda.Primitive using (lsuc; Level)

open import NatMap using (NatMap)

record IsPreorder {a} (A : Set a) (_≼_ : A → A → Set a) : Set a where
    field
        ≼-refl : Reflexive (_≼_)
        ≼-trans : Transitive (_≼_)
        ≼-antisym : Antisymmetric (_≡_) (_≼_)

isPreorderFlip : {a : Level} → {A : Set a} → {_≼_ : A → A → Set a} → IsPreorder A _≼_ → IsPreorder A (λ x y → y ≼ x)
isPreorderFlip isPreorder = record
    { ≼-refl = IsPreorder.≼-refl isPreorder
    ; ≼-trans = λ {x} {y} {z} x≽y y≽z → IsPreorder.≼-trans isPreorder y≽z x≽y
    ; ≼-antisym = λ {x} {y} x≽y y≽x → IsPreorder.≼-antisym isPreorder y≽x x≽y
    }

record Preorder {a} (A : Set a) : Set (lsuc a) where
    field
        _≼_ : A → A → Set a

        isPreorder : IsPreorder A _≼_

    open IsPreorder isPreorder public

record IsSemilattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A → A) : Set a where
    field
        isPreorder : IsPreorder A _≼_

        ⊔-assoc : (x y z : A) → (x ⊔ y) ⊔ z ≡ x ⊔ (y ⊔ z)
        ⊔-comm : (x y : A) → x ⊔ y ≡ y ⊔ x
        ⊔-idemp : (x : A) → x ⊔ x ≡ x

        ⊔-bound : (x y z : A) → x ⊔ y ≡ z → (x ≼ z × y ≼ z)
        ⊔-least : (x y z : A) → x ⊔ y ≡ z → ∀ (z' : A) → (x ≼ z' × y ≼ z') → z ≼ z'

    open IsPreorder isPreorder public

record Semilattice {a} (A : Set a) : Set (lsuc a) where
    field
        _≼_ : A → A → Set a
        _⊔_ : A → A → A

        isSemilattice : IsSemilattice A _≼_ _⊔_

    open IsSemilattice isSemilattice public

record IsLattice {a} (A : Set a) (_≼_ : A → A → Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where

    _≽_ : A → A → Set a
    a ≽ b = b ≼ a

    field
        joinSemilattice : IsSemilattice A _≼_ _⊔_
        meetSemilattice : IsSemilattice A _≽_ _⊓_

        absorb-⊔-⊓ : (x y : A) → x ⊔ (x ⊓ y) ≡ x
        absorb-⊓-⊔ : (x y : A) → x ⊓ (x ⊔ y) ≡ x

    open IsSemilattice joinSemilattice public
    open IsSemilattice meetSemilattice public renaming
        ( ⊔-assoc to ⊓-assoc
        ; ⊔-comm to ⊓-comm
        ; ⊔-idemp to ⊓-idemp
        ; ⊔-bound to ⊓-bound
        ; ⊔-least to ⊓-least
        )


record Lattice {a} (A : Set a) : Set (lsuc a) where
    field
        _≼_ : A → A → Set a
        _⊔_ : A → A → A
        _⊓_ : A → A → A

        isLattice : IsLattice A _≼_ _⊔_ _⊓_

    open IsLattice isLattice public

private module NatInstances where
    open Nat
    open NatProps
    open Eq
    open Data.Sum

    NatPreorder : Preorder ℕ
    NatPreorder = record
        { _≼_ = _≤_
        ; isPreorder = record
            { ≼-refl = ≤-refl
            ; ≼-trans = ≤-trans
            ; ≼-antisym = ≤-antisym
            }
        }

    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)

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

        max-least : (x y z : ℕ) → x ⊔ y ≡ z → ∀ (z' : ℕ) → (x ≤ z' × y ≤ z') → z ≤ z'
        max-least x y z x⊔y≡z z' (x≤z' , y≤z') with (⊔-sel x y)
        ...                                    | inj₁ x⊔y≡x rewrite trans (sym x⊔y≡z) (x⊔y≡x) = x≤z'
        ...                                    | inj₂ x⊔y≡y rewrite trans (sym x⊔y≡z) (x⊔y≡y) = y≤z'

    NatMaxSemilattice : Semilattice ℕ
    NatMaxSemilattice = record
        { _≼_ = _≤_
        ; _⊔_ = _⊔_
        ; isSemilattice = record
            { isPreorder = Preorder.isPreorder NatPreorder
            ; ⊔-assoc = ⊔-assoc
            ; ⊔-comm = ⊔-comm
            ; ⊔-idemp = ⊔-idem
            ; ⊔-bound = λ x y z x⊔y≡z → (max-bound₁ x⊔y≡z , max-bound₂ x⊔y≡z)
            ; ⊔-least = max-least
            }
        }

    private
        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)

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

        min-greatest : (x y z : ℕ) → x ⊓ y ≡ z → ∀ (z' : ℕ) → (z' ≤ x × z' ≤ y) → z' ≤ z
        min-greatest x y z x⊓y≡z z' (z'≤x , z'≤y) with (⊓-sel x y)
        ...                                    | inj₁ x⊓y≡x rewrite trans (sym x⊓y≡z) (x⊓y≡x) = z'≤x
        ...                                    | inj₂ x⊓y≡y rewrite trans (sym x⊓y≡z) (x⊓y≡y) = z'≤y


    NatMinSemilattice : Semilattice ℕ
    NatMinSemilattice = record
        { _≼_ = _≥_
        ; _⊔_ = _⊓_
        ; isSemilattice = record
            { isPreorder = isPreorderFlip (Preorder.isPreorder NatPreorder)
            ; ⊔-assoc = ⊓-assoc
            ; ⊔-comm = ⊓-comm
            ; ⊔-idemp = ⊓-idem
            ; ⊔-bound = λ x y z x⊓y≡z → (min-bound₁ x⊓y≡z , min-bound₂ x⊓y≡z)
            ; ⊔-least = min-greatest
            }
        }

    private
        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

    NatLattice : Lattice ℕ
    NatLattice = record
        { _≼_ = _≤_
        ; _⊔_ = _⊔_
        ; _⊓_ = _⊓_
        ; isLattice = record
            { joinSemilattice = Semilattice.isSemilattice NatMaxSemilattice
            ; meetSemilattice = Semilattice.isSemilattice NatMinSemilattice
            ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
            ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
            }
        }