agda-spa/Lattice.agda

module Lattice where

open import Equivalence
import Chain

import Data.Nat.Properties as NatProps
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym; subst)
open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎)
open import Relation.Binary.Definitions
open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Data.Nat as Nat using (ℕ; _≤_; _+_; suc)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
open import Function.Definitions using (Injective)
open import Data.Empty using (⊥)

absurd : ∀ {a} {A : Set a} →  ⊥ → A
absurd ()

record IsDecidable {a} {A : Set a} (R : A → A → Set a) : Set a where
    field
        R-dec : ∀ (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
        )

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 _≈_ _⊔_ _⊓_
        fixedHeight : Chain.Height (_≈_) (IsLattice.≈-equiv isLattice) (IsLattice._≺_ isLattice) (IsLattice.≺-cong isLattice) h

    open IsLattice isLattice public


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

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

        private
            ≡-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊔ a₃) ≡ (a₂ ⊔ a₄)
            ≡-⊔-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl

            ≡-⊓-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≡ a₂ → a₃ ≡ a₄ → (a₁ ⊓ a₃) ≡ (a₂ ⊓ a₄)
            ≡-⊓-cong a₁≡a₂ a₃≡a₄ rewrite a₁≡a₂ rewrite a₃≡a₄ = refl

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

        NatIsMinSemilattice : IsSemilattice ℕ _≡_ _⊓_
        NatIsMinSemilattice = record
            { ≈-equiv = record
                { ≈-refl = refl
                ; ≈-sym = sym
                ; ≈-trans = trans
                }
            ; ≈-⊔-cong = ≡-⊓-cong
            ; ⊔-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

        module ProdEquiv = IsEquivalenceInstances.ForProd _≈₁_ _≈₂_ (IsSemilattice.≈-equiv sA) (IsSemilattice.≈-equiv sB)
        open ProdEquiv using (_≈_) public

        infixl 20 _⊔_

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

        ProdIsSemilattice : IsSemilattice (A × B) _≈_ _⊔_
        ProdIsSemilattice = record
            { ≈-equiv = ProdEquiv.ProdEquivalence
            ; ≈-⊔-cong = λ (a₁≈a₂ , b₁≈b₂) (a₃≈a₄ , b₃≈b₄) →
                ( IsSemilattice.≈-⊔-cong sA a₁≈a₂ a₃≈a₄
                , IsSemilattice.≈-⊔-cong sB b₁≈b₂ b₃≈b₄
                )
            ; ⊔-assoc = λ (a₁ , b₁) (a₂ , b₂) (a₃ , b₃) →
                ( IsSemilattice.⊔-assoc sA a₁ a₂ a₃
                , IsSemilattice.⊔-assoc sB b₁ b₂ b₃
                )
            ; ⊔-comm = λ (a₁ , b₁) (a₂ , b₂) →
                ( IsSemilattice.⊔-comm sA a₁ a₂
                , IsSemilattice.⊔-comm sB b₁ b₂
                )
            ; ⊔-idemp = λ (a , b) →
                ( IsSemilattice.⊔-idemp sA a
                , IsSemilattice.⊔-idemp sB b
                )
            }

    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; ≈-⊔-cong to ≈₂-⊔₂-cong
            ; ⊔-assoc to ⊔₂-assoc; ⊔-comm to ⊔₂-comm; ⊔-idemp to ⊔₂-idemp
            )

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

        infixl 20 _⊔_
        infixl 20 _⊓_

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

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

        MapIsUnionSemilattice : IsSemilattice Map _≈_ _⊔_
        MapIsUnionSemilattice = record
            { ≈-equiv = MapEquiv.LiftEquivalence
            ; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} → union-cong _≈₂_ _⊔₂_ ≈₂-⊔₂-cong {m₁} {m₂} {m₃} {m₄}
            ; ⊔-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
            ; ≈-⊔-cong = λ {m₁} {m₂} {m₃} {m₄} → intersect-cong _≈₂_ _⊔₂_ ≈₂-⊔₂-cong {m₁} {m₂} {m₃} {m₄}
            ; ⊔-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

        module ProdJoin = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊔₂_ (IsLattice.joinSemilattice lA) (IsLattice.joinSemilattice lB)
        open ProdJoin using (_⊔_; _≈_) public

        module ProdMeet = IsSemilatticeInstances.ForProd _≈₁_ _≈₂_ _⊓₁_ _⊓₂_ (IsLattice.meetSemilattice lA) (IsLattice.meetSemilattice lB)
        open ProdMeet using () renaming (_⊔_ to _⊓_) public

        ProdIsLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
        ProdIsLattice = record
            { joinSemilattice = ProdJoin.ProdIsSemilattice
            ; meetSemilattice = ProdMeet.ProdIsSemilattice
            ; absorb-⊔-⊓ = λ (a₁ , b₁) (a₂ , b₂) →
                ( IsLattice.absorb-⊔-⊓ lA a₁ a₂
                , IsLattice.absorb-⊔-⊓ lB b₁ b₂
                )
            ; absorb-⊓-⊔ = λ (a₁ , b₁) (a₂ , b₂) →
                ( IsLattice.absorb-⊓-⊔ lA a₁ a₂
                , IsLattice.absorb-⊓-⊔ lB b₁ b₂
                )
            }

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

        open import Map A B ≡-dec-A
        open IsLattice lB renaming
            ( ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym
            ; ⊔-idemp to ⊔₂-idemp; ⊓-idemp to ⊓₂-idemp
            ; absorb-⊔-⊓ to absorb-⊔₂-⊓₂; absorb-⊓-⊔ to absorb-⊓₂-⊔₂
            )

        module MapJoin = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊔₂_ (IsLattice.joinSemilattice lB)
        open MapJoin using (_⊔_; _≈_) public

        module MapMeet = IsSemilatticeInstances.ForMap ≡-dec-A _≈₂_ _⊓₂_ (IsLattice.meetSemilattice lB)
        open MapMeet using (_⊓_) public

        MapIsLattice : IsLattice Map _≈_ _⊔_ _⊓_
        MapIsLattice = record
            { joinSemilattice = MapJoin.MapIsUnionSemilattice
            ; meetSemilattice = MapMeet.MapIsIntersectSemilattice
            ; absorb-⊔-⊓ = union-intersect-absorb _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ _⊓₂_ ⊔₂-idemp ⊓₂-idemp absorb-⊔₂-⊓₂ absorb-⊓₂-⊔₂
            ; absorb-⊓-⊔ = intersect-union-absorb _≈₂_ ≈₂-refl ≈₂-sym _⊔₂_ _⊓₂_ ⊔₂-idemp ⊓₂-idemp absorb-⊔₂-⊓₂ absorb-⊓₂-⊔₂
            }

module IsFiniteHeightLatticeInstances where
    module ForProd {a} {A B : Set a}
        (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set a)
        (decA : IsDecidable _≈₁_) (decB : IsDecidable _≈₂_)
        (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A)
        (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B)
        (h₁ h₂ : ℕ)
        (lA : IsFiniteHeightLattice A h₁ _≈₁_ _⊔₁_ _⊓₁_) (lB : IsFiniteHeightLattice B h₂ _≈₂_ _⊔₂_ _⊓₂_) where

        open NatProps
        module ProdLattice = IsLatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊓₁_ _⊔₂_ _⊓₂_ (IsFiniteHeightLattice.isLattice lA) (IsFiniteHeightLattice.isLattice lB)
        open ProdLattice using (_⊔_; _⊓_; _≈_) public
        open IsLattice ProdLattice.ProdIsLattice using (_≼_; _≺_; ≺-cong; ≈-equiv)
        open IsFiniteHeightLattice lA using () renaming (⊔-idemp to ⊔₁-idemp; _≼_ to _≼₁_; ≈-equiv to ≈₁-equiv; ≈-refl to ≈₁-refl; ≈-trans to ≈₁-trans; ≈-sym to ≈₁-sym; _≺_ to _≺₁_; ≺-cong to ≺₁-cong)
        open IsFiniteHeightLattice lB using () renaming (⊔-idemp to ⊔₂-idemp; _≼_ to _≼₂_; ≈-equiv to ≈₂-equiv; ≈-refl to ≈₂-refl; ≈-trans to ≈₂-trans; ≈-sym to ≈₂-sym; _≺_ to _≺₂_; ≺-cong to ≺₂-cong)
        open IsDecidable decA using () renaming (R-dec to ≈₁-dec)
        open IsDecidable decB using () renaming (R-dec to ≈₂-dec)

        module ChainMapping₁ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lA) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice)
        module ChainMapping₂ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lB) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice)

        module ChainA = Chain _≈₁_ ≈₁-equiv _≺₁_ ≺₁-cong
        module ChainB = Chain _≈₂_ ≈₂-equiv _≺₂_ ≺₂-cong
        module ProdChain = Chain _≈_ ≈-equiv _≺_ ≺-cong

        open ChainA using () renaming (Chain to Chain₁; done to done₁; step to step₁; Chain-≈-cong₁ to Chain₁-≈-cong₁)
        open ChainB using () renaming (Chain to Chain₂; done to done₂; step to step₂; Chain-≈-cong₁ to Chain₂-≈-cong₁)
        open ProdChain using (Chain; concat; done; step)

        private
            a,∙-Monotonic : ∀ (a : A) → Monotonic _≼₂_ _≼_ (λ b → (a , b))
            a,∙-Monotonic a {b₁} {b₂} (b , b₁⊔b≈b₂) = ((a , b) , (⊔₁-idemp a , b₁⊔b≈b₂))

            a,∙-Preserves-≈₂ : ∀ (a : A) → (λ b → (a , b)) Preserves _≈₂_ ⟶  _≈_
            a,∙-Preserves-≈₂ a {b₁} {b₂} b₁≈b₂ = (≈₁-refl , b₁≈b₂)

            ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b))
            ∙,b-Monotonic b {a₁} {a₂} (a , a₁⊔a≈a₂) = ((a , b) , (a₁⊔a≈a₂ , ⊔₂-idemp b))

            ∙,b-Preserves-≈₁ : ∀ (b : B) → (λ a → (a , b)) Preserves _≈₁_ ⟶  _≈_
            ∙,b-Preserves-≈₁ b {a₁} {a₂} a₁≈a₂ = (a₁≈a₂ , ≈₂-refl)

            amin : A
            amin = proj₁ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lA)))

            amax : A
            amax = proj₂ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lA)))

            bmin : B
            bmin = proj₁ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lB)))

            bmax : B
            bmax = proj₂ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lB)))

            unzip : ∀ {a₁ a₂ : A} {b₁ b₂ : B} {n : ℕ} → Chain (a₁ , b₁) (a₂ , b₂) n → Σ (ℕ × ℕ) (λ (n₁ , n₂) → ((Chain₁ a₁ a₂ n₁ × Chain₂ b₁ b₂ n₂) × (n ≤ n₁ + n₂)))
            unzip (done (a₁≈a₂ , b₁≈b₂)) = ((0 , 0) , ((done₁ a₁≈a₂ , done₂ b₁≈b₂) , ≤-refl))
            unzip {a₁} {a₂} {b₁} {b₂} {n} (step {(a₁ , b₁)} {(a , b)} (((d₁ , d₂) , (a₁⊔d₁≈a , b₁⊔d₂≈b)) , a₁b₁̷≈ab) (a≈a' , b≈b') a'b'a₂b₂)
                with ≈₁-dec a₁ a | ≈₂-dec b₁ b | unzip a'b'a₂b₂
            ...   | yes a₁≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) = absurd (a₁b₁̷≈ab (a₁≈a , b₁≈b))
            ...   | no a₁̷≈a  | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
                    ((suc n₁ , n₂) , ((step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , Chain₂-≈-cong₁ (≈₂-sym (≈₂-trans b₁≈b b≈b')) c₂), +-monoʳ-≤ 1 (n≤n₁+n₂)))
            ...   | yes a₁≈a | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
                    ((n₁ , suc n₂) , ( (Chain₁-≈-cong₁ (≈₁-sym (≈₁-trans a₁≈a a≈a')) c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂)
                                     , subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂)
                                     ))
            ...   | no a₁̷≈a  | no b₁̷≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
                    ((suc n₁ , suc n₂) , ( (step₁ ((d₁ , a₁⊔d₁≈a) , a₁̷≈a) a≈a' c₁ , step₂ ((d₂ , b₁⊔d₂≈b) , b₁̷≈b) b≈b' c₂)
                                         , ≤-stepsˡ 1 (subst (n ≤_) (sym (+-suc n₁ n₂)) (+-monoʳ-≤ 1 n≤n₁+n₂))
                                         ))

        ProdIsFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
        ProdIsFiniteHeightLattice = record
            { isLattice = ProdLattice.ProdIsLattice
            ; fixedHeight =
                ( ( ((amin , bmin) , (amax , bmax))
                  , concat
                      (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lA))))
                      (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lB))))
                  )
                , λ a₁b₁a₂b₂ → let ((n₁ , n₂) , ((a₁a₂ , b₁b₂) , n≤n₁+n₂)) = unzip a₁b₁a₂b₂
                               in ≤-trans n≤n₁+n₂ (+-mono-≤ (proj₂ (IsFiniteHeightLattice.fixedHeight lA) a₁a₂)
                                                            (proj₂ (IsFiniteHeightLattice.fixedHeight lB) b₁b₂))
                )
            }

module FixedHeightLatticeIsBounded {a} {A : Set a} {h : ℕ}
    {_≈_ : A → A → Set a}
    {_⊔_ : A → A → A} {_⊓_ : A → A → A}
    (decA : IsDecidable _≈_)
    (lA : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_) where

    open IsFiniteHeightLattice lA using (_≼_; _≺_; fixedHeight; ≈-equiv; ≈-refl; ≈-sym; ≈-trans; ≼-refl; ≼-cong; ≺-cong; ≈-⊔-cong; absorb-⊔-⊓; ⊔-comm; ⊓-comm)
    open IsDecidable decA using () renaming (R-dec to ≈-dec)
    open NatProps using (+-comm; m+1+n≰m)

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

    A-BoundedBelow : Σ A (λ ⊥ᴬ → ∀ (a : A) → ⊥ᴬ ≼ a)
    A-BoundedBelow = (⊥ᴬ , ⊥ᴬ≼)
        where
            ⊥ᴬ : A
            ⊥ᴬ = proj₁ (proj₁ (proj₁ fixedHeight))

            ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
            ⊥ᴬ≼ a
                with ≈-dec a ⊥ᴬ
            ...   | yes a≈⊥ᴬ = ≼-cong a≈⊥ᴬ ≈-refl (≼-refl a)
            ...   | no a̷≈⊥ᴬ with ≈-dec ⊥ᴬ (a ⊓ ⊥ᴬ)
            ...         | yes ⊥ᴬ≈a⊓⊥ᴬ = (a , ≈-trans (⊔-comm ⊥ᴬ a) (≈-trans (≈-⊔-cong (≈-refl {a}) ⊥ᴬ≈a⊓⊥ᴬ) (absorb-⊔-⊓ a ⊥ᴬ)))
            ...         | no ⊥ᴬ̷≈a⊓⊥ᴬ = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) (ChainA.step x≺⊥ᴬ ≈-refl (proj₂ (proj₁ fixedHeight))))
                            where
                                ⊥ᴬ⊓a̷≈⊥ᴬ : ¬ (⊥ᴬ ⊓ a) ≈ ⊥ᴬ
                                ⊥ᴬ⊓a̷≈⊥ᴬ = λ ⊥ᴬ⊓a≈⊥ᴬ → ⊥ᴬ̷≈a⊓⊥ᴬ (≈-trans (≈-sym ⊥ᴬ⊓a≈⊥ᴬ) (⊓-comm _ _))

                                x≺⊥ᴬ : (⊥ᴬ ⊓ a) ≺ ⊥ᴬ
                                x≺⊥ᴬ = ((⊥ᴬ , ≈-trans (⊔-comm _ _) (≈-trans (≈-refl {⊥ᴬ ⊔ (⊥ᴬ ⊓ a)}) (absorb-⊔-⊓ ⊥ᴬ a))) , ⊥ᴬ⊓a̷≈⊥ᴬ)

module FixedPoint {a} {A : Set a}
                  (h : ℕ)
                  (_≈_ : A → A → Set a) (decA : IsDecidable _≈_)
                  (_⊔_ : A → A → A) (_⊓_ : A → A → A)
                  (isFiniteHeightLattice : IsFiniteHeightLattice A h _≈_ _⊔_ _⊓_)
                  (f : A → A) (Monotonicᶠ : Monotonic (IsFiniteHeightLattice._≼_ isFiniteHeightLattice)
                                                      (IsFiniteHeightLattice._≼_ isFiniteHeightLattice) f) where
    open IsDecidable decA using () renaming (R-dec to ≈-dec)
    open IsFiniteHeightLattice isFiniteHeightLattice
    open FixedHeightLatticeIsBounded decA isFiniteHeightLattice
    open NatProps using (+-suc; +-comm)
    module ChainA = Chain _≈_ ≈-equiv _≺_ ≺-cong

    private
        ⊥ᴬ : A
        ⊥ᴬ = proj₁ A-BoundedBelow

        ⊥ᴬ≼ : ∀ (a : A) → ⊥ᴬ ≼ a
        ⊥ᴬ≼ = proj₂ A-BoundedBelow

        -- using 'g', for gas, here helps make sure the function terminates.
        -- since A forms a fixed-height lattice, we must find a solution after
        -- 'h' steps at most. Gas is set up such that as soon as it runs
        -- out, we have exceeded h steps, which shouldn't be possible.

        doStep : ∀ (g hᶜ : ℕ) (a₁ a₂ : A) (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h) (a₂≼fa₂ : a₂ ≼ f a₂) → Σ A (λ a → a ≈ f a)
        doStep 0 hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
        doStep (suc g') hᶜ a₁ a₂ c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
            with ≈-dec a₂ (f a₂)
        ...   | yes a₂≈fa₂ = (a₂ , a₂≈fa₂)
        ...   | no  a₂̷≈fa₂ = doStep g' (suc hᶜ) a₁ (f a₂) c' g+hᶜ≡sh (Monotonicᶠ a₂≼fa₂)
                    where
                        a₂≺fa₂ : a₂ ≺ f a₂
                        a₂≺fa₂ = (a₂≼fa₂ , a₂̷≈fa₂)

                        c' : ChainA.Chain a₁ (f a₂) (suc hᶜ)
                        c' rewrite +-comm 1 hᶜ = ChainA.concat c (ChainA.step a₂≺fa₂ ≈-refl (ChainA.done (≈-refl {f a₂})))

        fix : Σ A (λ a → a ≈ f a)
        fix = doStep (suc h) 0 ⊥ᴬ ⊥ᴬ (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))

    aᶠ : A
    aᶠ = proj₁ fix

    aᶠ≈faᶠ : aᶠ ≈ f aᶠ
    aᶠ≈faᶠ = proj₂ fix

    private
        stepPreservesLess : ∀ (g hᶜ : ℕ) (a₁ a₂ a : A) (a≈fa : a ≈ f a) (a₂≼a : a₂ ≼ a)
                         (c : ChainA.Chain a₁ a₂ hᶜ) (g+hᶜ≡h : g + hᶜ ≡ suc h)
                         (a₂≼fa₂ : a₂ ≼ f a₂) →
                         proj₁ (doStep g hᶜ a₁ a₂ c g+hᶜ≡h a₂≼fa₂) ≼ a
        stepPreservesLess 0 _ _ _ _ _ _ c g+hᶜ≡sh _ rewrite g+hᶜ≡sh = absurd (ChainA.Bounded-suc-n (proj₂ fixedHeight) c)
        stepPreservesLess (suc g') hᶜ a₁ a₂ a a≈fa a₂≼a c g+hᶜ≡sh a₂≼fa₂ rewrite sym (+-suc g' hᶜ)
            with ≈-dec a₂ (f a₂)
        ...   | yes _ = a₂≼a
        ...   | no  _ = stepPreservesLess g' _ _ _ a a≈fa (≼-cong ≈-refl (≈-sym a≈fa) (Monotonicᶠ a₂≼a)) _ _ _

    aᶠ≼ : ∀ (a : A) → a ≈ f a → aᶠ ≼ a
    aᶠ≼ a a≈fa = stepPreservesLess (suc h) 0 ⊥ᴬ ⊥ᴬ a a≈fa (⊥ᴬ≼ a) (ChainA.done ≈-refl) (+-comm (suc h) 0) (⊥ᴬ≼ (f ⊥ᴬ))