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 IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where
    field
        ≈-refl : {a : A} → a ≈ a
        ≈-sym : {a b : A} → a ≈ b → b ≈ a
        ≈-trans : {a b c : A} → a ≈ b → b ≈ c → a ≈ c

record IsSemilattice {a} (A : Set a)
    (_≈_ : A → A → Set a)
    (_⊔_ : A → A → A) : Set a where

    field
        ≈-equiv : IsEquivalence 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

    open IsEquivalence ≈-equiv public

record IsLattice {a} (A : Set a)
    (_≈_ : 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 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 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

module IsEquivalenceInstances where
    module ForMap {a b} (A : Set a) (B : Set b)
        (≡-dec-A : Decidable (_≡_ {a} {A}))
        (_≈₂_ : B → B → Set b)
        (eB : IsEquivalence B _≈₂_) where

        open import Map A B ≡-dec-A using (Map; lift; subset)
        open import Data.List using (_∷_; []) -- TODO: re-export these with nicer names from map

        open IsEquivalence eB renaming
            ( ≈-refl to ≈₂-refl
            ; ≈-sym to ≈₂-sym
            ; ≈-trans to ≈₂-trans
            )

        private
            _≈_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
            _≈_ = lift _≈₂_

            _⊆_ : Map → Map → Set (Agda.Primitive._⊔_ a b)
            _⊆_ = subset _≈₂_

            ⊆-refl : (m : Map) →  m ⊆ m
            ⊆-refl _ k v k,v∈m = (v , (≈₂-refl , k,v∈m))

            ⊆-trans : (m₁ m₂ m₃ : Map) →  m₁ ⊆ m₂ → m₂ ⊆ m₃ → m₁ ⊆ m₃
            ⊆-trans _ _ _ m₁⊆m₂ m₂⊆m₃ k v k,v∈m₁ =
                let
                    (v' , (v≈v' , k,v'∈m₂)) = m₁⊆m₂ k v k,v∈m₁
                    (v'' , (v'≈v'' , k,v''∈m₃)) = m₂⊆m₃ k v' k,v'∈m₂
                in (v'' , (≈₂-trans v≈v' v'≈v'' , k,v''∈m₃))

            ≈-refl : (m : Map) → m ≈ m
            ≈-refl m = (⊆-refl m , ⊆-refl m)

            ≈-sym : (m₁ m₂ : Map) → m₁ ≈ m₂ → m₂ ≈ m₁
            ≈-sym _ _ (m₁⊆m₂ , m₂⊆m₁) = (m₂⊆m₁ , m₁⊆m₂)

            ≈-trans : (m₁ m₂ m₃ : Map) → m₁ ≈ m₂ → m₂ ≈ m₃ → m₁ ≈ m₃
            ≈-trans m₁ m₂ m₃ (m₁⊆m₂ , m₂⊆m₁) (m₂⊆m₃ , m₃⊆m₂) =
                ( ⊆-trans m₁ m₂ m₃ m₁⊆m₂ m₂⊆m₃
                , ⊆-trans m₃ m₂ m₁ m₃⊆m₂ m₂⊆m₁
                )

        LiftEquivalence : IsEquivalence Map _≈_
        LiftEquivalence = record
            { ≈-refl = λ {m₁} → ≈-refl m₁
            ; ≈-sym = λ {m₁} {m₂} → ≈-sym m₁ m₂
            ; ≈-trans = λ {m₁} {m₂} {m₃} → ≈-trans m₁ m₂ m₃
            }

module IsSemilatticeInstances where
    module ForNat where
        open Nat
        open NatProps
        open Eq

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

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

    module ForProd {a} {A B : Set a}
        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
        (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → B)
        (sA : IsSemilattice A _≈₁_ _⊔₁_) (sB : IsSemilattice B _≈₂_ _⊔₂_) where

        open Eq
        open Data.Product

        private
            infix 4 _≈_
            infixl 20 _⊔_

            _≈_ : A × B → A × B → Set a
            (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)

            _⊔_ : A × B → A × B → A × B
            (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)

            ⊔-assoc : (p₁ p₂ p₃ : A × B) → (p₁ ⊔ p₂) ⊔ p₃ ≈ p₁ ⊔ (p₂ ⊔ p₃)
            ⊔-assoc (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) =
                ( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
                , IsSemilattice.⊔-assoc sB b₁ b₂ b₃
                )

            ⊔-comm : (p₁ p₂ : A × B) → p₁ ⊔ p₂ ≈ p₂ ⊔ p₁
            ⊔-comm (a₁ , b₁) (a₂ , b₂) =
                ( IsSemilattice.⊔-comm sA a₁ a₂
                , IsSemilattice.⊔-comm sB b₁ b₂
                )

            ⊔-idemp : (p : A × B) → p ⊔ p ≈ p
            ⊔-idemp (a , b) =
                ( IsSemilattice.⊔-idemp sA a
                , IsSemilattice.⊔-idemp sB b
                )

            ≈-refl : {p : A × B} → p ≈ p
            ≈-refl =
                ( IsSemilattice.≈-refl sA
                , IsSemilattice.≈-refl sB
                )

            ≈-sym : {p₁ p₂ : A × B} → p₁ ≈ p₂ → p₂ ≈ p₁
            ≈-sym (a₁≈a₂ , b₁≈b₂) =
                ( IsSemilattice.≈-sym sA a₁≈a₂
                , IsSemilattice.≈-sym sB b₁≈b₂
                )

            ≈-trans : {p₁ p₂ p₃ : A × B} → p₁ ≈ p₂ → p₂ ≈ p₃ → p₁ ≈ p₃
            ≈-trans (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) =
                ( IsSemilattice.≈-trans sA a₁≈a₂ a₂≈a₃
                , IsSemilattice.≈-trans sB b₁≈b₂ b₂≈b₃
                )


        ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
        ProdIsSemilattice = record
            { ≈-equiv = record
                { ≈-refl = ≈-refl
                ; ≈-sym = ≈-sym
                ; ≈-trans = ≈-trans
                }
            ; ⊔-assoc = ⊔-assoc
            ; ⊔-comm = ⊔-comm
            ; ⊔-idemp = ⊔-idemp
            }

    module ForMap {a} {A B : Set a}
        (≡-dec-A : Decidable (_≡_ {a} {A}))
        (_≈₂_ : B → B → Set a)
        (_⊔₂_ : B → B → B)
        (sB : IsSemilattice B _≈₂_ _⊔₂_) where

        open import Map A B ≡-dec-A
        open IsSemilattice sB renaming
            ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym
            ; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
            )

        private
            infix 4 _≈_
            infixl 20 _⊔_

            _≈_ : Map → Map → Set a
            _≈_ = lift (_≈₂_)

            _⊔_ : Map → Map → Map
            m₁ ⊔ m₂ = union _⊔₂_ m₁ m₂

            _⊓_ : Map → Map → Map
            m₁ ⊓ m₂ = intersect _⊔₂_ m₁ m₂

        module MapEquiv = IsEquivalenceInstances.ForMap A B ≡-dec-A _≈₂_ (IsSemilattice.≈-equiv sB)

        MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
        MapIsUnionSemilattice = record
            { ≈-equiv = MapEquiv.LiftEquivalence
            ; ⊔-assoc = union-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
            ; ⊔-comm = union-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
            ; ⊔-idemp = union-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
            }

        MapIsIntersectSemilattice : IsSemilattice Map _≈_ _⊓_
        MapIsIntersectSemilattice = record
            { ≈-equiv = MapEquiv.LiftEquivalence
            ; ⊔-assoc = intersect-assoc _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-assoc
            ; ⊔-comm = intersect-comm _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-comm
            ; ⊔-idemp = intersect-idemp _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ ⊔₂-idemp
            }

module IsLatticeInstances where
    module ForNat where
        open Nat
        open NatProps
        open Eq
        open IsSemilatticeInstances.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

        NatIsLattice : IsLattice ℕ _≡_ _⊔_ _⊓_
        NatIsLattice = record
            { joinSemilattice = NatIsMaxSemilattice
            ; meetSemilattice = NatIsMinSemilattice
            ; absorb-⊔-⊓ = λ x y → maxmin-absorb {x} {y}
            ; absorb-⊓-⊔ = λ x y → minmax-absorb {x} {y}
            }

    module ForProd {a} {A B : Set a}
        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
        (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
        (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
        (lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_) (lB : IsLattice B _≈₂_ _⊔₂_ _⊓₂_) where

        private
            module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
            module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)

            infix 4 _≈_
            infixl 20 _⊔_

            _≈_ : (A × B) → (A × B) → Set a
            (a₁ , b₁) ≈ (a₂ , b₂) = (a₁ ≈₁ a₂) × (b₁ ≈₂ b₂)

            _⊔_ : (A × B) → (A × B) → (A × B)
            (a₁ , b₁) ⊔ (a₂ , b₂) = (a₁ ⊔₁ a₂ , b₁ ⊔₂ b₂)

            _⊓_ : (A × B) → (A × B) → (A × B)
            (a₁ , b₁) ⊓ (a₂ , b₂) = (a₁ ⊓₁ a₂ , b₁ ⊓₂ b₂)

        open Eq
        open Data.Product

        private
            absorb-⊔-⊓ : (p₁ p₂ : A × B) → p₁ ⊔ (p₁ ⊓ p₂) ≈ p₁
            absorb-⊔-⊓ (a₁ , b₁) (a₂ , b₂) =
                ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
                , IsLattice.absorb-⊔-⊓ lB b₁ b₂
                )

            absorb-⊓-⊔ : (p₁ p₂ : A × B) → p₁ ⊓ (p₁ ⊔ p₂) ≈ p₁
            absorb-⊓-⊔ (a₁ , b₁) (a₂ , b₂) =
                ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
                , IsLattice.absorb-⊓-⊔ lB b₁ b₂
                )

        ProdIsLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
        ProdIsLattice = record
            { joinSemilattice = ProdJoin.ProdIsSemilattice
            ; meetSemilattice = ProdMeet.ProdIsSemilattice
            ; absorb-⊔-⊓ = absorb-⊔-⊓
            ; absorb-⊓-⊔ = absorb-⊓-⊔
            }