DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity
14f1494fc3
agda-spa/Lattice/Builder.agda
Danila Fedorin 14f1494fc3 Provide a definition of partial congruence 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
2025-07-22 18:01:48 +02:00

588 lines
35 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}))
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
)
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
}
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
}
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
}
-- 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₂)
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