agda-spa/Lattice/Prod.agda
Danila Fedorin 0ba4b46e16 Add proof of decidable equivalence for products
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2024-02-11 15:35:50 -08:00

179 lines
9.0 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

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 Data.Empty using (⊥-elim)
open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Relation.Binary.PropositionalEquality using (sym; subst)
open import Relation.Nullary using (¬_; yes; no)
open import Equivalence
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 _≈₂_) where
≈-dec : IsDecidable _≈_
≈-dec (a₁ , b₁) (a₂ , b₂)
with ≈₁-dec a₁ a₂ | ≈₂-dec b₁ b₂
... | yes a₁≈a₂ | yes b₁≈b₂ = yes (a₁≈a₂ , b₁≈b₂)
... | no a₁̷≈a₂ | _ = no (λ (a₁≈a₂ , _) a₁̷≈a₂ a₁≈a₂)
... | _ | no b₁̷≈b₂ = no (λ (_ , b₁≈b₂) b₁̷≈b₂ 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₂ = (⊔₁-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₂≈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)} ((a₁≼a , b₁≼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₂)) = ⊥-elim (a₁b₁̷≈ab (a₁≈a , b₁≈b))
... | no a₁̷≈a | yes b₁≈b | ((n₁ , n₂) , ((c₁ , c₂) , n≤n₁+n₂)) =
((suc n₁ , n₂) , ((step₁ (a₁≼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₂ (b₁≼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₁ (a₁≼a , a₁̷≈a) a≈a' c₁ , step₂ (b₁≼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₂))
)
}