From 36ae125e1e30d3dbb22ed72d7ed152e7ed18e326 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Tue, 22 Jul 2025 18:05:08 +0200 Subject: [PATCH] Prove associativity Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 83 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 83 insertions(+) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 4e689a2..62ebae7 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -694,6 +694,89 @@ pathJoin'-related' {Ls = Ls} p₁ p₂ p₃ p₂⊔p₃ p₂⊔?p₃=justp₂⊔ | eqPath'-pathJoin'-cong {Ls = Ls} (eqPath'-refl Ls p₁) p₂⊔p₃≈p₃⊔p₂ ... | nothing | nothing | nothing | ≈-nothing | refl | ≈-nothing = refl + +-- fact: pathJoin' Ls p₃ p₂ ≡ just p₃⊔p₂ + +pathJoin'-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (eqPath' Ls) (pathJoin' Ls) +pathJoin'-assoc {Ls = single l} lv₁ lv₂ lv₃ = lvJoin-assoc (toList l) lv₁ lv₂ lv₃ +pathJoin'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) + rewrite pathJoin'-homo-least₁ l ls least (((` lv₁) ∨ (` lv₂)) ∨ (` lv₃)) + rewrite pathJoin'-homo-least₁ l ls least ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃))) + = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-assoc (toList l) lv₁ lv₂ lv₃) +pathJoin'-assoc {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂) (inj₁ lv₃) + with lvJoin (toList l) lv₂ lv₃ +... | m@(just lv₂⊔lv₃) = ≈-just (eqLv-refl l lv₂⊔lv₃) +... | nothing = ≈-nothing +pathJoin'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂) (inj₁ lv₃) + = lift-≈-map inj₁ _ _ (λ _ _ x → x) + (lvJoin (toList l) lv₁ lv₃) + (lvJoin (toList l) lv₁ lv₃) + (IsEquivalence.≈-refl (lift-≈-Equivalence {{eqLv-Equivalence {L = l}}})) +pathJoin'-assoc {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂) (inj₁ lv₃@(inj₁ v₃)) + with pathJoin' ls p₁ p₂ +... | just _ = ≈-just (eqLv-refl l lv₃) +... | nothing = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ + (lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (PartialLatticeType.least-⊔-identˡ plt hasLeast v₃)) +pathJoin'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₁ lv₂) (inj₂ p₃) + with lvJoin (toList l) lv₁ lv₂ +... | m@(just lv₁⊔lv₂) = ≈-just (eqLv-refl l lv₁⊔lv₂) +... | nothing = ≈-nothing +pathJoin'-assoc {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂) (inj₂ p₃) + = ≈-just (eqLv-refl l lv₂) +pathJoin'-assoc {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₁ lv₁@(inj₁ v₁)) (inj₂ p₂) (inj₂ p₃) + with pathJoin' ls p₂ p₃ +... | just _ = ≈-just (eqLv-refl l lv₁) +... | nothing = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ + (lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (IsEquivalence.≈-sym (lift-≈-Equivalence {{PartialLatticeType.≈-equiv plt}}) (PartialLatticeType.least-⊔-identʳ plt hasLeast v₁))) +pathJoin'-assoc {Ls = Ls@(add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls)} (inj₂ p₁) (inj₂ p₂) (inj₂ p₃) + with pathJoin' ls p₁ p₂ in p₁⊔?p₂=? | pathJoin' ls p₂ p₃ in p₂⊔?p₃=? + | pathJoin'-assoc {Ls = ls} p₁ p₂ p₃ + | pathJoin'-related {Ls = ls} p₁ p₂ p₃ + | pathJoin'-related' {Ls = ls} p₁ p₂ p₃ +... | nothing | just p₂⊔p₃ | _ | _ | refl⇒refl⇒p₁⊔p₂p₃=nothing + rewrite refl⇒refl⇒p₁⊔p₂p₃=nothing p₂⊔p₃ refl refl + = ≈-just (eqPath'-refl Ls (inj₁ (inj₁ (PartialLatticeType.HasLeastElement.x {_} {plt} hasLeast)))) +... | just p₁⊔p₂ | nothing | _ | refl⇒refl⇒p₁p₂⊔p₃=nothing | _ + rewrite refl⇒refl⇒p₁p₂⊔p₃=nothing p₁⊔p₂ refl refl + = ≈-just (eqPath'-refl Ls (inj₁ (inj₁ (PartialLatticeType.HasLeastElement.x {_} {plt} hasLeast)))) +... | nothing | nothing | _ | _ | _ = ≈-just (eqPath'-refl Ls (inj₁ (inj₁ (PartialLatticeType.HasLeastElement.x {_} {plt} hasLeast)))) +... | just p₁⊔p₂ | just p₂⊔p₃ | p₁⊔p₂p₃≈?p₁p₂⊔p₃ | _ | _ + with pathJoin' ls p₁⊔p₂ p₃ | pathJoin' ls p₁ p₂⊔p₃ | p₁⊔p₂p₃≈?p₁p₂⊔p₃ +... | just p₁⊔p₂p₃ | just p₁p₂⊔p₃ | ≈-just p₁⊔p₂p₃≈p₁p₂⊔p₃ = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (≈-just p₁⊔p₂p₃≈p₁p₂⊔p₃) +... | nothing | nothing | ≈-nothing = ≈-just (eqPath'-refl Ls (inj₁ (inj₁ (PartialLatticeType.HasLeastElement.x {_} {plt} hasLeast)))) +pathJoin'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃) + rewrite pathJoin'-homo-greatest₁ l ls greatest (((` lv₁) ∨ (` lv₂)) ∨ (` lv₃)) + rewrite pathJoin'-homo-greatest₁ l ls greatest ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃))) + = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-assoc (toList l) lv₁ lv₂ lv₃) +pathJoin'-assoc {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂) (inj₁ lv₃) + with lvJoin (toList l) lv₂ lv₃ +... | m@(just lv₂⊔lv₃) = ≈-just (eqLv-refl l lv₂⊔lv₃) +... | nothing = ≈-nothing +pathJoin'-assoc {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂) (inj₁ lv₃) + = lift-≈-map inj₁ _ _ (λ _ _ x → x) + (lvJoin (toList l) lv₁ lv₃) + (lvJoin (toList l) lv₁ lv₃) + (IsEquivalence.≈-refl (lift-≈-Equivalence {{eqLv-Equivalence {L = l}}})) +pathJoin'-assoc {Ls = add-via-greatest l ls {{greatest = greatest}}} (inj₂ p₁) (inj₂ p₂) (inj₁ lv₃) + with pathJoin' ls p₁ p₂ in p₁⊔?p₂=? +... | just p₁⊔p₂ = ≈-just (eqLv-refl l lv₃) +... | nothing = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₁ p₂ greatest p₁⊔?p₂=?) +pathJoin'-assoc {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₁ lv₂) (inj₂ p₃) + with lvJoin (toList l) lv₁ lv₂ +... | m@(just lv₁⊔lv₂) = ≈-just (eqLv-refl l lv₁⊔lv₂) +... | nothing = ≈-nothing +pathJoin'-assoc {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂) (inj₂ p₃) + = ≈-just (eqLv-refl l lv₂) +pathJoin'-assoc {Ls = add-via-greatest l ls {{greatest = greatest}}} (inj₁ lv₁) (inj₂ p₂) (inj₂ p₃) + with pathJoin' ls p₂ p₃ in p₂⊔?p₃=? +... | just p₂⊔p₃ = ≈-just (eqLv-refl l lv₁) +... | nothing = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₂ p₃ greatest p₂⊔?p₃=?) +pathJoin'-assoc {Ls = add-via-greatest l ls {{greatest = greatest}}} (inj₂ p₁) (inj₂ p₂) (inj₂ p₃) + with pathJoin' ls p₁ p₂ in p₁⊔?p₂=? | pathJoin' ls p₂ p₃ in p₂⊔?p₃=? | pathJoin'-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 | _ | _ = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₁ p₂ greatest p₁⊔?p₂=?) +... | _ | nothing | _ = ⊥-elim (pathJoin'-greatest-total {Ls = ls} p₂ p₃ greatest 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₂)