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

Prove idempotence of meet and join

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-25 17:17:25 +02:00
parent 90e0046707
commit 05e693594d
1 changed files with 18 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
Lattice/Builder.agda
View File

@ -806,6 +806,15 @@ pathJoin'-assoc {Ls = add-via-greatest l ls {{greatest = greatest}}} (inj₂ p
... | nothing | _ | _ = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₁ p₂ greatest p₁⊔?p₂=?) ... | nothing | _ | _ = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₁ p₂ greatest p₁⊔?p₂=?)
... | _ | nothing | _ = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₂ p₃ greatest p₂⊔?p₃=?) ... | _ | nothing | _ = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₂ p₃ greatest p₂⊔?p₃=?)
pathJoin'-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (eqPath' Ls) (pathJoin' Ls)
pathJoin'-idemp {Ls = single l} lv = lvJoin-idemp (toList l) lv
pathJoin'-idemp {Ls = add-via-least l ls} (inj₁ lv) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-idemp (toList l) lv)
pathJoin'-idemp {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p)
with pathJoin' ls p p | pathJoin'-idemp {Ls = ls} p
... | just p⊔p | ≈-just p⊔p≈p = ≈-just p⊔p≈p
pathJoin'-idemp {Ls = add-via-greatest l ls} (inj₁ lv) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-idemp (toList l) lv)
pathJoin'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathJoin'-idemp {Ls = ls} p)
pathMeet'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathMeet' Ls) 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 = 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₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-comm (toList l) lv₁ lv₂)
@ -931,6 +940,15 @@ pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂
... | nothing | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁ p₂⊓p₃ = ≈-nothing ... | nothing | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁ p₂⊓p₃ = ≈-nothing
... | just p₁⊓p₂ | nothing | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁⊓p₂ p₃ = ≈-nothing ... | just p₁⊓p₂ | nothing | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁⊓p₂ p₃ = ≈-nothing
pathMeet'-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (eqPath' Ls) (pathMeet' Ls)
pathMeet'-idemp {Ls = single l} lv = lvMeet-idemp (toList l) lv
pathMeet'-idemp {Ls = add-via-least l ls} (inj₁ lv) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-idemp (toList l) lv)
pathMeet'-idemp {Ls = add-via-least l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p)
pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₁ lv)
with lvMeet (toList l) lv lv | lvMeet-idemp (toList l) lv
... | just lv⊔lv | ≈-just lv⊔lv≈lv = ≈-just lv⊔lv≈lv
pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p)
record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂) field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)