From d3bac2fe60eb22edaebc15e46ba78381f9613bb2 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 22 Jul 2025 17:59:54 +0200 Subject: [PATCH] Switch to representing least/greatest with absorption It's more convenient this way to require non-partiality. Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 88 ++++++++++++++++++++++++++++++++------------ 1 file changed, 65 insertions(+), 23 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index cbcfa56..33dd459 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -91,8 +91,8 @@ record IsPartialSemilattice {a} {A : Set 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 + ≼-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 @@ -120,14 +120,21 @@ record IsPartialSemilattice {a} {A : Set a} ... | 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 + record HasAbsorbingElement : 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 + x-absorbˡ : (a : A) → (x ⊔? a) ≈? just x - x-identityʳ : (a : A) → (a ⊔? x) ≈? just a - x-identityʳ a = ≈?-trans (⊔-comm a x) (x-identityˡ a) + x-absorbʳ : (a : A) → (a ⊔? x) ≈? just x + x-absorbʳ a = ≈?-trans (⊔-comm a x) (x-absorbˡ a) + + not-partial : ∀ (a₁ a₂ : A) → Σ A (λ a₃ → (a₁ ⊔? a₂) ≡ just a₃) + not-partial a₁ a₂ + with a₁ ⊔? a₂ | ≼-partialˡ {a = a₁} (x-absorbʳ a₂) + ... | just a₁⊔a₂ | _ = (a₁⊔a₂ , refl) + ... | nothing | refl⇒a₁⊔?x=nothing + with a₁ ⊔? x | refl⇒a₁⊔?x=nothing refl | x-absorbʳ a₁ + ... | nothing | refl | () record IsPartialLattice {a} {A : Set a} (_≈_ : A → A → Set a) @@ -141,10 +148,13 @@ record IsPartialLattice {a} {A : Set a} 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 partialJoinSemilattice + renaming (HasAbsorbingElement to HasGreatestElement) + public open IsPartialSemilattice partialMeetSemilattice using () renaming - ( ≈-⊔-cong to ≈-⊓-cong + ( HasAbsorbingElement to HasLeastElement + ; ≈-⊔-cong to ≈-⊓-cong ; ⊔-assoc to ⊓-assoc ; ⊔-comm to ⊓-comm ; ⊔-idemp to ⊓-idemp @@ -161,15 +171,25 @@ record PartialLattice {a} (A : Set a) : Set (lsuc a) where open IsPartialLattice isPartialLattice public - HasLeastElement : Set a - HasLeastElement = - IsPartialSemilattice.HasIdentityElement - (IsPartialLattice.partialJoinSemilattice isPartialLattice) + greatest-⊓-identʳ : ∀ (le : HasGreatestElement) (x : A) → + (x ⊓? HasGreatestElement.x le) ≈? (just x) + greatest-⊓-identʳ le x + with x ⊔? (HasGreatestElement.x le) | HasGreatestElement.x-absorbʳ le x | absorb-⊓-⊔ x (HasGreatestElement.x le) + ... | just x⊔greatest | ≈-just x⊔greatest≈greatest | x⊓xgreatest≈?x = ≈?-trans (≈?-sym (≈-⊓-cong (≈-refl {a = x}) x⊔greatest≈greatest)) x⊓xgreatest≈?x - HasGreatestElement : Set a - HasGreatestElement = - IsPartialSemilattice.HasIdentityElement - (IsPartialLattice.partialMeetSemilattice isPartialLattice) + greatest-⊓-identˡ : ∀ (le : HasGreatestElement) (x : A) → + (HasGreatestElement.x le ⊓? x) ≈? (just x) + greatest-⊓-identˡ le x = ≈?-trans (⊓-comm (HasGreatestElement.x le) x) (greatest-⊓-identʳ le x) + + least-⊔-identʳ : ∀ (le : HasLeastElement) (x : A) → + (x ⊔? HasLeastElement.x le) ≈? (just x) + least-⊔-identʳ le x + with x ⊓? (HasLeastElement.x le) | HasLeastElement.x-absorbʳ le x | absorb-⊔-⊓ x (HasLeastElement.x le) + ... | just x⊓least | ≈-just x⊓least≈least | x⊔xleast≈?x = ≈?-trans (≈?-sym (≈-⊔-cong (≈-refl {a = x}) x⊓least≈least)) x⊔xleast≈?x + + least-⊔-identˡ : ∀ (le : HasLeastElement) (x : A) → + (HasLeastElement.x le ⊔? x) ≈? (just x) + least-⊔-identˡ le x = ≈?-trans (⊔-comm (HasLeastElement.x le) x) (least-⊔-identʳ le x) record PartialLatticeType (a : Level) : Set (lsuc a) where field @@ -257,7 +277,7 @@ pathJoin' (add-via-least l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₁ lv₂ pathJoin' (add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls) (inj₂ p₁) (inj₂ p₂) with pathJoin' ls p₁ p₂ ... | just p = just (inj₂ p) -... | nothing = just (inj₁ (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasLeast))) +... | nothing = just (inj₁ (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasLeast))) pathJoin' (add-via-greatest l ls) (inj₁ lv₁) (inj₁ lv₂) = Maybe.map inj₁ (lvJoin (toList l) lv₁ lv₂) pathJoin' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₁ lv₁) pathJoin' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₁ lv₂) @@ -275,7 +295,7 @@ pathMeet' (add-via-greatest l ls {{greatest}}) (inj₁ lv₁) (inj₁ lv₂) ... | nothing with head ls | greatest | valueAtHead ls ... | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah - = just (inj₂ (vah (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasGreatest)))) + = just (inj₂ (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest)))) pathMeet' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₂ p₂) pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₂ p₁) pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathMeet' ls p₁ p₂) @@ -488,13 +508,35 @@ lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-co lvMeet-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvMeet L) lvMeet-idemp = lvCombine-idemp PartialLatticeType._⊓?_ PartialLatticeType.⊓-idemp +lvJoin-greatest-total : ∀ {a} {L : Layer a} → (lv₁ lv₂ : LayerValue L) → LayerGreatest L → lvJoin (toList L) lv₁ lv₂ ≡ nothing → ⊥ +lvJoin-greatest-total {L = plt ∷⁺ []} (inj₁ v₁) (inj₁ v₂) (MkLayerGreatest {{hasGreatest = hasGreatest}}) v₁⊔v₂≡nothing + with IsPartialLattice.HasGreatestElement.not-partial (PartialLatticeType.isPartialLattice plt) hasGreatest v₁ v₂ +... | (v₁v₂ , v₁⊔v₂≡justv₁v₂) + with trans (cong (Maybe.map inj₁) (sym v₁⊔v₂≡justv₁v₂)) v₁⊔v₂≡nothing +... | () + +pathJoin'-greatest-total : ∀ {a} {Ls : Layers a} → (p₁ p₂ : Path' Ls) → LayerGreatest (head Ls) → pathJoin' Ls p₁ p₂ ≡ nothing → ⊥ +pathJoin'-greatest-total {Ls = single L} lv₁ lv₂ layerGreatest lv₁⊔lv₂≡nothing = lvJoin-greatest-total {L = L} lv₁ lv₂ layerGreatest lv₁⊔lv₂≡nothing +pathJoin'-greatest-total {Ls = add-via-greatest L _} (inj₁ lv₁) (inj₁ lv₂) layerGreatest _ + with nothing <- lvJoin (toList L) lv₁ lv₂ in lv₁⊔?lv₂=? = lvJoin-greatest-total {L = L} lv₁ lv₂ layerGreatest lv₁⊔?lv₂=? +pathJoin'-greatest-total {Ls = add-via-least L _} (inj₁ lv₁) (inj₁ lv₂) layerGreatest _ + with nothing <- lvJoin (toList L) lv₁ lv₂ in lv₁⊔?lv₂=? = lvJoin-greatest-total {L = L} lv₁ lv₂ layerGreatest lv₁⊔?lv₂=? +pathJoin'-greatest-total {Ls = add-via-least (plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} Ls'} (inj₂ p₁) (inj₂ p₂) (MkLayerGreatest {{hasGreatest = hasGreatest}}) inj₂p₁⊔inj₂p₂≡nothing + with pathJoin' Ls' p₁ p₂ | inj₂p₁⊔inj₂p₂≡nothing +... | nothing | () +... | just _ | () +pathJoin'-greatest-total {Ls = add-via-greatest L Ls {{layerGreatest}}} (inj₂ p₁) (inj₂ p₂) _ inj₂p₁⊔inj₂p₂≡nothing + with pathJoin' Ls p₁ p₂ in p₁⊔p₂=? | inj₂p₁⊔inj₂p₂≡nothing +... | just p₁⊔p₂ | () +... | nothing | refl = pathJoin'-greatest-total {Ls = Ls} p₁ p₂ layerGreatest p₁⊔p₂=? + pathJoin'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathJoin' Ls) pathJoin'-comm {Ls = single l} lv₁ lv₂ = lvJoin-comm (toList l) lv₁ lv₂ pathJoin'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-comm (toList l) lv₁ lv₂) pathJoin'-comm {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂) with pathJoin' ls p₁ p₂ | pathJoin' ls p₂ p₁ | pathJoin'-comm {Ls = ls} p₁ p₂ ... | just p | just p' | ≈-just p≈p' = ≈-just p≈p' -... | nothing | nothing | ≈-nothing = ≈-just (eqLv-refl l (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasLeast))) +... | nothing | nothing | ≈-nothing = ≈-just (eqLv-refl l (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasLeast))) pathJoin'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqLv-refl l lv₁) pathJoin'-comm {Ls = add-via-least l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqLv-refl l lv₂) pathJoin'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-comm (toList l) lv₁ lv₂) @@ -515,11 +557,11 @@ pathMeet'-comm {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ with ls | greatest | valueAtHead ls -- begin dumb: don't know why, but abstracting on `head ls` leads to an ill-formed case ... | single l' | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah - = ≈-just (eqLv-refl l' (vah (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasGreatest)))) + = ≈-just (eqLv-refl l' (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest)))) ... | add-via-least l' {{least = least}} ls' | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah - = ≈-just (eqPath'-refl (add-via-least l' {{least}} ls') (vah (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasGreatest)))) + = ≈-just (eqPath'-refl (add-via-least l' {{least}} ls') (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest)))) ... | add-via-greatest l' ls' {{greatest = greatest'}} | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah - = ≈-just (eqPath'-refl (add-via-greatest l' ls' {{greatest'}}) (vah (inj₁ (IsPartialSemilattice.HasIdentityElement.x hasGreatest)))) + = ≈-just (eqPath'-refl (add-via-greatest l' ls' {{greatest'}}) (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest)))) -- end dumb pathMeet'-comm {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-comm {Ls = ls} p₁ p₂) pathMeet'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqPath'-refl ls p₂)