agda-spa/Lattice.agda

module Lattice where

open import Equivalence
import Chain

open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Data.Empty using (⊥-elim)
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)

record IsDecidable {a} {A : Set a} (R : A → A → Set a) : Set a where
    field
        R-dec : ∀ (a₁ a₂ : A) → Dec (R a₁ a₂)

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₂

    Monotonicˡ : ∀ {c} {C : Set c} → (A → C → B) →  Set (a ⊔ℓ b ⊔ℓ c)
    Monotonicˡ f = ∀ c →  Monotonic (λ a → f a c)

    Monotonicʳ : ∀ {c} {C : Set c} → (C → A → B) →  Set (a ⊔ℓ b ⊔ℓ c)
    Monotonicʳ f = ∀ a → Monotonic (f a)

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

    Monotonic₂ : (A → B → C) → Set (a ⊔ℓ b ⊔ℓ c)
    Monotonic₂ f = Monotonicˡ _≼₁_ _≼₃_ f × Monotonicʳ _≼₂_ _≼₃_ f

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

    _≼_ : A → A → Set a
    a ≼ b = (a ⊔ b) ≈ 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

    open import Relation.Binary.Reasoning.Base.Single _≈_ ≈-refl ≈-trans

    ⊔-Monotonicˡ : ∀ (a₁ : A) → Monotonic _≼_ _≼_ (λ a₂ → a₁ ⊔ a₂)
    ⊔-Monotonicˡ a {a₁} {a₂} a₁≼a₂ = ≈-trans (≈-sym lhs) (≈-⊔-cong (≈-refl {a}) a₁≼a₂)
        where
            lhs =
                begin
                    a ⊔ (a₁ ⊔ a₂)
                ∼⟨ ≈-⊔-cong (≈-sym (⊔-idemp _)) ≈-refl ⟩
                    (a ⊔ a) ⊔ (a₁ ⊔ a₂)
                ∼⟨ ⊔-assoc _ _ _ ⟩
                    a ⊔ (a ⊔ (a₁ ⊔ a₂))
                ∼⟨ ≈-⊔-cong ≈-refl (≈-sym (⊔-assoc _ _ _)) ⟩
                    a ⊔ ((a ⊔ a₁) ⊔ a₂)
                ∼⟨ ≈-⊔-cong ≈-refl (≈-⊔-cong (⊔-comm _ _) ≈-refl) ⟩
                    a ⊔ ((a₁ ⊔ a) ⊔ a₂)
                ∼⟨ ≈-⊔-cong ≈-refl (⊔-assoc _ _ _) ⟩
                    a ⊔ (a₁ ⊔ (a ⊔ a₂))
                ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
                    (a ⊔ a₁) ⊔ (a ⊔ a₂)
                ∎

    ⊔-Monotonicʳ : ∀ (a₂ : A) → Monotonic _≼_ _≼_ (λ a₁ → a₁ ⊔ a₂)
    ⊔-Monotonicʳ a {a₁} {a₂} a₁≼a₂ = ≈-trans (≈-sym lhs) (≈-⊔-cong a₁≼a₂ (≈-refl {a}))
        where
            lhs =
                begin
                    (a₁ ⊔ a₂) ⊔ a
                ∼⟨ ≈-⊔-cong ≈-refl (≈-sym (⊔-idemp _)) ⟩
                    (a₁ ⊔ a₂) ⊔ (a ⊔ a)
                ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
                    ((a₁ ⊔ a₂) ⊔ a) ⊔ a
                ∼⟨ ≈-⊔-cong (⊔-assoc _ _ _) ≈-refl ⟩
                    (a₁ ⊔ (a₂ ⊔ a)) ⊔ a
                ∼⟨ ≈-⊔-cong (≈-⊔-cong ≈-refl (⊔-comm _ _)) ≈-refl ⟩
                    (a₁ ⊔ (a ⊔ a₂)) ⊔ a
                ∼⟨ ≈-⊔-cong (≈-sym (⊔-assoc _ _ _)) ≈-refl ⟩
                    ((a₁ ⊔ a) ⊔ a₂) ⊔ a
                ∼⟨ ⊔-assoc _ _ _ ⟩
                    (a₁ ⊔ a) ⊔ (a₂ ⊔ a)
                ∎

    -- need to show: a₁ ⊔ (a₁ ⊔ a₂) ≈ a₁ ⊔ a₂
    -- (a₁ ⊔ a₁) ⊔ a₂ ≈ a₁ ⊔ (a₁ ⊔ a₂)

    x≼x⊔y : ∀ (a₁ a₂ : A) → a₁ ≼ (a₁ ⊔ a₂)
    x≼x⊔y a₁ a₂ = ≈-sym (≈-trans (≈-⊔-cong (≈-sym (⊔-idemp a₁)) (≈-refl {a₂})) (⊔-assoc a₁ a₁ a₂))

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

    ≼-trans : ∀ {a₁ a₂ a₃ : A} → a₁ ≼ a₂ → a₂ ≼ a₃ → a₁ ≼ a₃
    ≼-trans {a₁} {a₂} {a₃} a₁≼a₂ a₂≼a₃ =
        begin
            a₁ ⊔ a₃
        ∼⟨ ≈-⊔-cong ≈-refl (≈-sym a₂≼a₃) ⟩
            a₁ ⊔ (a₂ ⊔ a₃)
        ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩
            (a₁ ⊔ a₂) ⊔ a₃
        ∼⟨ ≈-⊔-cong a₁≼a₂ ≈-refl ⟩
            a₂ ⊔ a₃
        ∼⟨ a₂≼a₃ ⟩
            a₃
        ∎

    ≼-antisym : ∀ {a₁ a₂ : A} → a₁ ≼ a₂ → a₂ ≼ a₁ → a₁ ≈ a₂
    ≼-antisym {a₁} {a₂} a₁⊔a₂≈a₂ a₂⊔a₁≈a₁ =
        begin
            a₁
        ∼⟨ ≈-sym a₂⊔a₁≈a₁ ⟩
            a₂ ⊔ a₁
        ∼⟨ ⊔-comm _ _ ⟩
            a₁ ⊔ a₂
        ∼⟨ a₁⊔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₄ a₁⊔a₃≈a₃ =
        begin
            a₂ ⊔ a₄
        ∼⟨ ≈-⊔-cong (≈-sym a₁≈a₂) (≈-sym a₃≈a₄) ⟩
            a₁ ⊔ a₃
        ∼⟨ a₁⊔a₃≈a₃ ⟩
            a₃
        ∼⟨ 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₄)))
        )

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

    open IsSemilattice lA using (_≼_)

    id-Mono : Monotonic _≼_ _≼_ (λ x → x)
    id-Mono {a₁} {a₂} a₁≼a₂ = a₁≼a₂

module _ {a b} {A : Set a} {B : Set b}
         {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A}
         {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
         (lA : IsSemilattice A _≈₁_ _⊔₁_) (lB : IsSemilattice B _≈₂_ _⊔₂_) where

    open IsSemilattice lA using () renaming (_≼_ to _≼₁_)
    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)

    const-Mono : ∀ (x : B) → Monotonic _≼₁_ _≼₂_ (λ _ → x)
    const-Mono x _ = ⊔₂-idemp x

    open import Data.List as List using (List; foldr; foldl; _∷_)
    open import Utils using (Pairwise; _∷_)

    foldr-Mono : ∀ (l₁ l₂ : List A) (f : A → B → B) (b₁ b₂ : B) →
                 Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
                 (∀ b → Monotonic _≼₁_ _≼₂_ (λ a → f a b)) →
                 (∀ a → Monotonic _≼₂_ _≼₂_ (f a)) →
                 foldr f b₁ l₁ ≼₂ foldr f b₂ l₂
    foldr-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
    foldr-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
        ≼₂-trans (f-Mono₁ (foldr f b₁ xs) x≼y)
                 (f-Mono₂ y (foldr-Mono xs ys f b₁ b₂ xs≼ys b₁≼b₂ f-Mono₁ f-Mono₂))

    foldl-Mono : ∀ (l₁ l₂ : List A) (f : B → A → B) (b₁ b₂ : B) →
                 Pairwise _≼₁_ l₁ l₂ → b₁ ≼₂ b₂ →
                 (∀ a → Monotonic _≼₂_ _≼₂_ (λ b → f b a)) →
                 (∀ b → Monotonic _≼₁_ _≼₂_ (f b)) →
                 foldl f b₁ l₁ ≼₂ foldl f b₂ l₂
    foldl-Mono List.[] List.[] f b₁ b₂ _ b₁≼b₂ _ _ = b₁≼b₂
    foldl-Mono (x ∷ xs) (y ∷ ys) f b₁ b₂ (x≼y ∷ xs≼ys) b₁≼b₂ f-Mono₁ f-Mono₂ =
        foldl-Mono xs ys f (f b₁ x) (f b₂ y) xs≼ys (≼₂-trans (f-Mono₁ x b₁≼b₂) (f-Mono₂ b₂ x≼y)) f-Mono₁ f-Mono₂

module _ {a b} {A : Set a} {B : Set b}
         {_≈₂_ : B → B → Set b} {_⊔₂_ : B → B → B}
         (lB : IsSemilattice B _≈₂_ _⊔₂_) where

    open IsSemilattice lB using () renaming (_≼_ to _≼₂_; ⊔-idemp to ⊔₂-idemp; ≼-trans to ≼₂-trans)

    open import Data.List as List using (List; foldr; foldl; _∷_)
    open import Utils using (Pairwise; _∷_)

    foldr-Mono' : ∀ (l : List A) (f : A → B → B) →
                  (∀ a → Monotonic _≼₂_ _≼₂_ (f a)) →
                  Monotonic _≼₂_ _≼₂_ (λ b → foldr f b l)
    foldr-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
    foldr-Mono' (x ∷ xs) f f-Mono₂ b₁≼b₂ = f-Mono₂ x (foldr-Mono' xs f f-Mono₂ b₁≼b₂)

    foldl-Mono' : ∀ (l : List A) (f : B → A → B) →
                  (∀ b → Monotonic _≼₂_ _≼₂_ (λ a → f a b)) →
                  Monotonic _≼₂_ _≼₂_ (λ b → foldl f b l)
    foldl-Mono' List.[] f _ b₁≼b₂ = b₁≼b₂
    foldl-Mono' (x ∷ xs) f f-Mono₁ b₁≼b₂ = foldl-Mono' xs f f-Mono₁ (f-Mono₁ x b₁≼b₂)

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
        ; ⊔-Monotonicˡ to ⊓-Monotonicˡ
        ; ⊔-Monotonicʳ to ⊓-Monotonicʳ
        ; ≈-⊔-cong to ≈-⊓-cong
        ; _≼_ to _≽_
        ; _≺_ to _≻_
        ; ≼-refl to ≽-refl
        ; ≼-trans to ≽-trans
        )

    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

    private
        module MyChain = Chain _≈_ ≈-equiv _≺_ ≺-cong

    open MyChain.Height fixedHeight using (⊥; ⊤) public

    Known-⊥ : Set a
    Known-⊥ = ∀ (a : A) → ⊥ ≼ a

    Known-⊤ : Set a
    Known-⊤ = ∀ (a : A) → a ≼ ⊤

    -- If the equality is decidable, we can prove that the top and bottom
    -- elements of the chain are least and greatest elements of the lattice
    module _ {{≈-Decidable : IsDecidable _≈_}} where
        open IsDecidable ≈-Decidable using () renaming (R-dec to ≈-dec)

        open MyChain.Height fixedHeight using (bounded; longestChain)

        ⊥≼ : Known-⊥
        ⊥≼ a with ≈-dec a ⊥
        ...   | yes a≈⊥ = ≼-cong a≈⊥ ≈-refl (≼-refl a)
        ...   | no a̷≈⊥ with ≈-dec ⊥ (a ⊓ ⊥)
        ...         | yes ⊥≈a⊓⊥ = ≈-trans (⊔-comm ⊥ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥≈a⊓⊥) (absorb-⊔-⊓ a ⊥))
        ...         | no ⊥ᴬ̷≈a⊓⊥ = ⊥-elim (MyChain.Bounded-suc-n bounded (MyChain.step x≺⊥ ≈-refl longestChain))
                        where
                            ⊥⊓a̷≈⊥ : ¬ (⊥ ⊓ a) ≈ ⊥
                            ⊥⊓a̷≈⊥ = λ ⊥⊓a≈⊥ → ⊥ᴬ̷≈a⊓⊥ (≈-trans (≈-sym ⊥⊓a≈⊥) (⊓-comm _ _))

                            x≺⊥ : (⊥ ⊓ a) ≺ ⊥
                            x≺⊥ = (≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ ⊔ (⊥ ⊓ a)}) (absorb-⊔-⊓ ⊥ a)) , ⊥⊓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

record FiniteHeightLattice {a} (A : Set a) : Set (lsuc a) where
    field
        height : ℕ
        _≈_ : A → A → Set a
        _⊔_ : A → A → A
        _⊓_ : A → A → A

        {{isFiniteHeightLattice}} : IsFiniteHeightLattice A height _≈_ _⊔_ _⊓_

    open IsFiniteHeightLattice isFiniteHeightLattice public