open import Lattice

module Lattice.ExtendBelow {a} (A : Set a)
    {_≈₁_ : A → A → Set a} {_⊔₁_ : A → A → A} {_⊓₁_ : A → A → A}
    {{lA : IsLattice A _≈₁_ _⊔₁_ _⊓₁_}} where

open import Equivalence
open import Showable using (Showable; show)
open import Relation.Binary.Definitions using (Decidable)
open import Relation.Binary.PropositionalEquality using (refl)
open import Relation.Nullary using (Dec; ¬_; yes; no)

open IsLattice lA using ()
    renaming ( ≈-equiv to ≈₁-equiv
             ; ≈-⊔-cong to ≈₁-⊔₁-cong
             ; ⊔-assoc to ⊔₁-assoc; ⊔-comm to ⊔₁-comm; ⊔-idemp to ⊔₁-idemp
             ; ≈-⊓-cong to ≈₁-⊓₁-cong
             ; ⊓-assoc to ⊓₁-assoc; ⊓-comm to ⊓₁-comm; ⊓-idemp to ⊓₁-idemp
             ; absorb-⊔-⊓ to absorb-⊔₁-⊓₁; absorb-⊓-⊔ to absorb-⊓₁-⊔₁
             )

open IsEquivalence ≈₁-equiv using ()
    renaming (≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans)

data ExtendBelow : Set a where
    [_] : A → ExtendBelow
    ⊥ : ExtendBelow

instance
    showable : {{ showableA : Showable A }} → Showable ExtendBelow
    showable = record
        { show = (λ
            { ⊥ → "⊥"
            ; [ a ] → show a
            })
        }

data _≈_ : ExtendBelow → ExtendBelow → Set a where
    ≈-⊥-⊥ : ⊥ ≈ ⊥
    ≈-lift : ∀ {x y : A} → x ≈₁ y → [ x ] ≈ [ y ]

≈-refl : ∀ {ab : ExtendBelow} → ab ≈ ab
≈-refl {⊥} = ≈-⊥-⊥
≈-refl {[ x ]} = ≈-lift ≈₁-refl

≈-sym : ∀ {ab₁ ab₂ : ExtendBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₁
≈-sym ≈-⊥-⊥ = ≈-⊥-⊥
≈-sym (≈-lift x≈₁y) = ≈-lift (≈₁-sym x≈₁y)

≈-trans : ∀ {ab₁ ab₂ ab₃ : ExtendBelow} → ab₁ ≈ ab₂ → ab₂ ≈ ab₃ → ab₁ ≈ ab₃
≈-trans ≈-⊥-⊥ ≈-⊥-⊥ = ≈-⊥-⊥
≈-trans (≈-lift a₁≈a₂) (≈-lift a₂≈a₃) = ≈-lift (≈₁-trans a₁≈a₂ a₂≈a₃)

instance
    ≈-equiv : IsEquivalence ExtendBelow _≈_
    ≈-equiv = record
        { ≈-refl = ≈-refl
        ; ≈-sym = ≈-sym
        ; ≈-trans = ≈-trans
        }

_⊔_ : ExtendBelow → ExtendBelow → ExtendBelow
_⊔_ ⊥ x = x
_⊔_ [ a₁ ] ⊥ = [ a₁ ]
_⊔_ [ a₁ ] [ a₂ ] = [ a₁ ⊔₁ a₂ ]

_⊓_ : ExtendBelow → ExtendBelow → ExtendBelow
_⊓_ ⊥ x = ⊥
_⊓_ [ _ ] ⊥ = ⊥
_⊓_ [ a₁ ] [ a₂ ] = [ a₁ ⊓₁ a₂ ]

≈-⊔-cong : ∀ {x₁ x₂ x₃ x₄} → x₁ ≈ x₂ → x₃ ≈ x₄ →
           (x₁ ⊔ x₃) ≈ (x₂ ⊔ x₄)
≈-⊔-cong .{⊥} .{⊥} {x₃} {x₄} ≈-⊥-⊥ [a₃]≈[a₄] = [a₃]≈[a₄]
≈-⊔-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} .{⊥} .{⊥} [a₁]≈[a₂] ≈-⊥-⊥ = [a₁]≈[a₂]
≈-⊔-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} {x₃ = [ a₃ ]} {x₄ = [ a₄ ]} (≈-lift a₁≈a₂) (≈-lift a₃≈a₄) = ≈-lift (≈₁-⊔₁-cong a₁≈a₂ a₃≈a₄)

⊔-assoc : ∀ (x₁ x₂ x₃ : ExtendBelow) →  ((x₁ ⊔ x₂) ⊔ x₃) ≈ (x₁ ⊔ (x₂ ⊔ x₃))
⊔-assoc ⊥ x₁ x₂ = ≈-refl
⊔-assoc [ a₁ ] ⊥ x₂ = ≈-refl
⊔-assoc [ a₁ ] [ a₂ ] ⊥ = ≈-refl
⊔-assoc [ a₁ ] [ a₂ ] [ a₃ ] = ≈-lift (⊔₁-assoc a₁ a₂ a₃)

⊔-comm : ∀ (x₁ x₂ : ExtendBelow) →  (x₁ ⊔ x₂) ≈ (x₂ ⊔ x₁)
⊔-comm ⊥ ⊥ = ≈-refl
⊔-comm ⊥ [ a₂ ] = ≈-refl
⊔-comm [ a₁ ] ⊥ = ≈-refl
⊔-comm [ a₁ ] [ a₂ ] = ≈-lift (⊔₁-comm a₁ a₂)

⊔-idemp : ∀ (x : ExtendBelow) →  (x ⊔ x) ≈ x
⊔-idemp ⊥ = ≈-refl
⊔-idemp [ a ] = ≈-lift (⊔₁-idemp a)

≈-⊓-cong : ∀ {x₁ x₂ x₃ x₄} → x₁ ≈ x₂ → x₃ ≈ x₄ →
           (x₁ ⊓ x₃) ≈ (x₂ ⊓ x₄)
≈-⊓-cong .{⊥} .{⊥} {x₃} {x₄} ≈-⊥-⊥ [a₃]≈[a₄] = ≈-⊥-⊥
≈-⊓-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} .{⊥} .{⊥} [a₁]≈[a₂] ≈-⊥-⊥ = ≈-⊥-⊥
≈-⊓-cong {x₁ = [ a₁ ]} {x₂ = [ a₂ ]} {x₃ = [ a₃ ]} {x₄ = [ a₄ ]} (≈-lift a₁≈a₂) (≈-lift a₃≈a₄) = ≈-lift (≈₁-⊓₁-cong a₁≈a₂ a₃≈a₄)

⊓-assoc : ∀ (x₁ x₂ x₃ : ExtendBelow) →  ((x₁ ⊓ x₂) ⊓ x₃) ≈ (x₁ ⊓ (x₂ ⊓ x₃))
⊓-assoc ⊥ x₁ x₂ = ≈-refl
⊓-assoc [ a₁ ] ⊥ x₂ = ≈-refl
⊓-assoc [ a₁ ] [ a₂ ] ⊥ = ≈-refl
⊓-assoc [ a₁ ] [ a₂ ] [ a₃ ] = ≈-lift (⊓₁-assoc a₁ a₂ a₃)

⊓-comm : ∀ (x₁ x₂ : ExtendBelow) →  (x₁ ⊓ x₂) ≈ (x₂ ⊓ x₁)
⊓-comm ⊥ ⊥ = ≈-refl
⊓-comm ⊥ [ a₂ ] = ≈-refl
⊓-comm [ a₁ ] ⊥ = ≈-refl
⊓-comm [ a₁ ] [ a₂ ] = ≈-lift (⊓₁-comm a₁ a₂)

⊓-idemp : ∀ (x : ExtendBelow) →  (x ⊓ x) ≈ x
⊓-idemp ⊥ = ≈-refl
⊓-idemp [ a ] = ≈-lift (⊓₁-idemp a)

absorb-⊔-⊓ : (x₁ x₂ : ExtendBelow) → (x₁ ⊔ (x₁ ⊓ x₂)) ≈ x₁
absorb-⊔-⊓ ⊥ ⊥ = ≈-refl
absorb-⊔-⊓ ⊥ [ a₂ ] = ≈-refl
absorb-⊔-⊓ [ a₁ ] ⊥ = ≈-refl
absorb-⊔-⊓ [ a₁ ] [ a₂ ] = ≈-lift (absorb-⊔₁-⊓₁ a₁ a₂)

absorb-⊓-⊔ : (x₁ x₂ : ExtendBelow) → (x₁ ⊓ (x₁ ⊔ x₂)) ≈ x₁
absorb-⊓-⊔ ⊥ ⊥ = ≈-refl
absorb-⊓-⊔ ⊥ [ a₂ ] = ≈-refl
absorb-⊓-⊔ [ a₁ ] ⊥ = ⊓-idemp [ a₁ ]
absorb-⊓-⊔ [ a₁ ] [ a₂ ] = ≈-lift (absorb-⊓₁-⊔₁ a₁ a₂)

instance
    isJoinSemilattice : IsSemilattice ExtendBelow _≈_ _⊔_
    isJoinSemilattice = record
        { ≈-equiv = ≈-equiv
        ; ≈-⊔-cong = ≈-⊔-cong
        ; ⊔-assoc = ⊔-assoc
        ; ⊔-comm = ⊔-comm
        ; ⊔-idemp = ⊔-idemp
        }

    isMeetSemilattice : IsSemilattice ExtendBelow _≈_ _⊓_
    isMeetSemilattice = record
        { ≈-equiv = ≈-equiv
        ; ≈-⊔-cong = ≈-⊓-cong
        ; ⊔-assoc = ⊓-assoc
        ; ⊔-comm = ⊓-comm
        ; ⊔-idemp = ⊓-idemp
        }

    isLattice : IsLattice ExtendBelow _≈_ _⊔_ _⊓_
    isLattice = record
        { joinSemilattice = isJoinSemilattice
        ; meetSemilattice = isMeetSemilattice
        ; absorb-⊔-⊓ = absorb-⊔-⊓
        ; absorb-⊓-⊔ = absorb-⊓-⊔
        }

module _ {{≈₁-Decidable : IsDecidable _≈₁_}} where
    open IsDecidable ≈₁-Decidable using () renaming (R-dec to ≈₁-dec)

    ≈-dec : Decidable _≈_
    ≈-dec ⊥ ⊥ = yes ≈-⊥-⊥
    ≈-dec [ a₁ ] [ a₂ ]
        with ≈₁-dec a₁ a₂
    ...   | yes a₁≈a₂ = yes (≈-lift a₁≈a₂)
    ...   | no a₁̷≈a₂ = no (λ { (≈-lift a₁≈a₂) → a₁̷≈a₂ a₁≈a₂ })
    ≈-dec ⊥ [ _ ] = no (λ ())
    ≈-dec [ _ ] ⊥ = no (λ ())

    instance
        ≈-Decidable : IsDecidable _≈_
        ≈-Decidable = record { R-dec = ≈-dec }