module Lattice where

open import Equivalence
import Chain

open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Relation.Nullary using (Dec; ¬_)
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) renaming (_⊔_ to _⊔ℓ_)
open import Function.Definitions using (Injective)

IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a
IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)

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

    _≼_ : A → A → Set a
    a ≼ b = Σ A (λ c → (a ⊔ c) ≈ b)

    _≺_ : A → A → Set a
    a ≺ b = (a ≼ b) × (¬ a ≈ b)

    field
        ≈-equiv : IsEquivalence A _≈_
        ≈-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → (a₁ ⊔ a₃) ≈ (a₂ ⊔ 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

    ≼-refl : ∀ (a : A) → a ≼ a
    ≼-refl a = (a , ⊔-idemp a)

    ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
    ≼-cong a₁≈a₂ a₃≈a₄ (c₁ , a₁⊔c₁≈a₃) = (c₁ , ≈-trans (≈-⊔-cong (≈-sym a₁≈a₂) ≈-refl) (≈-trans a₁⊔c₁≈a₃ a₃≈a₄))

    ≺-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≺ a₃ → a₂ ≺ a₄
    ≺-cong a₁≈a₂ a₃≈a₄ (a₁≼a₃ , a₁̷≈a₃) =
        ( ≼-cong a₁≈a₂ a₃≈a₄ a₁≼a₃
        , λ a₂≈a₄ → a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈a₄)))
        )

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 using () renaming
        ( ⊔-assoc to ⊓-assoc
        ; ⊔-comm to ⊓-comm
        ; ⊔-idemp to ⊓-idemp
        ; ≈-⊔-cong to ≈-⊓-cong
        ; _≼_ to _≽_
        ; _≺_ to _≻_
        ; ≼-refl to ≽-refl
        )

    FixedHeight : ∀ (h : ℕ) → Set a
    FixedHeight h = Chain.Height (_≈_) ≈-equiv _≺_ ≺-cong h

record IsFiniteHeightLattice {a} (A : Set a)
    (h : ℕ)
    (_≈_ : A → A → Set a)
    (_⊔_ : A → A → A)
    (_⊓_ : A → A → A) : Set (lsuc a) where

    field
        isLattice : IsLattice A _≈_ _⊔_ _⊓_

    open IsLattice isLattice public

    field
        fixedHeight : FixedHeight h

module _ {a b} {A : Set a} {B : Set b}
    (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where

    Monotonic : (A → B) → Set (a ⊔ℓ b)
    Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂

module ChainMapping {a b} {A : Set a} {B : Set b}
    {_≈₁_ : A → A → Set a} {_≈₂_ : B → B → Set b}
    {_⊔₁_ : A → A → A} {_⊔₂_ : B → B → B}
    (slA : IsSemilattice A _≈₁_ _⊔₁_) (slB : IsSemilattice B _≈₂_ _⊔₂_) where

    open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_; ≈-equiv to ≈₁-equiv; ≺-cong to ≺₁-cong)
    open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_; ≈-equiv to ≈₂-equiv; ≺-cong to ≺₂-cong)

    open Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong using () renaming (Chain to Chain₁; step to step₁; done to done₁)
    open Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong using () renaming (Chain to Chain₂; step to step₂; done to done₂)

    Chain-map : ∀ (f : A → B) →
                Monotonic _≼₁_ _≼₂_ f →
                Injective _≈₁_ _≈₂_ f →
                f Preserves _≈₁_ ⟶  _≈₂_ →
                ∀ {a₁ a₂ : A} {n : ℕ} → Chain₁ a₁ a₂ n → Chain₂ (f a₁) (f a₂) n
    Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (done₁ a₁≈a₂) =
        done₂ (Preservesᶠ a₁≈a₂)
    Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ (step₁ (a₁≼₁a , a₁̷≈₁a) a≈₁a' a'a₂) =
        let fa₁≺₂fa = (Monotonicᶠ a₁≼₁a , λ fa₁≈₂fa → a₁̷≈₁a (Injectiveᶠ fa₁≈₂fa))
            fa≈fa' = Preservesᶠ a≈₁a'
        in step₂ fa₁≺₂fa fa≈fa' (Chain-map f Monotonicᶠ Injectiveᶠ Preservesᶠ a'a₂)

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