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

Prove idempotence of value combining

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2025-07-05 16:55:11 -07:00
parent fdef8c0a60
commit 7fdbf0397d
1 changed files with 27 additions and 14 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

41
Lattice/Builder.agda
View File

@ -356,16 +356,6 @@ lvCombine-homo₂ plt plts f (e₁ ∨ e₂)
... | just x₁ | nothing = refl ... | just x₁ | nothing = refl
... | nothing | just x₂ = refl ... | nothing | just x₂ = refl
lvCombine-comm : ∀ {a} (f : CombineForPLT a) →
(∀ plt → PartialComm (PartialLatticeType._≈_ plt) (f plt)) →
∀ (L : List (PartialLatticeType a)) →
PartialComm (eqL L) (lvCombine f L)
lvCombine-comm f f-comm L@(plt ∷ plts) lv₁@(inj₁ v₁) (inj₁ v₂)
rewrite lvCombine-homo₁ plt plts f ((` v₁) ∨ (` v₂)) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-comm plt v₁ v₂)
lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-comm f f-comm plts lv₁ lv₂)
lvCombine-comm f f-comm (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = ≈-nothing
lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = ≈-nothing
lvCombine-assoc : ∀ {a} (f : CombineForPLT a) → lvCombine-assoc : ∀ {a} (f : CombineForPLT a) →
(∀ plt → PartialAssoc (PartialLatticeType._≈_ plt) (f plt)) → (∀ plt → PartialAssoc (PartialLatticeType._≈_ plt) (f plt)) →
∀ (L : List (PartialLatticeType a)) → ∀ (L : List (PartialLatticeType a)) →
@ -397,18 +387,41 @@ lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) (inj₂
rewrite lvCombine-homo₂ plt plts f ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃))) rewrite lvCombine-homo₂ plt plts f ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃)))
= lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-assoc f f-assoc plts lv₁ lv₂ lv₃) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-assoc f f-assoc plts lv₁ lv₂ lv₃)
lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvJoin L) lvCombine-comm : ∀ {a} (f : CombineForPLT a) →
lvJoin-comm = lvCombine-comm PartialLatticeType._⊔?_ PartialLatticeType.⊔-comm (∀ plt → PartialComm (PartialLatticeType._≈_ plt) (f plt)) →
∀ (L : List (PartialLatticeType a)) →
PartialComm (eqL L) (lvCombine f L)
lvCombine-comm f f-comm L@(plt ∷ plts) lv₁@(inj₁ v₁) (inj₁ v₂)
rewrite lvCombine-homo₁ plt plts f ((` v₁) ∨ (` v₂)) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-comm plt v₁ v₂)
lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-comm f f-comm plts lv₁ lv₂)
lvCombine-comm f f-comm (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = ≈-nothing
lvCombine-comm f f-comm (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = ≈-nothing
lvCombine-idemp : ∀ {a} (f : CombineForPLT a) →
(∀ plt → PartialIdemp (PartialLatticeType._≈_ plt) (f plt)) →
∀ (L : List (PartialLatticeType a)) →
PartialIdemp (eqL L) (lvCombine f L)
lvCombine-idemp f f-idemp (plt ∷ plts) (inj₁ v) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-idemp plt v)
lvCombine-idemp f f-idemp (plt ∷ plts) (inj₂ lv) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (lvCombine-idemp f f-idemp plts lv)
lvJoin-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvJoin L) lvJoin-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvJoin L)
lvJoin-assoc = lvCombine-assoc PartialLatticeType._⊔?_ PartialLatticeType.⊔-assoc lvJoin-assoc = lvCombine-assoc PartialLatticeType._⊔?_ PartialLatticeType.⊔-assoc
lvMeet-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvMeet L) lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvJoin L)
lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-comm lvJoin-comm = lvCombine-comm PartialLatticeType._⊔?_ PartialLatticeType.⊔-comm
lvJoin-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvJoin L)
lvJoin-idemp = lvCombine-idemp PartialLatticeType._⊔?_ PartialLatticeType.⊔-idemp
lvMeet-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvMeet L) lvMeet-assoc : ∀ {a} (L : List (PartialLatticeType a)) → PartialAssoc (eqL L) (lvMeet L)
lvMeet-assoc = lvCombine-assoc PartialLatticeType._⊓?_ PartialLatticeType.⊓-assoc lvMeet-assoc = lvCombine-assoc PartialLatticeType._⊓?_ PartialLatticeType.⊓-assoc
lvMeet-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvMeet L)
lvMeet-comm = lvCombine-comm PartialLatticeType._⊓?_ PartialLatticeType.⊓-comm
lvMeet-idemp : ∀ {a} (L : List (PartialLatticeType a)) → PartialIdemp (eqL L) (lvMeet L)
lvMeet-idemp = lvCombine-idemp PartialLatticeType._⊓?_ PartialLatticeType.⊓-idemp
pathJoin'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathJoin' Ls) pathJoin'-comm : ∀ {a} {Ls : Layers a} → PartialComm (eqPath' Ls) (pathJoin' Ls)
pathJoin'-comm {Ls = single l} lv₁ lv₂ = lvJoin-comm (toList l) lv₁ lv₂ pathJoin'-comm {Ls = single l} lv₁ lv₂ = lvJoin-comm (toList l) lv₁ lv₂
pathJoin'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-comm (toList l) lv₁ lv₂) pathJoin'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-comm (toList l) lv₁ lv₂)