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 IsSemilattice {a} (A : Set a) (_⊔_ : A → A → A) : Set a where
    field
        ⊔-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

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

        isSemilattice : IsSemilattice A _⊔_

    open IsSemilattice isSemilattice public

record IsLattice {a} (A : Set a) (_⊔_ : A → A → A) (_⊓_ : A → A → A) : Set a where
    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
        )


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

        isLattice : IsLattice A _⊔_ _⊓_

    open IsLattice isLattice public

module SemilatticeInstances where
    module ForNat where
        open Nat
        open NatProps
        open Eq

        NatMaxSemilattice : Semilattice ℕ
        NatMaxSemilattice = record
            { _⊔_ = _⊔_
            ; isSemilattice = record
                { ⊔-assoc = ⊔-assoc
                ; ⊔-comm = ⊔-comm
                ; ⊔-idemp = ⊔-idem
                }
            }

        NatMinSemilattice : Semilattice ℕ
        NatMinSemilattice = record
            { _⊔_ = _⊓_
            ; isSemilattice = record
                { ⊔-assoc = ⊓-assoc
                ; ⊔-comm = ⊓-comm
                ; ⊔-idemp = ⊓-idem
                }
            }

    module ForProd {a} {A B : Set a} (sA : Semilattice A) (sB : Semilattice B) where
        open Eq
        open Data.Product

        private
            _⊔_ : A × B → A × B → A × B
            (a₁ , b₁) ⊔ (a₂ , b₂) = (Semilattice._⊔_ sA a₁ a₂ , Semilattice._⊔_ sB b₁ b₂)

            ⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≡ p₁ ⊔ (p₂ ⊔ p₃)
            ⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃)
                rewrite Semilattice.⊔-assoc sA a₁ a₂ a₃
                rewrite Semilattice.⊔-assoc sB b₁ b₂ b₃ = refl

            ⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≡ p₂ ⊔ p₁
            ⊔-comm (a₁ , b₁) (a₂ , b₂)
                rewrite Semilattice.⊔-comm sA a₁ a₂
                rewrite Semilattice.⊔-comm sB b₁ b₂ = refl

            ⊔-idemp : (p : A × B) → p ⊔ p ≡ p
            ⊔-idemp (a , b)
                rewrite Semilattice.⊔-idemp sA a
                rewrite Semilattice.⊔-idemp sB b = refl

        ProdSemilattice : Semilattice (A × B)
        ProdSemilattice = record
            { _⊔_ = _⊔_
            ; isSemilattice = record
                { ⊔-assoc = ⊔-assoc
                ; ⊔-comm = ⊔-comm
                ; ⊔-idemp = ⊔-idemp
                }
            }

module LatticeInstances where
    module ForNat where
        open Nat
        open NatProps
        open Eq
        open SemilatticeInstances.ForNat
        open Data.Product


        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

        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}
                }
            }

    module ForProd {a} {A B : Set a} (lA : Lattice A) (lB : Lattice B) where
        private
            module ProdJoin = SemilatticeInstances.ForProd
                record { _⊔_ = Lattice._⊔_ lA; isSemilattice = Lattice.joinSemilattice lA }
                record { _⊔_ = Lattice._⊔_ lB; isSemilattice = Lattice.joinSemilattice lB }
            module ProdMeet = SemilatticeInstances.ForProd
                record { _⊔_ = Lattice._⊓_ lA; isSemilattice = Lattice.meetSemilattice lA }
                record { _⊔_ = Lattice._⊓_ lB; isSemilattice = Lattice.meetSemilattice lB }

            _⊔_ = Semilattice._⊔_ ProdJoin.ProdSemilattice
            _⊓_ = Semilattice._⊔_ ProdMeet.ProdSemilattice

        open Eq
        open Data.Product

        private
            absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≡ p₁
            absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂)
                rewrite Lattice.absorb-⊔-⊓ lA a₁ a₂
                rewrite Lattice.absorb-⊔-⊓ lB b₁ b₂ = refl

            absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≡ p₁
            absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂)
                rewrite Lattice.absorb-⊓-⊔ lA a₁ a₂
                rewrite Lattice.absorb-⊓-⊔ lB b₁ b₂ = refl

        ProdLattice : Lattice (A × B)
        ProdLattice = record
            { _⊔_ = _⊔_
            ; _⊓_ = _⊓_
            ; isLattice = record
                { joinSemilattice = Semilattice.isSemilattice ProdJoin.ProdSemilattice
                ; meetSemilattice = Semilattice.isSemilattice ProdMeet.ProdSemilattice
                ; absorb-⊔-⊓ = absorb-⊔-⊓
                ; absorb-⊓-⊔ = absorb-⊓-⊔
                }
            }