open import Lattice

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

open import Data.Nat using (ℕ; _≤_; _+_; suc)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Equivalence
open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Relation.Binary.Definitions
open import Relation.Binary.PropositionalEquality using (sym; subst)
open import Relation.Nullary using (¬_; yes; no)
import Chain

open IsLattice lA using () renaming
    ( ≈-equiv to ≈₁-equiv; ≈-refl to ≈₁-refl; ≈-sym to ≈₁-sym; ≈-trans to ≈₁-trans
    ; joinSemilattice to joinSemilattice₁
    ; meetSemilattice to meetSemilattice₁
    ; FixedHeight to FixedHeight₁
    ; ⊔-idemp to ⊔₁-idemp
    ; _≼_ to _≼₁_;  _≺_ to _≺₁_
    ; ≺-cong to ≺₁-cong
    )

open IsLattice lB using () renaming
    ( ≈-equiv to ≈₂-equiv; ≈-refl to ≈₂-refl; ≈-sym to ≈₂-sym; ≈-trans to ≈₂-trans
    ; joinSemilattice to joinSemilattice₂
    ; meetSemilattice to meetSemilattice₂
    ; FixedHeight to FixedHeight₂
    ; ⊔-idemp to ⊔₂-idemp
    ; _≼_ to _≼₂_;  _≺_ to _≺₂_
    ; ≺-cong to ≺₂-cong
    )

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

≈-equiv : IsEquivalence (A × B) _≈_
≈-equiv = record
    { ≈-refl = λ {p} → (≈₁-refl , ≈₂-refl)
    ; ≈-sym = λ {p₁} {p₂} (a₁≈a₂ , b₁≈b₂) → (≈₁-sym a₁≈a₂ , ≈₂-sym b₁≈b₂)
    ; ≈-trans = λ {p₁} {p₂} {p₃} (a₁≈a₂ , b₁≈b₂) (a₂≈a₃ , b₂≈b₃) →
        ( ≈₁-trans a₁≈a₂ a₂≈a₃ , ≈₂-trans b₁≈b₂ 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₂)

private module ProdIsSemilattice (f₁ : A → A → A) (f₂ : B → B → B) (sA : IsSemilattice A _≈₁_ f₁) (sB : IsSemilattice B _≈₂_ f₂) where
    isSemilattice : IsSemilattice (A × B) _≈_ (λ (a₁ , b₁) (a₂ , b₂) → (f₁ a₁ a₂ , f₂ b₁ b₂))
    isSemilattice = record
        { ≈-equiv = ≈-equiv
        ; ≈-⊔-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
            )
        }

isJoinSemilattice : IsSemilattice (A × B) _≈_ _⊔_
isJoinSemilattice = ProdIsSemilattice.isSemilattice _⊔₁_ _⊔₂_ joinSemilattice₁ joinSemilattice₂

isMeetSemilattice : IsSemilattice (A × B) _≈_ _⊓_
isMeetSemilattice = ProdIsSemilattice.isSemilattice _⊓₁_ _⊓₂_ meetSemilattice₁ meetSemilattice₂

isLattice : IsLattice (A × B) _≈_ _⊔_ _⊓_
isLattice = record
    { joinSemilattice = isJoinSemilattice
    ; meetSemilattice = isMeetSemilattice
    ; 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 _ (≈₁-dec : IsDecidable _≈₁_) (≈₂-dec : IsDecidable _≈₂_)
         (h₁ h₂ : ℕ)
         (fhA : FixedHeight₁ h₁) (fhB : FixedHeight₂ h₂) where

    open import Data.Nat.Properties
    open IsLattice isLattice using (_≼_; _≺_; ≺-cong)

    module ChainMapping₁ = ChainMapping joinSemilattice₁ isJoinSemilattice
    module ChainMapping₂ = ChainMapping joinSemilattice₂ isJoinSemilattice

    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₁ fhA))

        amax : A
        amax = proj₂ (proj₁ (proj₁ fhA))

        bmin : B
        bmin = proj₁ (proj₁ (proj₁ fhB))

        bmax : B
        bmax = proj₂ (proj₁ (proj₁ fhB))

        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₂))
                                     ))

    isFiniteHeightLattice : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
    isFiniteHeightLattice = record
        { isLattice = isLattice
        ; fixedHeight =
            ( ( ((amin , bmin) , (amax , bmax))
              , concat
                  (ChainMapping₁.Chain-map (λ a → (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ fhA)))
                  (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (a,∙-Preserves-≈₂ _) (proj₂ (proj₁ fhB)))
              )
            , λ 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₂ fhA a₁a₂) (proj₂ fhB b₁b₂))
            )
        }