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

Add helper definitions for partial commutativity, associativity, reflexivity

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-02 15:11:12 -05:00
parent dd101c6e9b
commit da6e82d04b
1 changed files with 19 additions and 10 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
Lattice/Builder.agda
View File

@ -29,6 +29,15 @@ lift-≈-map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B)
lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ (just a₁) (just a₂) (≈-just a₁≈a₂) = ≈-just (≈ᵃ→≈ᵇ a₁ a₂ a₁≈a₂)
lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ nothing nothing ≈-nothing = ≈-nothing
PartialAssoc : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialAssoc {a} {A} _≈_ _⊗_ = ∀ (x y z : A) → lift-≈ _≈_ ((x ⊗ y) >>= (_⊗ z)) ((y ⊗ z) >>= (x ⊗_))
PartialComm : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialComm {a} {A} _≈_ _⊗_ = ∀ (x y : A) → lift-≈ _≈_ (x ⊗ y) (y ⊗ x)
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)
record IsPartialSemilattice {a} {A : Set a}
(_≈_ : A → A → Set a)
(_⊔?_ : A → A → Maybe A) : Set a where
@ -40,9 +49,9 @@ record IsPartialSemilattice {a} {A : Set a}
≈-equiv : IsEquivalence A _≈_
≈-⊔-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → (a₁ ⊔? a₃) ≈? (a₂ ⊔? a₄)
⊔-assoc : (x y z : A) → ((x ⊔? y) >>= (_⊔? z)) ≈? ((y ⊔? z) >>= (x ⊔?_))
⊔-comm : (x y : A) → (x ⊔? y) ≈? (y ⊔? x)
⊔-idemp : (x : A) → (x ⊔? x) ≈? just x
⊔-assoc : PartialAssoc _≈_ _⊔?_
⊔-comm : PartialComm _≈_ _⊔?_
⊔-idemp : PartialIdemp _≈_ _⊔?_
record HasIdentityElement : Set a where
field
@ -254,9 +263,9 @@ eqPath'-refl (add-via-greatest l ls) (inj₂ p) = eqPath'-refl ls p
-- prove theorems such as commutativity and idempotence.
lvCombine-comm : ∀ {a} (f : CombineForPLT a) →
(∀ plt v₁ v₂ → PartialLatticeType._≈?_ plt (f plt v₁ v₂) (f plt v₂ v₁)) →
∀ (L : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue L) →
lift-≈ (eqL L) (lvCombine f L lv₁ lv₂) (lvCombine f L lv₂ lv₁)
(∀ plt → PartialComm (PartialLatticeType._≈_ plt) (f plt)) →
∀ (L : List (PartialLatticeType a)) →
PartialComm (eqL L) (lvCombine f L)
lvCombine-comm f f-comm L@(plt ∷ plts) lv₁@(inj₁ v₁) (inj₁ v₂)
with f plt v₁ v₂
| f plt v₂ v₁
@ -270,13 +279,13 @@ lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂)
lvCombine-comm f f-comm (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = ≈-nothing
lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = ≈-nothing
lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue L) → lift-≈ (eqL L) (lvJoin L lv₁ lv₂) (lvJoin L lv₂ lv₁)
lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvJoin L)
lvJoin-comm = lvCombine-comm PartialLatticeType._⊔?_ PartialLatticeType.⊔-comm
lvMeet-comm : ∀ {a} (L : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue L) → lift-≈ (eqL L) (lvMeet L lv₁ lv₂) (lvMeet L lv₂ lv₁)
lvMeet-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvMeet L)
lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-comm
pathJoin'-comm : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path' Ls) → lift-≈ (eqPath' Ls) (pathJoin' Ls p₁ p₂) (pathJoin' Ls 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₂)
@ -290,7 +299,7 @@ pathJoin'-comm {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₂ p₂) = lift-
pathJoin'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqLv-refl l lv₁)
pathJoin'-comm {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqLv-refl l lv₂)
pathMeet'-comm : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path' Ls) → lift-≈ (eqPath' Ls) (pathMeet' Ls p₁ p₂) (pathMeet' Ls p₂ p₁)
pathMeet'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathMeet' Ls)
pathMeet'-comm {Ls = single l} lv₁ lv₂ = lvMeet-comm (toList l) lv₁ lv₂
pathMeet'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-comm (toList l) lv₁ lv₂)
pathMeet'-comm {Ls = add-via-least l ls} (inj₂ p₁) (inj₂ p₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-comm {Ls = ls} p₁ p₂)