Prove that AxB is a finite height semilattice

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2023-09-03 23:56:39 -07:00
parent fb86d3f84f
commit 5cab39ca82
2 changed files with 44 additions and 9 deletions

View File

@ -16,7 +16,7 @@ module _ where
data Chain : A A Set a where data Chain : A A Set a where
done : {a a' : A} a a' Chain a a' 0 done : {a a' : A} a a' Chain a a' 0
step : {a₁ a₂ a₂' a₃ : A} {n : } a₁ R a₂ a₂ a₂' Chain a₂ a₃ n Chain a₁ a₃ (suc n) step : {a₁ a₂ a₂' a₃ : A} {n : } a₁ R a₂ a₂ a₂' Chain a₂' a₃ n Chain a₁ a₃ (suc n)
Chain-≈-cong₁ : {a₁ a₁' a₂} {n : } a₁ a₁' Chain a₁ a₂ n Chain a₁' a₂ n Chain-≈-cong₁ : {a₁ a₁' a₂} {n : } a₁ a₁' Chain a₁ a₂ n Chain a₁' a₂ n
Chain-≈-cong₁ a₁≈a₁' (done a₁≈a₂) = done (≈-trans (≈-sym a₁≈a₁') a₁≈a₂) Chain-≈-cong₁ a₁≈a₁' (done a₁≈a₂) = done (≈-trans (≈-sym a₁≈a₁') a₁≈a₂)

View File

@ -4,17 +4,22 @@ open import Equivalence
import Chain import Chain
import Data.Nat.Properties as NatProps import Data.Nat.Properties as NatProps
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym) 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.Definitions
open import Relation.Binary.Core using (_Preserves_⟶_ ) open import Relation.Binary.Core using (_Preserves_⟶_ )
open import Relation.Nullary using (Dec; ¬_) open import Relation.Nullary using (Dec; ¬_; yes; no)
open import Data.Nat as Nat using (; _≤_; _+_) open import Data.Nat as Nat using (; _≤_; _+_; suc)
open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂) open import Data.Product using (_×_; Σ; _,_; proj₁; proj₂)
open import Data.Sum using (_⊎_; inj₁; inj₂) open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔_) open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔_)
open import Function.Definitions using (Injective) open import Function.Definitions using (Injective)
open import Data.Empty using ()
record IsDecidable {a} (A : Set a) (R : A A Set a) : Set a where absurd : {a} {A : Set a} A
absurd ()
record IsDecidable {a} {A : Set a} (R : A A Set a) : Set a where
field field
R-dec : (a₁ a₂ : A) Dec (R a₁ a₂) R-dec : (a₁ a₂ : A) Dec (R a₁ a₂)
@ -356,20 +361,32 @@ module IsLatticeInstances where
module IsFiniteHeightLatticeInstances where module IsFiniteHeightLatticeInstances where
module ForProd {a} {A B : Set a} module ForProd {a} {A B : Set a}
(_≈₁_ : A A Set a) (_≈₂_ : B B Set a) (_≈₁_ : A A Set a) (_≈₂_ : B B Set a)
(decA : IsDecidable _≈₁_) (decB : IsDecidable _≈₂_)
(_⊔₁_ : A A A) (_⊓₁_ : A A A) (_⊔₁_ : A A A) (_⊓₁_ : A A A)
(_⊔₂_ : B B B) (_⊓₂_ : B B B) (_⊔₂_ : B B B) (_⊓₂_ : B B B)
(h₁ h₂ : ) (h₁ h₂ : )
(lA : IsFiniteHeightLattice A h₁ _≈₁_ _⊔₁_ _⊓₁_) (lB : IsFiniteHeightLattice B h₂ _≈₂_ _⊔₂_ _⊓₂_) where (lA : IsFiniteHeightLattice A h₁ _≈₁_ _⊔₁_ _⊓₁_) (lB : IsFiniteHeightLattice B h₂ _≈₂_ _⊔₂_ _⊓₂_) where
open NatProps
module ProdLattice = IsLatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊓₁_ _⊔₂_ _⊓₂_ (IsFiniteHeightLattice.isLattice lA) (IsFiniteHeightLattice.isLattice lB) module ProdLattice = IsLatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊓₁_ _⊔₂_ _⊓₂_ (IsFiniteHeightLattice.isLattice lA) (IsFiniteHeightLattice.isLattice lB)
open ProdLattice using (_⊔_; _⊓_; _≈_) public open ProdLattice using (_⊔_; _⊓_; _≈_) public
open IsLattice ProdLattice.ProdIsLattice using (_≼_; _≺_; ≺-cong; ≈-equiv) open IsLattice ProdLattice.ProdIsLattice using (_≼_; _≺_; ≺-cong; ≈-equiv)
open IsFiniteHeightLattice lA using () renaming (⊔-idemp to ⊔₁-idemp; _≼_ to _≼₁_; ≈-refl to ≈₁-refl) 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 _≼₂_; ≈-refl to ≈₂-refl) 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 lA) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice)
module ChainMapping = ChainMapping (IsFiniteHeightLattice.joinSemilattice lB) (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 private
a,∙-Monotonic : (a : A) Monotonic _≼₂_ _≼_ (λ b (a , b)) 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,∙-Monotonic a {b₁} {b₂} (b , b₁⊔b≈b₂) = ((a , b) , (⊔₁-idemp a , b₁⊔b≈b₂))
@ -395,15 +412,33 @@ module IsFiniteHeightLatticeInstances where
bmax : B bmax : B
bmax = proj₂ (proj₁ (proj₁ (IsFiniteHeightLattice.fixedHeight lB))) 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 : IsFiniteHeightLattice (A × B) (h₁ + h₂) _≈_ _⊔_ _⊓_
ProdIsFiniteHeightLattice = record ProdIsFiniteHeightLattice = record
{ isLattice = ProdLattice.ProdIsLattice { isLattice = ProdLattice.ProdIsLattice
; fixedHeight = ; fixedHeight =
( ( ((amin , bmin) , (amax , bmax)) ( ( ((amin , bmin) , (amax , bmax))
, Chain.concat _≈_ ≈-equiv _≺_ ≺-cong , concat
(ChainMapping₁.Chain-map (λ a (a , bmin)) (∙,b-Monotonic _) proj₁ (∙,b-Preserves-≈₁ _) (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lA)))) (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)))) (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₂))
) )
} }