From 05e693594d9c7f76a0ed9a77c3a1e5767eb983ef Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 25 Jul 2025 17:17:25 +0200 Subject: [PATCH] Prove idempotence of meet and join Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 18 ++++++++++++++++++ 1 file changed, 18 insertions(+) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 68a7da7..b9ed96f 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -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₃=?) +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 {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₂) @@ -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 ... | 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 field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)