From b6292bf9bd22a6d5ea6040b03fff5b1bb6e23e04 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 20 Aug 2023 21:53:27 -0700 Subject: [PATCH] Prove that a lattice of height h1+h2 exists for products Signed-off-by: Danila Fedorin --- Lattice.agda | 76 +++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 67 insertions(+), 9 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index bf3eb90..229caed 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -4,11 +4,11 @@ import Data.Nat.Properties as NatProps open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym) open import Relation.Binary.Definitions open import Relation.Nullary using (Dec; ¬_) -open import Data.Nat as Nat using (ℕ; _≤_) -open import Data.Product using (_×_; Σ; _,_) +open import Data.Nat as Nat using (ℕ; _≤_; _+_) +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 Chain using (Chain; Height; done; step) +open import Chain using (Chain; Height; done; step; concat) open import Function.Definitions using (Injective) record IsEquivalence {a} (A : Set a) (_≈_ : A → A → Set a) : Set a where @@ -38,6 +38,9 @@ record IsSemilattice {a} (A : Set a) ⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x) ⊔-idemp : (x : A) → (x ⊔ x) ≈ x + ≼-refl : ∀ (a : A) → a ≼ a + ≼-refl a = (a , ⊔-idemp a) + open IsEquivalence ≈-equiv public record IsLattice {a} (A : Set a) @@ -57,6 +60,9 @@ record IsLattice {a} (A : Set a) ( ⊔-assoc to ⊓-assoc ; ⊔-comm to ⊓-comm ; ⊔-idemp to ⊓-idemp + ; _≼_ to _≽_ + ; _≺_ to _≻_ + ; ≼-refl to ≽-refl ) record IsFiniteHeightLattice {a} (A : Set a) @@ -72,17 +78,20 @@ record IsFiniteHeightLattice {a} (A : Set a) open IsLattice isLattice public module _ {a b} {A : Set a} {B : Set b} - (_≈₁_ : A → A → Set a) (_≈₂_ : B → B → Set b) - (_⊔₁_ : A → A → A) (_⊔₂_ : B → B → 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 _≺₁_) open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_) - Monotonic : (A → B) → Set (a ⊔ℓ b) - Monotonic f = ∀ {a₁ a₂ : A} → a₁ ≼₁ a₂ → f a₁ ≼₂ f a₂ - - Chain-map : ∀ (f : A → B) → Monotonic f → Injective _≈₁_ _≈₂_ f → + Chain-map : ∀ (f : A → B) → Monotonic _≼₁_ _≼₂_ f → Injective _≈₁_ _≈₂_ f → ∀ {a₁ a₂ : A} {n : ℕ} → Chain _≺₁_ a₁ a₂ n → Chain _≺₂_ (f a₁) (f a₂) n Chain-map f Monotonicᶠ Injectiveᶠ done = done Chain-map f Monotonicᶠ Injectiveᶠ (step (a₁≼₁a , a₁̷≈₁a) aa₂) = @@ -378,3 +387,52 @@ module IsLatticeInstances where ; 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) + (_⊔₁_ : A → A → A) (_⊓₁_ : A → A → A) + (_⊔₂_ : B → B → B) (_⊓₂_ : B → B → B) + (h₁ h₂ : ℕ) + (lA : IsFiniteHeightLattice A h₁ _≈₁_ _⊔₁_ _⊓₁_) (lB : IsFiniteHeightLattice B h₂ _≈₂_ _⊔₂_ _⊓₂_) where + + module ProdLattice = IsLatticeInstances.ForProd _≈₁_ _≈₂_ _⊔₁_ _⊓₁_ _⊔₂_ _⊓₂_ (IsFiniteHeightLattice.isLattice lA) (IsFiniteHeightLattice.isLattice lB) + open ProdLattice using (_⊔_; _⊓_; _≈_) public + open IsLattice ProdLattice.ProdIsLattice using (_≼_; _≺_) + open IsFiniteHeightLattice lA using () renaming (⊔-idemp to ⊔₁-idemp; _≼_ to _≼₁_) + open IsFiniteHeightLattice lB using () renaming (⊔-idemp to ⊔₂-idemp; _≼_ to _≼₂_) + + module ChainMapping₁ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lA) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice) + module ChainMapping₂ = ChainMapping (IsFiniteHeightLattice.joinSemilattice lB) (IsLattice.joinSemilattice ProdLattice.ProdIsLattice) + + 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₂)) + + ∙,b-Monotonic : ∀ (b : B) → Monotonic _≼₁_ _≼_ (λ a → (a , b)) + ∙,b-Monotonic b {a₁} {a₂} (a , a₁⊔a≈a₂) = ((a , b) , (a₁⊔a≈a₂ , ⊔₂-idemp b)) + + 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))) + + 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₁ (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lA)))) + (ChainMapping₂.Chain-map (λ b → (amax , b)) (a,∙-Monotonic _) proj₂ (proj₂ (proj₁ (IsFiniteHeightLattice.fixedHeight lB)))) + ) + , _ + ) + }