From 65d15903584be3659e9728eb9301982313bfc594 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 1 Mar 2024 23:26:25 -0800 Subject: [PATCH] Prove monotonicity of lub in one argument Signed-off-by: Danila Fedorin --- Lattice.agda | 32 ++++++++++++++++++++++++++------ 1 file changed, 26 insertions(+), 6 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index 54d6dbc..ce29ab8 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -14,6 +14,12 @@ open import Function.Definitions using (Injective) IsDecidable : ∀ {a} {A : Set a} (R : A → A → Set a) → Set a IsDecidable {a} {A} R = ∀ (a₁ a₂ : A) → Dec (R a₁ a₂) +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₂ + record IsSemilattice {a} (A : Set a) (_≈_ : A → A → Set a) (_⊔_ : A → A → A) : Set a where @@ -36,6 +42,26 @@ record IsSemilattice {a} (A : Set a) open import Relation.Binary.Reasoning.Base.Single _≈_ ≈-refl ≈-trans + ⊔-Monotonicˡ : ∀ (a₁ : A) → Monotonic _≼_ _≼_ (λ a₂ → a₁ ⊔ a₂) + ⊔-Monotonicˡ a {a₁} {a₂} a₁≼a₂ = ≈-trans (≈-sym lhs) (≈-⊔-cong (≈-refl {a}) a₁≼a₂) + where + lhs = + begin + a ⊔ (a₁ ⊔ a₂) + ∼⟨ ≈-⊔-cong (≈-sym (⊔-idemp _)) ≈-refl ⟩ + (a ⊔ a) ⊔ (a₁ ⊔ a₂) + ∼⟨ ⊔-assoc _ _ _ ⟩ + a ⊔ (a ⊔ (a₁ ⊔ a₂)) + ∼⟨ ≈-⊔-cong ≈-refl (≈-sym (⊔-assoc _ _ _)) ⟩ + a ⊔ ((a ⊔ a₁) ⊔ a₂) + ∼⟨ ≈-⊔-cong ≈-refl (≈-⊔-cong (⊔-comm _ _) ≈-refl) ⟩ + a ⊔ ((a₁ ⊔ a) ⊔ a₂) + ∼⟨ ≈-⊔-cong ≈-refl (⊔-assoc _ _ _) ⟩ + a ⊔ (a₁ ⊔ (a ⊔ a₂)) + ∼⟨ ≈-sym (⊔-assoc _ _ _) ⟩ + (a ⊔ a₁) ⊔ (a ⊔ a₂) + ∎ + ≼-refl : ∀ (a : A) → a ≼ a ≼-refl a = ⊔-idemp a @@ -97,12 +123,6 @@ record IsFiniteHeightLattice {a} (A : Set a) field fixedHeight : FixedHeight h -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}