From 6055a79e6a2ea44dca77fadae895ccc593fe7ca7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 22 Jul 2025 18:04:53 +0200 Subject: [PATCH] Prove a side lemma about nothing/just Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 95 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 95 insertions(+) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 9ad74bb..4e689a2 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -124,6 +124,14 @@ 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})) + y≼x⊔?y : ∀ (x y : A) → maybe (λ x⊔y → y ≼ x⊔y) (Trivial a) (x ⊔? y) + y≼x⊔?y x y + with x ⊔? y | y ⊔? x | ⊔-comm y x | x≼x⊔?y y x + ... | nothing | nothing | ≈-nothing | _ = mkTrivial + ... | just x⊔y | just y⊔x | ≈-just y⊔x≈x⊔y | y⊔yx≈yx + = ≈?-trans (≈?-sym (≈-⊔-cong (≈-refl {a = y}) y⊔x≈x⊔y)) + (≈?-trans y⊔yx≈yx (≈-just y⊔x≈x⊔y)) + record HasAbsorbingElement : Set a where field x : A @@ -162,6 +170,15 @@ record IsPartialLattice {a} {A : Set a} ; ⊔-assoc to ⊓-assoc ; ⊔-comm to ⊓-comm ; ⊔-idemp to ⊓-idemp + ; _≼_ to _≽_ + ; ≈-≼-cong to ≈-≽-cong + ; ≼-partialˡ to ≽-partialˡ + ; ≼-partialʳ to ≽-partialʳ + ; ≼-refl to ≽-refl + ; ≼-refl' to ≽-refl' + ; x⊔?x≼x to x⊓?x≽x + ; x≼x⊔?y to x≽x⊓?y + ; y≼x⊔?y to y≽x⊓?y ) public @@ -599,6 +616,84 @@ 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₂) +lvCombine-related : ∀ {a} (f : CombineForPLT a) → + (∀ plt {a₁} {a₂} {a} → + PartialLatticeType._≈?_ plt (f plt a₁ a₂) (just a₂) → + (f plt a₁ a) ≡ nothing → (f plt a₂ a) ≡ nothing) → + (∀ plt a₁ a₂ → + maybe (λ a₁⊔a₂ → PartialLatticeType._≈?_ plt (f plt a₂ a₁⊔a₂) (just a₁⊔a₂)) + (Trivial a) (f plt a₁ a₂)) → + ∀ (L : List (PartialLatticeType a)) + (lv₁ lv₂ lv₃ : ListValue L) → (lv₁⊔lv₂ : ListValue L) → lvCombine f L lv₁ lv₂ ≡ just lv₁⊔lv₂ → lvCombine f L lv₂ lv₃ ≡ nothing → lvCombine f L lv₁⊔lv₂ lv₃ ≡ nothing +lvCombine-related f f-partial f-Mono [] () +lvCombine-related f f-partial f-Mono (plt ∷ plts) (inj₁ v₁) (inj₁ v₂) lv₃ lv₁⊗lv₂ lv₁⊗?lv₂≡justlv₁⊗lv₂ lv₂⊗?lv₃≡nothing + with f plt v₁ v₂ | lv₁⊗?lv₂≡justlv₁⊗lv₂ | lv₃ | f-Mono plt v₁ v₂ +... | just _ | refl | inj₂ _ | _ = refl +... | just v₁⊗v₂ | refl | inj₁ v₃ | v₂≼v₁⊗v₂ + with f plt v₂ v₃ | lv₂⊗?lv₃≡nothing | f-partial plt {v₂} {v₁⊗v₂} {v₃} v₂≼v₁⊗v₂ +... | nothing | refl | refl⇒v₁v₂⊗?v₃≡nothing = cong (Maybe.map inj₁) (refl⇒v₁v₂⊗?v₃≡nothing refl) +lvCombine-related f f-partial f-Mono (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) lv₃ lv₁⊔lv₂ lv₁⊗?lv₂≡justlv₁⊗lv₂ lv₂⊗?lv₃≡nothing + with lvCombine f plts lv₁ lv₂ in lv₁⊗?lv₂≡? | lv₁⊗?lv₂≡justlv₁⊗lv₂ | lv₃ +... | just lv₁⊔lv₂ | refl | inj₁ v₃ = refl +... | just lv₁⊔lv₂ | refl | inj₂ lv₃' + with lvCombine f plts lv₂ lv₃' in lv₂⊗?lv₃'≡? | lv₂⊗?lv₃≡nothing +... | nothing | refl = cong (Maybe.map inj₂) (lvCombine-related f f-partial f-Mono plts lv₁ lv₂ lv₃' lv₁⊔lv₂ lv₁⊗?lv₂≡? lv₂⊗?lv₃'≡?) + +lvJoin-related : ∀ {a} (L : List (PartialLatticeType a)) + (lv₁ lv₂ lv₃ : ListValue L) → (lv₁⊔lv₂ : ListValue L) → lvJoin L lv₁ lv₂ ≡ just lv₁⊔lv₂ → lvJoin L lv₂ lv₃ ≡ nothing → lvJoin L lv₁⊔lv₂ lv₃ ≡ nothing +lvJoin-related = lvCombine-related PartialLatticeType._⊔?_ PartialLatticeType.≼-partialʳ PartialLatticeType.y≼x⊔?y + +lvMeet-related : ∀ {a} (L : List (PartialLatticeType a)) + (lv₁ lv₂ lv₃ : ListValue L) → (lv₁⊔lv₂ : ListValue L) → lvMeet L lv₁ lv₂ ≡ just lv₁⊔lv₂ → lvMeet L lv₂ lv₃ ≡ nothing → lvMeet L lv₁⊔lv₂ lv₃ ≡ nothing +lvMeet-related = lvCombine-related PartialLatticeType._⊓?_ PartialLatticeType.≽-partialʳ PartialLatticeType.y≽x⊓?y + +-- crucially for the well-behavedness of path joins etc., divergences (e.g., +-- "couldn't find path join") don't propagate far if they happen near +-- the end of a path. As a result, it should not be possible to have two +-- "deep" paths that produce `nothing`. The *-shallow-* lemmas state that. + +pathJoin'-shallow-least : ∀ {a} (l : Layer a) (ls : Layers a) least (p₁ p₂ : Path' ls) → pathJoin' (add-via-least l {{least}} ls) (inj₂ p₁) (inj₂ p₂) ≡ nothing → ⊥ +pathJoin'-shallow-least l@(plt ∷⁺ []) ls (MkLayerLeast {{hasLeast = hasLeast}}) p₁ p₂ inj₂p₁⊔inj₂p₂≡nothing + with pathJoin' ls p₁ p₂ | inj₂p₁⊔inj₂p₂≡nothing +... | just _ | () +... | nothing | () + +pathJoin'-shallow-greatest : ∀ {a} (l : Layer a) (ls : Layers a) greatest (p₁ p₂ : Path' ls) → pathJoin' (add-via-greatest l ls {{greatest}}) (inj₂ p₁) (inj₂ p₂) ≡ nothing → ⊥ +pathJoin'-shallow-greatest l ls greatest p₁ p₂ inj₂p₁⊔inj₂p₂≡nothing + with pathJoin' ls p₁ p₂ | pathJoin'-greatest-total {Ls = ls} p₁ p₂ greatest | inj₂p₁⊔inj₂p₂≡nothing +... | just p₁⊔p₂ | _ | () +... | nothing | refl⇒⊥ | _ = ⊥-elim (refl⇒⊥ refl) + +pathJoin'-related : ∀ {a} {Ls : Layers a} (p₁ p₂ p₃ : Path' Ls) → (p₁⊔p₂ : Path' Ls) → pathJoin' Ls p₁ p₂ ≡ just p₁⊔p₂ → pathJoin' Ls p₂ p₃ ≡ nothing → pathJoin' Ls p₁⊔p₂ p₃ ≡ nothing +pathJoin'-related {Ls = single l} = lvJoin-related (toList l) +pathJoin'-related {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) _ lv₁⊔?lv₂=justlv₁⊔lv₂ lv₂⊔?lv₃=nothing + with lvJoin (toList l) lv₁ lv₂ | lv₁⊔?lv₂=justlv₁⊔lv₂ | lvJoin (toList l) lv₂ lv₃ | lv₂⊔?lv₃=nothing | lvJoin-related (toList l) lv₁ lv₂ lv₃ +... | just lv₁⊔lv₂ | refl | nothing | refl | refl⇒refl⇒lv₁lv₂⊔lv₃=nothing = cong (Maybe.map inj₁) (refl⇒refl⇒lv₁lv₂⊔lv₃=nothing lv₁⊔lv₂ refl refl) +pathJoin'-related {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂) (inj₁ lv₃) _ refl lv₂⊔?lv₃=nothing rewrite lv₂⊔?lv₃=nothing = refl +pathJoin'-related {Ls = add-via-least l {{least}} ls} _ (inj₂ p₂) (inj₂ p₃) _ _ injp₂⊔?injp₃=nothing = ⊥-elim (pathJoin'-shallow-least l ls least p₂ p₃ injp₂⊔?injp₃=nothing) +pathJoin'-related {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) _ lv₁⊔?lv₂=justlv₁⊔lv₂ lv₂⊔?lv₃=nothing + with lvJoin (toList l) lv₁ lv₂ | lv₁⊔?lv₂=justlv₁⊔lv₂ | lvJoin (toList l) lv₂ lv₃ | lv₂⊔?lv₃=nothing | lvJoin-related (toList l) lv₁ lv₂ lv₃ +... | just lv₁⊔lv₂ | refl | nothing | refl | refl⇒refl⇒lv₁lv₂⊔lv₃=nothing = cong (Maybe.map inj₁) (refl⇒refl⇒lv₁lv₂⊔lv₃=nothing lv₁⊔lv₂ refl refl) +pathJoin'-related {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₁ lv₂) (inj₁ lv₃) _ refl lv₂⊔?lv₃=nothing rewrite lv₂⊔?lv₃=nothing = refl +pathJoin'-related {Ls = add-via-greatest l ls {{greatest}}} _ (inj₂ p₂) (inj₂ p₃) _ _ injp₂⊔?injp₃=nothing + with pathJoin' ls p₂ p₃ in p₂⊔?p₃=? | injp₂⊔?injp₃=nothing +... | nothing | refl = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₂ p₃ greatest p₂⊔?p₃=?) + +pathJoin'-related' : ∀ {a} {Ls : Layers a} (p₁ p₂ p₃ : Path' Ls) → (p₂⊔p₃ : Path' Ls) → pathJoin' Ls p₂ p₃ ≡ just p₂⊔p₃ → pathJoin' Ls p₁ p₂ ≡ nothing → pathJoin' Ls p₁ p₂⊔p₃ ≡ nothing +pathJoin'-related' {Ls = Ls} p₁ p₂ p₃ p₂⊔p₃ p₂⊔?p₃=justp₂⊔p₃ p₁⊔?p₂=nothing + rewrite p₂⊔?p₃=justp₂⊔p₃ + rewrite p₁⊔?p₂=nothing + with pathJoin' Ls p₂ p₃ in p₂⊔?p₃=justp₂⊔p₃' | pathJoin' Ls p₃ p₂ in p₃⊔p₂=? | pathJoin'-comm {Ls = Ls} p₂ p₃ + | pathJoin' Ls p₂ p₁ in p₂⊔p₁=? | pathJoin' Ls p₁ p₂ | pathJoin'-comm {Ls = Ls} p₂ p₁ +... | just p₂⊔p₃' | just p₃⊔p₂ | ≈-just p₂⊔p₃≈p₃⊔p₂ + | nothing | nothing | ≈-nothing + rewrite just-injective p₂⊔?p₃=justp₂⊔p₃ + with pathJoin' Ls p₃⊔p₂ p₁ | pathJoin' Ls p₁ p₃⊔p₂ | pathJoin' Ls p₁ p₂⊔p₃ + | pathJoin'-comm {Ls = Ls} p₃⊔p₂ p₁ + | pathJoin'-related {Ls = Ls} p₃ p₂ p₁ p₃⊔p₂ p₃⊔p₂=? p₂⊔p₁=? + | eqPath'-pathJoin'-cong {Ls = Ls} (eqPath'-refl Ls p₁) p₂⊔p₃≈p₃⊔p₂ +... | nothing | nothing | nothing | ≈-nothing | refl | ≈-nothing = refl + 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₂)