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

Prove associativity

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-22 18:05:08 +02:00
parent 6055a79e6a
commit 36ae125e1e
1 changed files with 83 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

83
Lattice/Builder.agda
View File

@ -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₂)