DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
6055a79e6a
agda-spa/Lattice/Builder.agda
Danila Fedorin 6055a79e6a Prove a side lemma about nothing/just 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-07-22 18:04:53 +02:00

734 lines
48 KiB
Agda
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

module Lattice.Builder where
open import Lattice
open import Equivalence
open import Data.Maybe as Maybe using (Maybe; just; nothing; _>>=_; maybe)
open import Data.Maybe.Properties using (just-injective)
open import Data.Unit using (⊤; tt)
open import Data.List.NonEmpty using (List⁺; tail; toList) renaming (_∷_ to _∷⁺_)
open import Data.List using (List; _∷_; [])
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Data.Product using (Σ; _,_)
open import Data.Empty using (⊥; ⊥-elim)
open import Relation.Binary.PropositionalEquality as Eq using (_≡_; refl; sym; trans; cong; subst)
open import Agda.Primitive using (lsuc; Level) renaming (_⊔_ to _⊔ℓ_)
maybe-injection : ∀ {a} {A : Set a} (x : A) → just x ≡ nothing → ⊥
maybe-injection x ()
data lift-≈ {a} {A : Set a} (_≈_ : A → A → Set a) : Maybe A → Maybe A → Set a where
≈-just : ∀ {a₁ a₂ : A} → a₁ ≈ a₂ → lift-≈ _≈_ (just a₁) (just a₂)
≈-nothing : lift-≈ _≈_ nothing nothing
lift-≈-map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B)
(_≈ᵃ_ : A → A → Set a) (_≈ᵇ_ : B → B → Set b) →
(∀ a₁ a₂ → a₁ ≈ᵃ a₂ → f a₁ ≈ᵇ f a₂) →
∀ m₁ m₂ → lift-≈ _≈ᵃ_ m₁ m₂ → lift-≈ _≈ᵇ_ (Maybe.map f m₁) (Maybe.map f m₂)
lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ (just a₁) (just a₂) (≈-just a₁≈a₂) = ≈-just (≈ᵃ→≈ᵇ a₁ a₂ a₁≈a₂)
lift-≈-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ→≈ᵇ nothing nothing ≈-nothing = ≈-nothing
instance
lift-≈-Equivalence : ∀ {a} {A : Set a} {_≈_ : A → A → Set a} {{isEquivalence : IsEquivalence A _≈_}} → IsEquivalence (Maybe A) (lift-≈ _≈_)
lift-≈-Equivalence {{isEquivalence}} = record
{ ≈-trans =
(λ { (≈-just a₁≈a₂) (≈-just a₂≈a₃) → ≈-just (IsEquivalence.≈-trans isEquivalence a₁≈a₂ a₂≈a₃)
; ≈-nothing ≈-nothing → ≈-nothing
})
; ≈-sym =
(λ { (≈-just a₁≈a₂) → ≈-just (IsEquivalence.≈-sym isEquivalence a₁≈a₂)
; ≈-nothing → ≈-nothing
})
; ≈-refl = λ { {just a} → ≈-just (IsEquivalence.≈-refl isEquivalence)
; {nothing} → ≈-nothing
}
}
PartialCong : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialCong {a} {A} _≈_ _⊗_ = ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → lift-≈ _≈_ (a₁ ⊗ a₃) (a₂ ⊗ a₄)
PartialAssoc : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialAssoc {a} {A} _≈_ _⊗_ = ∀ (x y z : A) → lift-≈ _≈_ ((x ⊗ y) >>= (_⊗ z)) ((y ⊗ z) >>= (x ⊗_))
PartialComm : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialComm {a} {A} _≈_ _⊗_ = ∀ (x y : A) → lift-≈ _≈_ (x ⊗ y) (y ⊗ x)
PartialIdemp : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗_ : A → A → Maybe A) → Set a
PartialIdemp {a} {A} _≈_ _⊗_ = ∀ (x : A) → lift-≈ _≈_ (x ⊗ x) (just x)
data Trivial a : Set a where
instance
mkTrivial : Trivial a
data Empty a : Set a where
record IsPartialSemilattice {a} {A : Set a}
(_≈_ : A → A → Set a)
(_⊔?_ : A → A → Maybe A) : Set a where
_≈?_ : Maybe A → Maybe A → Set a
_≈?_ = lift-≈ _≈_
_≼_ : A → A → Set a
_≼_ x y = (x ⊔? y) ≈? (just y)
field
≈-equiv : IsEquivalence A _≈_
≈-⊔-cong : PartialCong _≈_ _⊔?_
⊔-assoc : PartialAssoc _≈_ _⊔?_
⊔-comm : PartialComm _≈_ _⊔?_
⊔-idemp : PartialIdemp _≈_ _⊔?_
open IsEquivalence ≈-equiv public
open IsEquivalence (lift-≈-Equivalence {{≈-equiv}}) public using ()
renaming (≈-trans to ≈?-trans; ≈-sym to ≈?-sym; ≈-refl to ≈?-refl)
≈-≼-cong : ∀ {a₁ a₂ a₃ a₄} → a₁ ≈ a₂ → a₃ ≈ a₄ → a₁ ≼ a₃ → a₂ ≼ a₄
≈-≼-cong {a₁} {a₂} {a₃} {a₄} a₁≈a₂ a₃≈a₄ a₁≼a₃ = ≈?-trans (≈?-trans (≈?-sym (≈-⊔-cong a₁≈a₂ a₃≈a₄)) a₁≼a₃) (≈-just a₃≈a₄)
-- curious: similar property (properties?) to partial commutative monoids (PCMs)
-- from Iris.
≼-partialˡ : ∀ {a a₁ a₂} → a₁ ≼ a₂ → (a ⊔? a₁) ≡ nothing → (a ⊔? a₂) ≡ nothing
≼-partialˡ {a} {a₁} {a₂} a₁≼a₂ a⊔a₁≡nothing
with a₁ ⊔? a₂ | a₁≼a₂ | a ⊔? a₁ | a⊔a₁≡nothing | ⊔-assoc a a₁ a₂
... | just a₁⊔a₂ | ≈-just a₁⊔a₂≈a₂ | nothing | refl | aa₁⊔a₂≈a⊔a₁a₂
with a ⊔? a₁⊔a₂ | aa₁⊔a₂≈a⊔a₁a₂ | a ⊔? a₂ | ≈-⊔-cong (≈-refl {a = a}) a₁⊔a₂≈a₂
... | nothing | ≈-nothing | nothing | ≈-nothing = refl
≼-partialʳ : ∀ {a₁ a₂ a} → a₁ ≼ a₂ → (a₁ ⊔? a) ≡ nothing → (a₂ ⊔? a) ≡ nothing
≼-partialʳ {a₁} {a₂} {a} a₁≼a₂ a₁⊔a≡nothing
with a₁ ⊔? a | a ⊔? a₁ | a₁⊔a≡nothing | ⊔-comm a₁ a | ≼-partialˡ {a} {a₁} {a₂} a₁≼a₂
... | nothing | nothing | refl | ≈-nothing | refl⇒a⊔a₂=nothing
with a₂ ⊔? a | a ⊔? a₂ | ⊔-comm a₂ a | refl⇒a⊔a₂=nothing refl
... | nothing | nothing | ≈-nothing | refl = refl
≼-refl : ∀ (x : A) → x ≼ x
≼-refl x = ⊔-idemp x
≼-refl' : ∀ {a₁ a₂ : A} → a₁ ≈ a₂ → a₁ ≼ a₂
≼-refl' {a₁} {a₂} a₁≈a₂ = ≈-≼-cong ≈-refl a₁≈a₂ (≼-refl a₁)
x⊔?x≼x : ∀ (x : A) → maybe (λ x⊔x → x⊔x ≼ x) (Empty a) (x ⊔? x)
x⊔?x≼x x
with x ⊔? x | ⊔-idemp x
... | just x⊔x | ≈-just x⊔x≈x = ≈-≼-cong (≈-sym x⊔x≈x) ≈-refl (≼-refl x)
x≼x⊔?y : ∀ (x y : A) → maybe (λ x⊔y → x ≼ x⊔y) (Trivial a) (x ⊔? y)
x≼x⊔?y x y
with x ⊔? y in x⊔?y= | x ⊔? x | ⊔-idemp x | ⊔-assoc x x y | x⊔?x≼x x
... | nothing | _ | _ | _ | _ = mkTrivial
... | just x⊔y | just x⊔x | ≈-just x⊔x≈x | ⊔-assoc-xxy | x⊔x≼x
with x⊔x ⊔? y in xx⊔?y= | x ⊔? x⊔y
... | nothing | nothing =
⊥-elim (maybe-injection _ (trans (sym x⊔?y=) (≼-partialʳ x⊔x≼x xx⊔?y=)))
... | 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
x-absorbˡ : (a : A) → (x ⊔? a) ≈? just x
x-absorbʳ : (a : A) → (a ⊔? x) ≈? just x
x-absorbʳ a = ≈?-trans (⊔-comm a x) (x-absorbˡ a)
not-partial : ∀ (a₁ a₂ : A) → Σ A (λ a₃ → (a₁ ⊔? a₂) ≡ just a₃)
not-partial a₁ a₂
with a₁ ⊔? a₂ | ≼-partialˡ {a = a₁} (x-absorbʳ a₂)
... | just a₁⊔a₂ | _ = (a₁⊔a₂ , refl)
... | nothing | refl⇒a₁⊔?x=nothing
with a₁ ⊔? x | refl⇒a₁⊔?x=nothing refl | x-absorbʳ a₁
... | nothing | refl | ()
record IsPartialLattice {a} {A : Set a}
(_≈_ : A → A → Set a)
(_⊔?_ : A → A → Maybe A)
(_⊓?_ : A → A → Maybe A) : Set a where
field
{{partialJoinSemilattice}} : IsPartialSemilattice _≈_ _⊔?_
{{partialMeetSemilattice}} : IsPartialSemilattice _≈_ _⊓?_
absorb-⊔-⊓ : (x y : A) → maybe (λ x⊓y → lift-≈ _≈_ (x ⊔? x⊓y) (just x)) (Trivial _) (x ⊓? y)
absorb-⊓-⊔ : (x y : A) → maybe (λ x⊔y → lift-≈ _≈_ (x ⊓? x⊔y) (just x)) (Trivial _) (x ⊔? y)
open IsPartialSemilattice partialJoinSemilattice
renaming (HasAbsorbingElement to HasGreatestElement)
public
open IsPartialSemilattice partialMeetSemilattice using ()
renaming
( HasAbsorbingElement to HasLeastElement
; ≈-⊔-cong to ≈-⊓-cong
; ⊔-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
record PartialLattice {a} (A : Set a) : Set (lsuc a) where
field
_≈_ : A → A → Set a
_⊔?_ : A → A → Maybe A
_⊓?_ : A → A → Maybe A
{{isPartialLattice}} : IsPartialLattice _≈_ _⊔?_ _⊓?_
open IsPartialLattice isPartialLattice public
greatest-⊓-identʳ : ∀ (le : HasGreatestElement) (x : A) →
(x ⊓? HasGreatestElement.x le) ≈? (just x)
greatest-⊓-identʳ le x
with x ⊔? (HasGreatestElement.x le) | HasGreatestElement.x-absorbʳ le x | absorb-⊓-⊔ x (HasGreatestElement.x le)
... | just x⊔greatest | ≈-just x⊔greatest≈greatest | x⊓xgreatest≈?x = ≈?-trans (≈?-sym (≈-⊓-cong (≈-refl {a = x}) x⊔greatest≈greatest)) x⊓xgreatest≈?x
greatest-⊓-identˡ : ∀ (le : HasGreatestElement) (x : A) →
(HasGreatestElement.x le ⊓? x) ≈? (just x)
greatest-⊓-identˡ le x = ≈?-trans (⊓-comm (HasGreatestElement.x le) x) (greatest-⊓-identʳ le x)
least-⊔-identʳ : ∀ (le : HasLeastElement) (x : A) →
(x ⊔? HasLeastElement.x le) ≈? (just x)
least-⊔-identʳ le x
with x ⊓? (HasLeastElement.x le) | HasLeastElement.x-absorbʳ le x | absorb-⊔-⊓ x (HasLeastElement.x le)
... | just x⊓least | ≈-just x⊓least≈least | x⊔xleast≈?x = ≈?-trans (≈?-sym (≈-⊔-cong (≈-refl {a = x}) x⊓least≈least)) x⊔xleast≈?x
least-⊔-identˡ : ∀ (le : HasLeastElement) (x : A) →
(HasLeastElement.x le ⊔? x) ≈? (just x)
least-⊔-identˡ le x = ≈?-trans (⊔-comm (HasLeastElement.x le) x) (least-⊔-identʳ le x)
record PartialLatticeType (a : Level) : Set (lsuc a) where
field
EltType : Set a
{{partialLattice}} : PartialLattice EltType
open PartialLattice partialLattice public
Layer : (a : Level) → Set (lsuc a)
Layer a = List⁺ (PartialLatticeType a)
data LayerLeast {a} : Layer a → Set (lsuc a) where
instance
MkLayerLeast : {T : Set a}
{{ partialLattice : PartialLattice T }}
{{ hasLeast : PartialLattice.HasLeastElement partialLattice }} →
LayerLeast (record { EltType = T; partialLattice = partialLattice } ∷⁺ [])
data LayerGreatest {a} : Layer a → Set (lsuc a) where
instance
MkLayerGreatest : {T : Set a}
{{ partialLattice : PartialLattice T }}
{{ hasGreatest : PartialLattice.HasGreatestElement partialLattice }} →
LayerGreatest (record { EltType = T; partialLattice = partialLattice } ∷⁺ [])
interleaved mutual
data Layers a : Set (lsuc a)
head : ∀ {a} → Layers a → Layer a
data Layers where
single : Layer a → Layers a
add-via-least : (l : Layer a) {{ least : LayerLeast l }} (ls : Layers a) → Layers a
add-via-greatest : (l : Layer a) (ls : Layers a) {{ greatest : LayerGreatest (head ls) }} → Layers a
head (single l) = l
head (add-via-greatest l _) = l
head (add-via-least l _) = l
ListValue : ∀ {a} → List (PartialLatticeType a) → Set a
ListValue [] = Empty _
ListValue (plt ∷ plts) = PartialLatticeType.EltType plt ⊎ ListValue plts
-- Define LayerValue and Path' as functions to avoid increasing the universe level.
-- Path' in particular needs to be at the same level as the other lattices
-- in the builder to ensure composability.
LayerValue : ∀ {a} → Layer a → Set a
LayerValue l⁺ = ListValue (toList l⁺)
Path' : ∀ {a} → Layers a → Set a
Path' (single l) = LayerValue l
Path' (add-via-least l ls) = LayerValue l ⊎ Path' ls
Path' (add-via-greatest l ls) = LayerValue l ⊎ Path' ls
record Path {a} (Ls : Layers a) : Set a where
constructor MkPath
field path : Path' Ls
valueAtHead : ∀ {a} (ls : Layers a) (lv : LayerValue (head ls)) → Path' ls
valueAtHead (single _) lv = lv
valueAtHead (add-via-least _ _) lv = inj₁ lv
valueAtHead (add-via-greatest _ _) lv = inj₁ lv
CombineForPLT : ∀ a → Set (lsuc a)
CombineForPLT a = ∀ (plt : PartialLatticeType a) → PartialLatticeType.EltType plt → PartialLatticeType.EltType plt → Maybe (PartialLatticeType.EltType plt)
lvCombine : ∀ {a} (f : CombineForPLT a) (l : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue l) → Maybe (ListValue l)
lvCombine _ [] _ _ = nothing
lvCombine f (plt ∷ plts) (inj₁ v₁) (inj₁ v₂) = Maybe.map inj₁ (f plt v₁ v₂)
lvCombine f (_ ∷ plts) (inj₂ lv₁) (inj₂ lv₂) = Maybe.map inj₂ (lvCombine f plts lv₁ lv₂)
lvCombine _ (_ ∷ plts) (inj₁ _) (inj₂ _) = nothing
lvCombine _ (_ ∷ plts) (inj₂ _) (inj₁ _) = nothing
lvJoin : ∀ {a} (l : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue l) → Maybe (ListValue l)
lvJoin = lvCombine PartialLatticeType._⊔?_
lvMeet : ∀ {a} (l : List (PartialLatticeType a)) (lv₁ lv₂ : ListValue l) → Maybe (ListValue l)
lvMeet = lvCombine PartialLatticeType._⊓?_
pathJoin' : ∀ {a} (Ls : Layers a) (p₁ p₂ : Path' Ls) → Maybe (Path' Ls)
pathJoin' (single l) lv₁ lv₂ = lvJoin (toList l) lv₁ lv₂
pathJoin' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = Maybe.map inj₁ (lvJoin (toList l) lv₁ lv₂)
pathJoin' (add-via-least l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₁ lv₁)
pathJoin' (add-via-least l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₁ lv₂)
pathJoin' (add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls) (inj₂ p₁) (inj₂ p₂)
with pathJoin' ls p₁ p₂
... | just p = just (inj₂ p)
... | nothing = just (inj₁ (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasLeast)))
pathJoin' (add-via-greatest l ls) (inj₁ lv₁) (inj₁ lv₂) = Maybe.map inj₁ (lvJoin (toList l) lv₁ lv₂)
pathJoin' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₁ lv₁)
pathJoin' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₁ lv₂)
pathJoin' (add-via-greatest l ls {{greatest}}) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathJoin' ls p₁ p₂) -- not our job to provide the least element here. If there was a "greatest" there, recursion would've found it (?)
pathMeet' : ∀ {a} (Ls : Layers a) (p₁ p₂ : Path' Ls) → Maybe (Path' Ls)
pathMeet' (single l) lv₁ lv₂ = lvMeet (toList l) lv₁ lv₂
pathMeet' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = Maybe.map inj₁ (lvMeet (toList l) lv₁ lv₂)
pathMeet' (add-via-least l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₂ p₂)
pathMeet' (add-via-least l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₂ p₁)
pathMeet' (add-via-least l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathMeet' ls p₁ p₂)
pathMeet' (add-via-greatest l ls {{greatest}}) (inj₁ lv₁) (inj₁ lv₂)
with lvMeet (toList l) lv₁ lv₂
... | just lv = just (inj₁ lv)
... | nothing
with head ls | greatest | valueAtHead ls
... | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
= just (inj₂ (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))))
pathMeet' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = just (inj₂ p₂)
pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = just (inj₂ p₁)
pathMeet' (add-via-greatest l ls) (inj₂ p₁) (inj₂ p₂) = Maybe.map inj₂ (pathMeet' ls p₁ p₂)
eqL : ∀ {a} (L : List (PartialLatticeType a)) → ListValue L → ListValue L → Set a
eqL [] ()
eqL (plt ∷ plts) (inj₁ v₁ ) (inj₁ v₂) = PartialLattice._≈_ (PartialLatticeType.partialLattice plt) v₁ v₂
eqL (plt ∷ plts) (inj₂ v₁ ) (inj₂ v₂) = eqL plts v₁ v₂
eqL (plt ∷ plts) (inj₁ _) (inj₂ _) = Empty _
eqL (plt ∷ plts) (inj₂ _) (inj₁ _) = Empty _
eqL-trans : ∀ {a} (L : List (PartialLatticeType a)) {lv₁ lv₂ lv₃ : ListValue L} → eqL L lv₁ lv₂ → eqL L lv₂ lv₃ → eqL L lv₁ lv₃
eqL-trans [] {()}
eqL-trans (plt ∷ plts) {inj₁ v₁} {inj₁ v₂} {inj₁ v₃} v₁≈v₂ v₂≈v₃ = PartialLatticeType.≈-trans plt v₁≈v₂ v₂≈v₃
eqL-trans (plt ∷ plts) {inj₂ lv₁} {inj₂ lv₂} {inj₂ lv₃} lv₁≈lv₂ lv₂≈lv₃ = eqL-trans plts lv₁≈lv₂ lv₂≈lv₃
eqL-sym : ∀ {a} (L : List (PartialLatticeType a)) {lv₁ lv₂ : ListValue L} → eqL L lv₁ lv₂ → eqL L lv₂ lv₁
eqL-sym [] {()}
eqL-sym (plt ∷ plts) {inj₁ v₁} {inj₁ v₂} v₁≈v₂ = PartialLatticeType.≈-sym plt v₁≈v₂
eqL-sym (plt ∷ plts) {inj₂ lv₁} {inj₂ lv₂} lv₁≈lv₂ = eqL-sym plts lv₁≈lv₂
eqL-refl : ∀ {a} (L : List (PartialLatticeType a)) (lv : ListValue L) → eqL L lv lv
eqL-refl [] ()
eqL-refl (plt ∷ plts) (inj₁ v) = IsEquivalence.≈-refl (PartialLatticeType.≈-equiv plt)
eqL-refl (plt ∷ plts) (inj₂ v) = eqL-refl plts v
instance
eqL-Equivalence : ∀ {a} {L : List (PartialLatticeType a)} → IsEquivalence (ListValue L) (eqL L)
eqL-Equivalence {L = L} = record
{ ≈-trans = eqL-trans L
; ≈-sym = eqL-sym L
; ≈-refl = λ {lv} → eqL-refl L lv
}
eqL-lvCombine-cong : ∀ {a} (f : CombineForPLT a) →
(∀ plt → PartialCong (PartialLatticeType._≈_ plt) (f plt)) →
∀ (L : List (PartialLatticeType a)) →
PartialCong (eqL L) (lvCombine f L)
eqL-lvCombine-cong f f-Cong [] {()}
eqL-lvCombine-cong f f-Cong (plt ∷ plts) {inj₁ v₁} {inj₁ v₂} {inj₁ v₃} {inj₁ v₄} v₁≈v₂ v₃≈v₄
with f plt v₁ v₃ | f plt v₂ v₄ | f-Cong plt v₁≈v₂ v₃≈v₄
... | just _ | just _ | ≈-just v₁⊗v₃≈v₂⊗v₄ = ≈-just v₁⊗v₃≈v₂⊗v₄
... | nothing | nothing | ≈-nothing = ≈-nothing
eqL-lvCombine-cong f f-Cong (plt ∷ plts) {inj₂ lv₁} {inj₂ lv₂} {inj₁ v₃} {inj₁ v₄} _ _ = ≈-nothing
eqL-lvCombine-cong f f-Cong (plt ∷ plts) {inj₁ v₁} {inj₁ v₂} {inj₂ lv₃} {inj₂ lv₄} _ _ = ≈-nothing
eqL-lvCombine-cong f f-Cong (plt ∷ plts) {inj₂ lv₁} {inj₂ lv₂} {inj₂ lv₃} {inj₂ lv₄} lv₁≈lv₂ lv₃≈lv₄
with lvCombine f plts lv₁ lv₃ | lvCombine f plts lv₂ lv₄ | eqL-lvCombine-cong f f-Cong plts {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
... | just _ | just _ | ≈-just lv₁⊗v₃≈v₂⊗v₄ = ≈-just lv₁⊗v₃≈v₂⊗v₄
... | nothing | nothing | ≈-nothing = ≈-nothing
eqLv : ∀ {a} (L : Layer a) → LayerValue L → LayerValue L → Set a
eqLv L = eqL (toList L)
eqLv-trans : ∀ {a} (L : Layer a) → {lv₁ lv₂ lv₃ : LayerValue L} → eqLv L lv₁ lv₂ → eqLv L lv₂ lv₃ → eqLv L lv₁ lv₃
eqLv-trans L {lv₁} {lv₂} {lv₃} = eqL-trans (toList L) {lv₁} {lv₂} {lv₃}
eqLv-sym : ∀ {a} (L : Layer a) → {lv₁ lv₂ : LayerValue L} → eqLv L lv₁ lv₂ → eqLv L lv₂ lv₁
eqLv-sym L {lv₁} {lv₂} = eqL-sym (toList L) {lv₁} {lv₂}
eqLv-refl : ∀ {a} (L : Layer a) → (lv : LayerValue L) → eqLv L lv lv
eqLv-refl L = eqL-refl (toList L)
instance
eqLv-Equivalence : ∀ {a} {L : Layer a} → IsEquivalence (LayerValue L) (eqLv L)
eqLv-Equivalence {L = L} = record
{ ≈-trans = λ {lv₁} {lv₂} {lv₃} → eqLv-trans L {lv₁} {lv₂} {lv₃}
; ≈-sym = λ {lv₁} {lv₂} → eqLv-sym L {lv₁} {lv₂}
; ≈-refl = λ {lv} → eqLv-refl L lv
}
eqLv-lvCombine-cong : ∀ {a} (f : CombineForPLT a) →
(∀ plt → PartialCong (PartialLatticeType._≈_ plt) (f plt)) →
∀ (L : Layer a) →
PartialCong (eqLv L) (lvCombine f (toList L))
eqLv-lvCombine-cong f f-Cong L {lv₁} {lv₂} {lv₃} {lv₄} = eqL-lvCombine-cong f f-Cong (toList L) {lv₁} {lv₂} {lv₃} {lv₄}
eqLv-lvJoin-cong : ∀ {a} (L : Layer a) → PartialCong (eqLv L) (lvJoin (toList L))
eqLv-lvJoin-cong = eqLv-lvCombine-cong PartialLatticeType._⊔?_ PartialLatticeType.≈-⊔-cong
eqLv-lvMeet-cong : ∀ {a} (L : Layer a) → PartialCong (eqLv L) (lvMeet (toList L))
eqLv-lvMeet-cong = eqLv-lvCombine-cong PartialLatticeType._⊓?_ PartialLatticeType.≈-⊓-cong
eqPath' : ∀ {a} (Ls : Layers a) → Path' Ls → Path' Ls → Set a
eqPath' (single l) lv₁ lv₂ = eqLv l lv₁ lv₂
eqPath' (add-via-least l ls) (inj₁ lv₁) (inj₁ lv₂) = eqLv l lv₁ lv₂
eqPath' (add-via-least l ls) (inj₂ p₁) (inj₂ p₂) = eqPath' ls p₁ p₂
eqPath' (add-via-least l ls) (inj₁ lv₁) (inj₂ p₂) = Empty _
eqPath' (add-via-least l ls) (inj₂ p₁) (inj₁ lv₂) = Empty _
eqPath' (add-via-greatest l ls) (inj₁ lv₁) (inj₁ lv₂) = eqLv l lv₁ lv₂
eqPath' (add-via-greatest l ls) (inj₂ p₁) (inj₂ p₂) = eqPath' ls p₁ p₂
eqPath' (add-via-greatest l ls) (inj₁ lv₁) (inj₂ p₂) = Empty _
eqPath' (add-via-greatest l ls) (inj₂ p₁) (inj₁ lv₂) = Empty _
eqPath'-trans : ∀ {a} (Ls : Layers a) → {p₁ p₂ p₃ : Path' Ls} → eqPath' Ls p₁ p₂ → eqPath' Ls p₂ p₃ → eqPath' Ls p₁ p₃
eqPath'-trans (single l) {lv₁} {lv₂} {lv₃} lv₁≈lv₂ lv₂≈lv₃ = eqLv-trans l {lv₁} {lv₂} {lv₃} lv₁≈lv₂ lv₂≈lv₃
eqPath'-trans (add-via-least l ls) {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} lv₁≈lv₂ lv₂≈lv₃ = eqLv-trans l {lv₁} {lv₂} {lv₃} lv₁≈lv₂ lv₂≈lv₃
eqPath'-trans (add-via-least l ls) {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} p₁≈p₂ p₂≈p₃ = eqPath'-trans ls p₁≈p₂ p₂≈p₃
eqPath'-trans (add-via-greatest l ls) {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} lv₁≈lv₂ lv₂≈lv₃ = eqLv-trans l {lv₁} {lv₂} {lv₃} lv₁≈lv₂ lv₂≈lv₃
eqPath'-trans (add-via-greatest l ls) {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} p₁≈p₂ p₂≈p₃ = eqPath'-trans ls p₁≈p₂ p₂≈p₃
eqPath'-sym : ∀ {a} (Ls : Layers a) → {p₁ p₂ : Path' Ls} → eqPath' Ls p₁ p₂ → eqPath' Ls p₂ p₁
eqPath'-sym (single l) {lv₁} {lv₂} lv₁≈lv₂ = eqLv-sym l {lv₁} {lv₂} lv₁≈lv₂
eqPath'-sym (add-via-least l ls) {inj₁ lv₁} {inj₁ lv₂}lv₁≈lv₂ = eqLv-sym l {lv₁} {lv₂} lv₁≈lv₂
eqPath'-sym (add-via-least l ls) {inj₂ p₁} {inj₂ p₂} p₁≈p₂ = eqPath'-sym ls p₁≈p₂
eqPath'-sym (add-via-greatest l ls) {inj₁ lv₁} {inj₁ lv₂}lv₁≈lv₂ = eqLv-sym l {lv₁} {lv₂} lv₁≈lv₂
eqPath'-sym (add-via-greatest l ls) {inj₂ p₁} {inj₂ p₂} p₁≈p₂ = eqPath'-sym ls p₁≈p₂
eqPath'-refl : ∀ {a} (Ls : Layers a) → (p : Path' Ls) → eqPath' Ls p p
eqPath'-refl (single l) lv = eqLv-refl l lv
eqPath'-refl (add-via-least l ls) (inj₁ lv) = eqLv-refl l lv
eqPath'-refl (add-via-least l ls) (inj₂ p) = eqPath'-refl ls p
eqPath'-refl (add-via-greatest l ls) (inj₁ lv) = eqLv-refl l lv
eqPath'-refl (add-via-greatest l ls) (inj₂ p) = eqPath'-refl ls p
instance
eqPath'-Equivalence : ∀ {a} {Ls : Layers a} → IsEquivalence (Path' Ls) (eqPath' Ls)
eqPath'-Equivalence {Ls = Ls} = record
{ ≈-trans = eqPath'-trans Ls
; ≈-sym = eqPath'-sym Ls
; ≈-refl = λ {x} → eqPath'-refl Ls x
}
eqPath'-pathJoin'-cong : ∀ {a} {Ls : Layers a} {a₁ a₂ a₃ a₄} → eqPath' Ls a₁ a₂ → eqPath' Ls a₃ a₄ → lift-≈ (eqPath' Ls) (pathJoin' Ls a₁ a₃) (pathJoin' Ls a₂ a₄)
eqPath'-pathJoin'-cong {Ls = single l} {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄ = eqLv-lvJoin-cong l {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
eqPath'-pathJoin'-cong {Ls = add-via-least l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} {inj₁ lv₄} lv₁≈lv₂ lv₃≈lv₄
with lvJoin (toList l) lv₁ lv₃ | lvJoin (toList l) lv₂ lv₄ | eqLv-lvJoin-cong l {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
... | just _ | just _ | ≈-just lv₁⊔lv₃≈lv₂⊔lv₄ = ≈-just lv₁⊔lv₃≈lv₂⊔lv₄
... | nothing | nothing | ≈-nothing = ≈-nothing
eqPath'-pathJoin'-cong {Ls = add-via-least l ls} {inj₂ p₁} {inj₂ p₂} {inj₁ lv₃} {inj₁ lv₄} p₁≈p₂ lv₃≈lv₄ = ≈-just lv₃≈lv₄
eqPath'-pathJoin'-cong {Ls = add-via-least l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₂ p₃} {inj₂ p₄} lv₁≈lv₂ p₃≈p₄ = ≈-just lv₁≈lv₂
eqPath'-pathJoin'-cong {Ls = Ls@(add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls)} {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} {inj₂ p₄} p₁≈p₂ p₃≈p₄
with pathJoin' ls p₁ p₃ | pathJoin' ls p₂ p₄ | eqPath'-pathJoin'-cong {Ls = ls} {p₁} {p₂} {p₃} {p₄} p₁≈p₂ p₃≈p₄
... | just p₁⊔p₃ | just p₂⊔p₄ | ≈-just p₁⊔p₃≈p₂⊔p₄ = ≈-just p₁⊔p₃≈p₂⊔p₄
... | nothing | nothing | ≈-nothing = ≈-just (eqPath'-refl Ls (inj₁ (inj₁ (PartialLatticeType.HasLeastElement.x {_} {plt} hasLeast))))
eqPath'-pathJoin'-cong {Ls = add-via-greatest l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} {inj₁ lv₄} lv₁≈lv₂ lv₃≈lv₄
with lvJoin (toList l) lv₁ lv₃ | lvJoin (toList l) lv₂ lv₄ | eqLv-lvJoin-cong l {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
... | just _ | just _ | ≈-just lv₁⊔lv₃≈lv₂⊔lv₄ = ≈-just lv₁⊔lv₃≈lv₂⊔lv₄
... | nothing | nothing | ≈-nothing = ≈-nothing
eqPath'-pathJoin'-cong {Ls = add-via-greatest l ls} {inj₂ p₁} {inj₂ p₂} {inj₁ lv₃} {inj₁ lv₄} p₁≈p₂ lv₃≈lv₄ = ≈-just lv₃≈lv₄
eqPath'-pathJoin'-cong {Ls = add-via-greatest l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₂ p₃} {inj₂ p₄} lv₁≈lv₂ p₃≈p₄ = ≈-just lv₁≈lv₂
eqPath'-pathJoin'-cong {Ls = add-via-greatest l ls {{greatest}}} {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} {inj₂ p₄} p₁≈p₂ p₃≈p₄
with pathJoin' ls p₁ p₃ | pathJoin' ls p₂ p₄ | eqPath'-pathJoin'-cong {Ls = ls} {p₁} {p₂} {p₃} {p₄} p₁≈p₂ p₃≈p₄
... | just p₁⊔p₃ | just p₂⊔p₄ | ≈-just p₁⊔p₃≈p₂⊔p₄ = ≈-just p₁⊔p₃≈p₂⊔p₄
... | nothing | nothing | ≈-nothing = ≈-nothing
-- Now that we can compare paths for "equality", we can state and
-- prove theorems such as commutativity and idempotence.
data Expr {a} (A : Set a) : Set a where
`_ : A → Expr A
_∨_ : Expr A → Expr A → Expr A
map : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) → Expr A → Expr B
map f (` x) = ` (f x)
map f (e₁ ∨ e₂) = map f e₁ ∨ map f e₂
eval : ∀ {a} {A : Set a} (_⊔?_ : A → A → Maybe A) (e : Expr A) → Maybe A
eval _⊔?_ (` x) = just x
eval _⊔?_ (e₁ ∨ e₂) = (eval _⊔?_ e₁) >>= (λ v₁ → (eval _⊔?_ e₂) >>= (v₁ ⊔?_))
-- a function is "partially sub-homomorphic" for some subset of B (image of f) if
-- for (f A), it preserves the structure of operations _⊕ on A in B.
PartiallySubHomo : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (_⊕_ : A → A → Maybe A) (_⊗_ : B → B → Maybe B) → Set (a ⊔ℓ b)
PartiallySubHomo {A = A} f _⊕_ _⊗_ = ∀ (a₁ a₂ : A) → (f a₁ ⊗ f a₂) ≡ Maybe.map f (a₁ ⊕ a₂)
-- this evaluation property, which depends on PartiallySubHomo, effectively makes
-- it easier to talk about compound operations and the preservation of their
-- structure when _⊗_ is PartiallySubHomo.
--
-- i.e., if (f a) ⊗ (f b) = Maybe.map f (a ⊕ b), then we can make similar claims about f (a ⊕ b ⊕ c)
eval-subHomo : ∀ {a b} {A : Set a} {B : Set b} (f : A → B) (_⊕_ : A → A → Maybe A) (_⊗_ : B → B → Maybe B) (e : Expr A) →
PartiallySubHomo f _⊕_ _⊗_ →
eval _⊗_ (map f e) ≡ Maybe.map f (eval _⊕_ e)
eval-subHomo f _⊕_ _⊗_ (` _) psh = refl
eval-subHomo f _⊕_ _⊗_ (e₁ ∨ e₂) psh
rewrite eval-subHomo f _⊕_ _⊗_ e₁ psh rewrite eval-subHomo f _⊕_ _⊗_ e₂ psh
with eval _⊕_ e₁ | eval _⊕_ e₂
... | just x₁ | just x₂ = psh x₁ x₂
... | nothing | nothing = refl
... | just x₁ | nothing = refl
... | nothing | just x₂ = refl
lvCombine-homo₁ : ∀ {a} plt plts (f : CombineForPLT a) (e : Expr (PartialLatticeType.EltType plt)) → eval (lvCombine f (plt ∷ plts)) (map inj₁ e) ≡ Maybe.map inj₁ (eval (f plt) e)
lvCombine-homo₁ plt plts f e = eval-subHomo inj₁ (f plt) (lvCombine f (plt ∷ plts)) e (λ a₁ a₂ → refl)
lvCombine-homo₂ : ∀ {a} plt plts (f : CombineForPLT a) (e : Expr (ListValue plts)) → eval (lvCombine f (plt ∷ plts)) (map inj₂ e) ≡ Maybe.map inj₂ (eval (lvCombine f plts) e)
lvCombine-homo₂ plt plts f e = eval-subHomo inj₂ (lvCombine f plts) (lvCombine f (plt ∷ plts)) e (λ a₁ a₂ → refl)
pathJoin'-homo-least₁ : ∀ {a} (l : Layer a) (ls : Layers a) least (e : Expr (LayerValue l)) → eval (pathJoin' (add-via-least l {{least}} ls)) (map inj₁ e) ≡ Maybe.map inj₁ (eval (lvJoin (toList l)) e)
pathJoin'-homo-least₁ l ls least e = eval-subHomo inj₁ (lvJoin (toList l)) (pathJoin' (add-via-least l {{least}} ls)) e (λ a₁ a₂ → refl)
pathJoin'-homo-greatest₁ : ∀ {a} (l : Layer a) (ls : Layers a) greatest (e : Expr (LayerValue l)) → eval (pathJoin' (add-via-greatest l ls {{greatest}})) (map inj₁ e) ≡ Maybe.map inj₁ (eval (lvJoin (toList l)) e)
pathJoin'-homo-greatest₁ l ls greatest e = eval-subHomo inj₁ (lvJoin (toList l)) (pathJoin' (add-via-greatest l ls {{greatest}})) e (λ a₁ a₂ → refl)
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)
lvCombine-assoc : ∀ {a} (f : CombineForPLT a) →
(∀ plt → PartialAssoc (PartialLatticeType._≈_ plt) (f plt)) →
∀ (L : List (PartialLatticeType a)) →
PartialAssoc (eqL L) (lvCombine f L)
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ v₁) (inj₁ v₂) (inj₁ v₃)
rewrite lvCombine-homo₁ plt plts f (((` v₁) ∨ (` v₂)) ∨ (` v₃))
rewrite lvCombine-homo₁ plt plts f ((` v₁) ∨ ((` v₂) ∨ (` v₃)))
= lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (f-assoc plt v₁ v₂ v₃)
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ _) (inj₁ v₂) (inj₁ v₃)
with f plt v₂ v₃
... | just _ = ≈-nothing
... | nothing = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ _) (inj₂ _) (inj₁ _) = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) (inj₁ _)
with lvCombine f plts lv₁ lv₂
... | just _ = ≈-nothing
... | nothing = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ v₁) (inj₁ v₂) (inj₂ _)
with f plt v₁ v₂
... | just _ = ≈-nothing
... | nothing = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ _) (inj₁ _) (inj₂ _) = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₁ _) (inj₂ lv₂) (inj₂ lv₃)
with lvCombine f plts lv₂ lv₃
... | just _ = ≈-nothing
... | nothing = ≈-nothing
lvCombine-assoc f f-assoc L@(plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂) (inj₂ lv₃)
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₃)
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-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 = lvCombine-assoc PartialLatticeType._⊔?_ PartialLatticeType.⊔-assoc
lvJoin-comm : ∀ {a} (L : List (PartialLatticeType a)) → PartialComm (eqL L) (lvJoin L)
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 = 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
lvJoin-greatest-total : ∀ {a} {L : Layer a} → (lv₁ lv₂ : LayerValue L) → LayerGreatest L → lvJoin (toList L) lv₁ lv₂ ≡ nothing → ⊥
lvJoin-greatest-total {L = plt ∷⁺ []} (inj₁ v₁) (inj₁ v₂) (MkLayerGreatest {{hasGreatest = hasGreatest}}) v₁⊔v₂≡nothing
with IsPartialLattice.HasGreatestElement.not-partial (PartialLatticeType.isPartialLattice plt) hasGreatest v₁ v₂
... | (v₁v₂ , v₁⊔v₂≡justv₁v₂)
with trans (cong (Maybe.map inj₁) (sym v₁⊔v₂≡justv₁v₂)) v₁⊔v₂≡nothing
... | ()
pathJoin'-greatest-total : ∀ {a} {Ls : Layers a} → (p₁ p₂ : Path' Ls) → LayerGreatest (head Ls) → pathJoin' Ls p₁ p₂ ≡ nothing → ⊥
pathJoin'-greatest-total {Ls = single L} lv₁ lv₂ layerGreatest lv₁⊔lv₂≡nothing = lvJoin-greatest-total {L = L} lv₁ lv₂ layerGreatest lv₁⊔lv₂≡nothing
pathJoin'-greatest-total {Ls = add-via-greatest L _} (inj₁ lv₁) (inj₁ lv₂) layerGreatest _
with nothing <- lvJoin (toList L) lv₁ lv₂ in lv₁⊔?lv₂=? = lvJoin-greatest-total {L = L} lv₁ lv₂ layerGreatest lv₁⊔?lv₂=?
pathJoin'-greatest-total {Ls = add-via-least L _} (inj₁ lv₁) (inj₁ lv₂) layerGreatest _
with nothing <- lvJoin (toList L) lv₁ lv₂ in lv₁⊔?lv₂=? = lvJoin-greatest-total {L = L} lv₁ lv₂ layerGreatest lv₁⊔?lv₂=?
pathJoin'-greatest-total {Ls = add-via-least (plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} Ls'} (inj₂ p₁) (inj₂ p₂) (MkLayerGreatest {{hasGreatest = hasGreatest}}) inj₂p₁⊔inj₂p₂≡nothing
with pathJoin' Ls' p₁ p₂ | inj₂p₁⊔inj₂p₂≡nothing
... | nothing | ()
... | just _ | ()
pathJoin'-greatest-total {Ls = add-via-greatest L Ls {{layerGreatest}}} (inj₂ p₁) (inj₂ p₂) _ inj₂p₁⊔inj₂p₂≡nothing
with pathJoin' Ls p₁ p₂ in p₁⊔p₂=? | inj₂p₁⊔inj₂p₂≡nothing
... | just p₁⊔p₂ | ()
... | nothing | refl = pathJoin'-greatest-total {Ls = Ls} p₁ p₂ layerGreatest p₁⊔p₂=?
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 = 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@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
with pathJoin' ls p₁ p₂ | pathJoin' ls p₂ p₁ | pathJoin'-comm {Ls = ls} p₁ p₂
... | just p | just p' | ≈-just p≈p' = ≈-just p≈p'
... | nothing | nothing | ≈-nothing = ≈-just (eqLv-refl l (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasLeast)))
pathJoin'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqLv-refl l lv₁)
pathJoin'-comm {Ls = add-via-least l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqLv-refl l lv₂)
pathJoin'-comm {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₁ lv₂) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-comm (toList l) lv₁ lv₂)
pathJoin'-comm {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₂ p₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathJoin'-comm {Ls = ls} p₁ p₂)
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₂)
pathMeet'-comm {Ls = add-via-least l ls} (inj₂ p₁) (inj₂ p₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-comm {Ls = ls} p₁ p₂)
pathMeet'-comm {Ls = add-via-least l ls} (inj₁ lv₁) (inj₂ p₂) = ≈-just (eqPath'-refl ls p₂)
pathMeet'-comm {Ls = add-via-least l ls} (inj₂ p₁) (inj₁ lv₂) = ≈-just (eqPath'-refl ls p₁)
pathMeet'-comm {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
with lvMeet (toList l) lv₁ lv₂ | lvMeet (toList l) lv₂ lv₁ | lvMeet-comm (toList l) lv₁ lv₂
... | just lv | just lv' | ≈-just lv≈lv' = ≈-just lv≈lv'
... | nothing | nothing | ≈-nothing
with ls | greatest | valueAtHead ls
-- begin dumb: don't know why, but abstracting on `head ls` leads to an ill-formed case
... | single l' | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
= ≈-just (eqLv-refl l' (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))))
... | add-via-least l' {{least = least}} ls' | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
= ≈-just (eqPath'-refl (add-via-least l' {{least}} ls') (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))))
... | add-via-greatest l' ls' {{greatest = greatest'}} | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
= ≈-just (eqPath'-refl (add-via-greatest l' ls' {{greatest'}}) (vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))))
-- end dumb
pathMeet'-comm {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p₂) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-comm {Ls = ls} p₁ 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₁)
record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)
_⊔̇_ : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) → Maybe (Path Ls)
_⊔̇_ {a} {ls} p₁ p₂ = Maybe.map MkPath (pathJoin' ls (Path.path p₁) (Path.path p₂))
_⊓̇_ : ∀ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) → Maybe (Path Ls)
_⊓̇_ {a} {ls} p₁ p₂ = Maybe.map MkPath (pathMeet' ls (Path.path p₁) (Path.path p₂))
-- data ListValue {a : Level} : List (PartialLatticeType a) → Set (lsuc a) where
-- here : ∀ {plt : PartialLatticeType a} {pltl : List (PartialLatticeType a)}
-- (v : PartialLatticeType.EltType plt) → ListValue (plt ∷ pltl)
-- there : ∀ {plt : PartialLatticeType a} {pltl : List (PartialLatticeType a)} →
-- ListValue pltl → ListValue (plt ∷ pltl)
Reference in New Issue View Git Blame Copy Permalink