From 624332666595ad03af81f37650cc9b0202d9d64e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 25 Jul 2025 15:21:59 +0200 Subject: [PATCH] Prove associativity of meet Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 105 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 105 insertions(+) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index d17c730..b0dba7a 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -517,6 +517,9 @@ pathJoin'-homo-greatest₁ l ls greatest e = eval-subHomo inj₁ (lvJoin (toList pathJoin'-homo-greatest₂ : ∀ {a} (l : Layer a) (ls : Layers a) greatest (e : Expr (Path' ls)) → eval (pathJoin' (add-via-greatest l ls {{greatest}})) (map inj₂ e) ≡ Maybe.map inj₂ (eval (pathJoin' ls) e) pathJoin'-homo-greatest₂ l ls greatest e = eval-subHomo inj₂ (pathJoin' ls) (pathJoin' (add-via-greatest l ls {{greatest}})) e (λ a₁ a₂ → refl) +pathMeet'-homo-least₁ : ∀ {a} (l : Layer a) (ls : Layers a) least (e : Expr (LayerValue l)) → eval (pathMeet' (add-via-least l {{least}} ls)) (map inj₁ e) ≡ Maybe.map inj₁ (eval (lvMeet (toList l)) e) +pathMeet'-homo-least₁ l ls least e = eval-subHomo inj₁ (lvMeet (toList l)) (pathMeet' (add-via-least l {{least}} ls)) e (λ a₁ a₂ → refl) + lvCombine-assoc : ∀ {a} (f : CombineForPLT a) → (∀ plt → PartialAssoc (PartialLatticeType._≈_ plt) (f plt)) → ∀ (L : List (PartialLatticeType a)) → @@ -803,6 +806,108 @@ pathMeet'-comm {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ 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₂ p₁) (inj₁ lv₂) = ≈-just (eqPath'-refl ls p₁) +greatestPath-pathMeet'-identˡ : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls)) + (p : Path' Ls) → + let pᵍ = greatestPath Ls greatest + in lift-≈ (eqPath' Ls) (pathMeet' Ls pᵍ p) (just p) +greatestPath-pathMeet'-identˡ (single (plt ∷⁺ []) ) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ v) + = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (PartialLatticeType.greatest-⊓-identˡ plt hasGreatest v) +greatestPath-pathMeet'-identˡ (add-via-least (plt ∷⁺ []) ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ (inj₁ v)) + = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ + (lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (PartialLatticeType.greatest-⊓-identˡ plt hasGreatest v)) +greatestPath-pathMeet'-identˡ (add-via-least l ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₂ p) = ≈-just (eqPath'-refl ls p) +greatestPath-pathMeet'-identˡ {a = a} (add-via-greatest (plt ∷⁺ []) ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ (inj₁ v)) + with PartialLatticeType._⊓?_ plt (PartialLatticeType.HasGreatestElement.x {a = a} {plt} hasGreatest) v | PartialLatticeType.greatest-⊓-identˡ plt hasGreatest v +... | just vᵍ⊔v | ≈-just vᵍ⊔v≈v = ≈-just vᵍ⊔v≈v +greatestPath-pathMeet'-identˡ (add-via-greatest l ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₂ p) = ≈-just (eqPath'-refl ls p) + +greatestPath-pathMeet'-identʳ : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls)) + (p : Path' Ls) → + let pᵍ = greatestPath Ls greatest + in lift-≈ (eqPath' Ls) (pathMeet' Ls p pᵍ) (just p) +greatestPath-pathMeet'-identʳ Ls greatest p + = IsEquivalence.≈-trans (lift-≈-Equivalence {{eqPath'-Equivalence {Ls = Ls}}}) + (pathMeet'-comm {Ls = Ls} p (greatestPath Ls greatest)) + (greatestPath-pathMeet'-identˡ Ls greatest p) + +pathMeet'-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (eqPath' Ls) (pathMeet' Ls) +pathMeet'-assoc {Ls = single l} lv₁ lv₂ lv₃ = lvMeet-assoc (toList l) lv₁ lv₂ lv₃ +pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) + rewrite pathMeet'-homo-least₁ l ls least (((` lv₁) ∨ (` lv₂)) ∨ (` lv₃)) + rewrite pathMeet'-homo-least₁ l ls least ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃))) + = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-assoc (toList l) lv₁ lv₂ lv₃) +pathMeet'-assoc {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₁ (inj₁ v₂)) (inj₁ (inj₁ v₃)) + with PartialLatticeType._⊓?_ plt v₂ v₃ | IsPartialLattice.HasLeastElement.not-partial (PartialLatticeType.isPartialLattice plt) hasLeast v₂ v₃ +... | just v₂⊓l₃ | (_ , refl) = ≈-just (eqPath'-refl ls p₁) +pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂) (inj₁ lv₃) + = ≈-just (eqPath'-refl ls p₂) +pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₂ p₂) (inj₁ lv₃) + with pathMeet' ls p₁ p₂ +... | just p₁⊓p₂ = ≈-just (eqPath'-refl ls p₁⊓p₂) +... | nothing = ≈-nothing +pathMeet'-assoc {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₁ (inj₁ v₁)) (inj₁ (inj₁ v₂)) (inj₂ p₃) + with PartialLatticeType._⊓?_ plt v₁ v₂ | IsPartialLattice.HasLeastElement.not-partial (PartialLatticeType.isPartialLattice plt) hasLeast v₁ v₂ +... | just _ | (_ , refl) = ≈-just (eqPath'-refl ls p₃) +pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂) (inj₂ p₃) + with pathMeet' ls p₁ p₃ +... | just p₁⊓p₃ = ≈-just (eqPath'-refl ls p₁⊓p₃) +... | nothing = ≈-nothing +pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂) (inj₂ p₃) + with pathMeet' ls p₂ p₃ +... | just p₂⊓p₃ = ≈-just (eqPath'-refl ls p₂⊓p₃) +... | nothing = ≈-nothing +pathMeet'-assoc {Ls = add-via-least l ls} (inj₂ p₁) (inj₂ p₂) (inj₂ p₃) + with pathMeet' ls p₁ p₂ in p₁⊓?p₂=? | pathMeet' ls p₂ p₃ in p₂⊓?p₃=? | pathMeet'-assoc {Ls = ls} p₁ p₂ p₃ +... | just p₁⊓p₂ | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ p₁⊓p₂p₃≈p₁p₂⊓p₃ +... | nothing | nothing | _ = ≈-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 +-- begin dumb: due to annoying nested with-abstractions, we have several written-out cases here +-- for the same inj₁/inj₁/inj₁ combination. +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) + with lvMeet (toList l) lv₁ lv₂ | lvMeet (toList l) lv₂ lv₃ | lvMeet-assoc (toList l) lv₁ lv₂ lv₃ +... | just lv₁⊓lv₂ | just lv₂⊓lv₃ | p₁⊓?p₂p₃≈p₁p₂⊓?p₃ + with lvMeet (toList l) lv₁⊓lv₂ lv₃ | lvMeet (toList l) lv₁ lv₂⊓lv₃ | p₁⊓?p₂p₃≈p₁p₂⊓?p₃ +... | just _ | just _ | ≈-just p₁⊓p₂p₃≈p₁p₂⊓p₃ = ≈-just p₁⊓p₂p₃≈p₁p₂⊓p₃ +... | nothing | nothing | ≈-nothing = ≈-just (eqPath'-refl ls (greatestPath ls greatest)) +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) + | nothing | nothing | _ = ≈-just (eqPath'-refl ls (greatestPath ls greatest)) +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) + | just lv₁⊓lv₂ | nothing | p₁⊓?p₂p₃≈p₁p₂⊓?p₃ + with nothing <- lvMeet (toList l) lv₁⊓lv₂ lv₃ = ≈-just (eqPath'-refl ls (greatestPath ls greatest)) +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) + | nothing | just lv₂⊓lv₃ | p₁⊓?p₂p₃≈p₁p₂⊓?p₃ + with nothing <- lvMeet (toList l) lv₁ lv₂⊓lv₃ = ≈-just (eqPath'-refl ls (greatestPath ls greatest)) +-- end dumb +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₁ lv₂) (inj₁ lv₃) + with lvMeet (toList l) lv₂ lv₃ +... | just _ = ≈-just (eqPath'-refl ls p₁) +... | nothing = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (IsEquivalence.≈-sym (lift-≈-Equivalence {{eqPath'-Equivalence {Ls = ls}}}) (greatestPath-pathMeet'-identʳ ls greatest p₁)) +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂) (inj₁ lv₃) + = ≈-just (eqPath'-refl ls p₂) +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p₂) (inj₁ lv₃) + with pathMeet' ls p₁ p₂ +... | just p₁⊓p₂ = ≈-just (eqPath'-refl ls p₁⊓p₂) +... | nothing = ≈-nothing +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₂ p₃) + with lvMeet (toList l) lv₁ lv₂ +... | just _ = ≈-just (eqPath'-refl ls p₃) +... | nothing = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (greatestPath-pathMeet'-identˡ ls greatest p₃) +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₁ lv₂) (inj₂ p₃) + with pathMeet' ls p₁ p₃ +... | just p₁⊓p₃ = ≈-just (eqPath'-refl ls p₁⊓p₃) +... | nothing = ≈-nothing +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂) (inj₂ p₃) + with pathMeet' ls p₂ p₃ +... | just p₂⊓p₃ = ≈-just (eqPath'-refl ls p₂⊓p₃) +... | nothing = ≈-nothing +pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p₂) (inj₂ p₃) + with pathMeet' ls p₁ p₂ in p₁⊓?p₂=? | pathMeet' ls p₂ p₃ in p₂⊓?p₃=? | pathMeet'-assoc {Ls = ls} p₁ p₂ p₃ +... | just p₁⊓p₂ | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ p₁⊓p₂p₃≈p₁p₂⊓p₃ +... | nothing | nothing | _ = ≈-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 + record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)