From c1c34c69a5118839ce6892190fee4068981aab71 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 11 Jul 2025 15:44:29 +0200 Subject: [PATCH] Strengthen absorption laws If x \/ y is defined, x /\ (x \/ y) has to be defined, too. Previously, we stated them in terms of "if x /\ (x \/ y) is defined", which is not right. Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index f9f2374..4ba0465 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -129,10 +129,6 @@ record IsPartialSemilattice {a} {A : Set a} x-identityʳ : (a : A) → (a ⊔? x) ≈? just a x-identityʳ a = ≈?-trans (⊔-comm a x) (x-identityˡ a) -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 - record IsPartialLattice {a} {A : Set a} (_≈_ : A → A → Set a) (_⊔?_ : A → A → Maybe A) @@ -142,8 +138,8 @@ record IsPartialLattice {a} {A : Set a} {{partialJoinSemilattice}} : IsPartialSemilattice _≈_ _⊔?_ {{partialMeetSemilattice}} : IsPartialSemilattice _≈_ _⊓?_ - absorb-⊔-⊓ : (x y : A) → Maybe-≈ _≈_ ((x ⊓? y) >>= (x ⊔?_)) x - absorb-⊓-⊔ : (x y : A) → Maybe-≈ _≈_ ((x ⊔? y) >>= (x ⊓?_)) x + absorb-⊔-⊓ : (x y : A) → maybe (λ x⊓y → lift-≈ _≈_ (x ⊔? x⊓y) (just x)) (Trivial _) (x ⊓? y) + absorb-⊓-⊔ : (x y : A) → maybe (λ x⊔y → lift-≈ _≈_ (x ⊓? x⊔y) (just x)) (Trivial _) (x ⊔? y) open IsPartialSemilattice partialJoinSemilattice public open IsPartialSemilattice partialMeetSemilattice using ()