From 67e96b27cff3c08392fb500fe79bc9c29f182699 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 3 Sep 2023 19:33:04 -0700 Subject: [PATCH] Add congruence instances for < and <= on semilattices Signed-off-by: Danila Fedorin --- Lattice.agda | 20 +++++++++++++++----- 1 file changed, 15 insertions(+), 5 deletions(-) diff --git a/Lattice.agda b/Lattice.agda index 22769dc..4f722ce 100644 --- a/Lattice.agda +++ b/Lattice.agda @@ -1,7 +1,7 @@ module Lattice where -open import Chain using (Chain; Height; done; step; concat) open import Equivalence +open import Chain import Data.Nat.Properties as NatProps open import Relation.Binary.PropositionalEquality as Eq using (_≡_; sym) @@ -35,10 +35,19 @@ record IsSemilattice {a} (A : Set a) ⊔-comm : (x y : A) → (x ⊔ y) ≈ (y ⊔ x) ⊔-idemp : (x : A) → (x ⊔ x) ≈ x + open IsEquivalence ≈-equiv public + ≼-refl : ∀ (a : A) → a ≼ a ≼-refl a = (a , ⊔-idemp a) - open IsEquivalence ≈-equiv public + ≼-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄ + ≼-cong a₁≈a₂ a₃≈a₄ (c₁ , a₁⊔c₁≈a₃) = (c₁ , ≈-trans (≈-⊔-cong (≈-sym a₁≈a₂) ≈-refl) (≈-trans a₁⊔c₁≈a₃ a₃≈a₄)) + + ≺-cong : ∀ {a₁ a₂ a₃ a₄ : A} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≺ a₃ → a₂ ≺ a₄ + ≺-cong a₁≈a₂ a₃≈a₄ (a₁≼a₃ , a₁̷≈a₃) = + ( ≼-cong a₁≈a₂ a₃≈a₄ a₁≼a₃ + , λ a₂≈a₄ → a₁̷≈a₃ (≈-trans a₁≈a₂ (≈-trans a₂≈a₄ (≈-sym a₃≈a₄))) + ) record IsLattice {a} (A : Set a) (_≈_ : A → A → Set a) @@ -71,10 +80,11 @@ record IsFiniteHeightLattice {a} (A : Set a) field isLattice : IsLattice A _≈_ _⊔_ _⊓_ - fixedHeight : Height (IsLattice._≺_ isLattice) h + fixedHeight : Chain.Height (IsLattice._≺_ isLattice) h open IsLattice isLattice public + module _ {a b} {A : Set a} {B : Set b} (_≼₁_ : A → A → Set a) (_≼₂_ : B → B → Set b) where @@ -86,8 +96,8 @@ module ChainMapping {a b} {A : Set a} {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 _≺₂_) + open IsSemilattice slA renaming (_≼_ to _≼₁_; _≺_ to _≺₁_; ≈-equiv to ≈₁-equiv) + open IsSemilattice slB renaming (_≼_ to _≼₂_; _≺_ to _≺₂_; ≈-equiv to ≈₂-equiv) Chain-map : ∀ (f : A → B) → Monotonic _≼₁_ _≼₂_ f → Injective _≈₁_ _≈₂_ f → ∀ {a₁ a₂ : A} {n : ℕ} → Chain _≺₁_ a₁ a₂ n → Chain _≺₂_ (f a₁) (f a₂) n