DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Switch to representing least/greatest with absorption

Browse Source 
It's more convenient this way to require non-partiality.

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-22 17:59:54 +02:00
parent 5705f256fd
commit d3bac2fe60
1 changed files with 65 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

88
Lattice/Builder.agda
View File

@ -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₂ with a ⊔? a₁⊔a₂ | aa₁⊔a₂≈a⊔a₁a₂ | a ⊔? a₂ | ≈-⊔-cong (≈-refl {a = a}) a₁⊔a₂≈a₂
... | nothing | ≈-nothing | nothing | ≈-nothing = refl ... | 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 → (a₂ ⊔? a) ≡ nothing
≼-partialʳ {a} {a₁} {a₂} a₁≼a₂ 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₂ 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 ... | nothing | nothing | refl | ≈-nothing | refl⇒a⊔a₂=nothing
with a₂ ⊔? a | a ⊔? a₂ | ⊔-comm a₂ a | refl⇒a⊔a₂=nothing refl 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=) = ... | 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})) ≈?-trans (≈?-sym ⊔-assoc-xxy) (≈-⊔-cong x⊔x≈x (≈-refl {a = y}))
record HasIdentityElement : Set a where record HasAbsorbingElement : Set a where
field field
x : A x : A
not-partial : ∀ (a₁ a₂ : A) → Σ A (λ a₃ → (a₁ ⊔? a₂) ≡ just a₃) x-absorbˡ : (a : A) → (x ⊔? a) ≈? just x
x-identityˡ : (a : A) → (x ⊔? a) ≈? just a
x-identityʳ : (a : A) → (a ⊔? x) ≈? just a x-absorbʳ : (a : A) → (a ⊔? x) ≈? just x
x-identityʳ a = ≈?-trans (⊔-comm a x) (x-identityˡ a) 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} record IsPartialLattice {a} {A : Set a}
(_≈_ : 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)
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 () open IsPartialSemilattice partialMeetSemilattice using ()
renaming renaming
( ≈-⊔-cong to ≈-⊓-cong ( HasAbsorbingElement to HasLeastElement
; ≈-⊔-cong to ≈-⊓-cong
; ⊔-assoc to ⊓-assoc ; ⊔-assoc to ⊓-assoc
; ⊔-comm to ⊓-comm ; ⊔-comm to ⊓-comm
; ⊔-idemp to ⊓-idemp ; ⊔-idemp to ⊓-idemp
@ -161,15 +171,25 @@ record PartialLattice {a} (A : Set a) : Set (lsuc a) where
open IsPartialLattice isPartialLattice public open IsPartialLattice isPartialLattice public
HasLeastElement : Set a greatest-⊓-identʳ : ∀ (le : HasGreatestElement) (x : A) →
HasLeastElement = (x ⊓? HasGreatestElement.x le) ≈? (just x)
IsPartialSemilattice.HasIdentityElement greatest-⊓-identʳ le x
(IsPartialLattice.partialJoinSemilattice isPartialLattice) 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 greatest-⊓-identˡ : ∀ (le : HasGreatestElement) (x : A) →
HasGreatestElement = (HasGreatestElement.x le ⊓? x) ≈? (just x)
IsPartialSemilattice.HasIdentityElement greatest-⊓-identˡ le x = ≈?-trans (⊓-comm (HasGreatestElement.x le) x) (greatest-⊓-identʳ le x)
(IsPartialLattice.partialMeetSemilattice isPartialLattice)
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 record PartialLatticeType (a : Level) : Set (lsuc a) where
field 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₂) pathJoin' (add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls) (inj₂ p₁) (inj₂ p₂)
with pathJoin' ls p₁ p₂ with pathJoin' ls p₁ p₂
... | just p = just (inj₂ 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₁ 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₁ lv₁) (inj₂ p₂) = just (inj₁ lv₁)
pathJoin' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = 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 ... | nothing
with head ls | greatest | valueAtHead ls with head ls | greatest | valueAtHead ls
... | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah ... | _ | 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₁ 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₁ lv₂) = just (inj₂ p₁)
pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathMeet' ls p₁ 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 : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvMeet L)
lvMeet-idemp = lvCombine-idemp PartialLatticeType._⊓?_ PartialLatticeType.⊓-idemp 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 : ∀ {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 = 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 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₂) 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₂ 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' ... | 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₁ 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-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₂) 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 with ls | greatest | valueAtHead ls
-- begin dumb: don't know why, but abstracting on `head ls` leads to an ill-formed case -- begin dumb: don't know why, but abstracting on `head ls` leads to an ill-formed case
... | single l' | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah ... | 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 ... | 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 ... | 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 -- 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 {{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₂) pathMeet'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqPath'-refl ls p₂)