From c48bd0272e22c8d360b128713dfd3e7080f3f3f9 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 5 Jul 2025 14:53:00 -0700 Subject: [PATCH] Define "less than or equal" for partial lattices and prove some properties Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 78 +++++++++++++++++++++++++++++++++++--------- 1 file changed, 63 insertions(+), 15 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index a503a41..7bcebc8 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -2,26 +2,23 @@ module Lattice.Builder where open import Lattice open import Equivalence -open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_) +open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe) open import Data.Unit using (⊤; tt) open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_) open import Data.List using (List; _∷_; []) open import Data.Sum using (_⊎_; inj₁; inj₂) -open import Data.Product using (Σ) +open import Data.Product using (Σ; _,_) +open import Data.Empty using (⊥; ⊥-elim) open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst) open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_) +maybe-injection : ∀ {a} {A : Set a} (x : A) → just x ≡ nothing → ⊥ +maybe-injection x () + data lift-≈ {a} {A : Set a} (_≈_ : A → A → Set a) : Maybe A → Maybe A → Set a where ≈-just : ∀ {a₁ a₂ : A} → a₁ ≈ a₂ → lift-≈ _≈_ (just a₁) (just a₂) ≈-nothing : lift-≈ _≈_ nothing nothing --- lift-≈-to-≈' : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_≈'_ : A → A → Set a) → --- (∀ x y → (x ≈ y) ≡ (x ≈' y)) → --- ∀ m₁ m₂ → lift-≈ _≈_ m₁ m₂ → lift-≈ _≈'_ m₁ m₂ --- lift-≈-to-≈' _≈_ _≈'_ ≈≡≈' (just x₁) (just x₂) (≈-just x₁≈x₂) --- rewrite ≈≡≈' x₁ x₂ = ≈-just x₁≈x₂ --- lift-≈-to-≈' _≈_ _≈'_ ≈≡≈' m₁ m₂ ≈-nothing = ≈-nothing - lift-≈-map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (_≈ᵃ_ : A → A → Set a) (_≈ᵇ_ : B → B → Set b) → (∀ a₁ a₂ → a₁ ≈ᵃ a₂ → f a₁ ≈ᵇ f a₂) → @@ -54,6 +51,12 @@ PartialComm {a} {A} _≈_ _⊗_ = ∀ (x y : A) → lift-≈ _≈_ (x ⊗ y) (y PartialIdemp : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a PartialIdemp {a} {A} _≈_ _⊗_ = ∀ (x : A) → lift-≈ _≈_ (x ⊗ x) (just x) +data Trivial a : Set a where + instance + mkTrivial : Trivial a + +data Empty a : Set a where + record IsPartialSemilattice {a} {A : Set a} (_≈_ : A → A → Set a) (_⊔?_ : A → A → Maybe A) : Set a where @@ -61,6 +64,9 @@ record IsPartialSemilattice {a} {A : Set a} _≈?_ : Maybe A → Maybe A → Set a _≈?_ = lift-≈ _≈_ + _≼_ : A → A → Set a + _≼_ x y = (x ⊔? y) ≈? (just y) + field ≈-equiv : IsEquivalence A _≈_ ≈-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → (a₁ ⊔? a₃) ≈? (a₂ ⊔? a₄) @@ -69,18 +75,60 @@ record IsPartialSemilattice {a} {A : Set a} ⊔-comm : PartialComm _≈_ _⊔?_ ⊔-idemp : PartialIdemp _≈_ _⊔?_ + open IsEquivalence ≈-equiv public + open IsEquivalence (lift-≈-Equivalence {{≈-equiv}}) public using () + renaming (≈-trans to ≈?-trans; ≈-sym to ≈?-sym; ≈-refl to ≈?-refl) + + ≈-≼-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄ + ≈-≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁≼a₃ + with a₁ ⊔? a₃ | a₂ ⊔? a₄ | ≈-⊔-cong a₁≈a₂ a₃≈a₄ | a₁≼a₃ + ... | just a₁⊔a₃ | just a₂⊔a₄ | ≈-just a₁⊔a₃≈a₂≈a₄ | ≈-just a₁⊔a₃≈a₃ + = ≈-just (≈-trans (≈-trans (≈-sym a₁⊔a₃≈a₂≈a₄) a₁⊔a₃≈a₃) a₃≈a₄) + + -- curious: similar property (properties?) to partial commutative monoids (PCMs) + -- from Iris. + ≼-partialˡ : ∀ {a a₁ a₂} → a₁ ≼ a₂ → (a ⊔? a₁) ≡ nothing → (a ⊔? a₂) ≡ nothing + ≼-partialˡ {a} {a₁} {a₂} a₁≼a₂ a⊔a₁≡nothing + with a₁ ⊔? a₂ | a₁≼a₂ | a ⊔? a₁ | a⊔a₁≡nothing | ⊔-assoc a a₁ a₂ + ... | just a₁⊔a₂ | ≈-just a₁⊔a₂≈a₂ | nothing | refl | aa₁⊔a₂≈a⊔a₁a₂ + with a ⊔? a₁⊔a₂ | aa₁⊔a₂≈a⊔a₁a₂ | a ⊔? a₂ | ≈-⊔-cong (≈-refl {a = a}) a₁⊔a₂≈a₂ + ... | nothing | ≈-nothing | nothing | ≈-nothing = refl + + ≼-partialʳ : ∀ {a a₁ a₂} → a₁ ≼ a₂ → (a₁ ⊔? a) ≡ nothing → (a₂ ⊔? a) ≡ nothing + ≼-partialʳ {a} {a₁} {a₂} a₁≼a₂ a₁⊔a≡nothing + with a₁ ⊔? a | a ⊔? a₁ | a₁⊔a≡nothing | ⊔-comm a₁ a | ≼-partialˡ {a} {a₁} {a₂} a₁≼a₂ + ... | nothing | nothing | refl | ≈-nothing | refl⇒a⊔a₂=nothing + with a₂ ⊔? a | a ⊔? a₂ | ⊔-comm a₂ a | refl⇒a⊔a₂=nothing refl + ... | nothing | nothing | ≈-nothing | refl = refl + + ≼-refl : ∀ (x : A) → x ≼ x + ≼-refl x = ⊔-idemp x + + ≼-refl' : ∀ {a₁ a₂ : A} → a₁ ≈ a₂ → a₁ ≼ a₂ + ≼-refl' {a₁} {a₂} a₁≈a₂ = ≈-≼-cong ≈-refl a₁≈a₂ (≼-refl a₁) + + x⊔?x≼x : ∀ (x : A) → maybe (λ x⊔x → x⊔x ≼ x) (Empty a) (x ⊔? x) + x⊔?x≼x x + with x ⊔? x | ⊔-idemp x + ... | just x⊔x | ≈-just x⊔x≈x = ≈-≼-cong (≈-sym x⊔x≈x) ≈-refl (≼-refl x) + + x≼x⊔?y : ∀ (x y : A) → maybe (λ x⊔y → x ≼ x⊔y) (Trivial a) (x ⊔? y) + x≼x⊔?y x y + with x ⊔? y in x⊔?y= | x ⊔? x | ⊔-idemp x | ⊔-assoc x x y | x⊔?x≼x x + ... | nothing | _ | _ | _ | _ = mkTrivial + ... | just x⊔y | just x⊔x | ≈-just x⊔x≈x | ⊔-assoc-xxy | x⊔x≼x + with x⊔x ⊔? y in xx⊔?y= | x ⊔? x⊔y + ... | nothing | nothing = + ⊥-elim (maybe-injection _ (trans (sym x⊔?y=) (≼-partialʳ x⊔x≼x xx⊔?y=))) + ... | just xx⊔y | just x⊔xy rewrite (sym xx⊔?y=) rewrite (sym x⊔?y=) = + ≈?-trans (≈?-sym ⊔-assoc-xxy) (≈-⊔-cong x⊔x≈x (≈-refl {a = y})) + record HasIdentityElement : Set a where field x : A not-partial : ∀ (a₁ a₂ : A) → Σ A (λ a₃ → (a₁ ⊔? a₂) ≡ just a₃) x-identity : (a : A) → (x ⊔? a) ≈? just a -data Trivial a : Set a where - instance - mkTrivial : Trivial a - -data Empty a : Set a where - Maybe-≈ : ∀ {a} {A : Set a} → (_≈_ : A → A → Set a) → Maybe A → A → Set a Maybe-≈ _≈_ (just a₁) a₂ = a₁ ≈ a₂ Maybe-≈ {a} _≈_ nothing a₂ = Trivial a