1201 lines
83 KiB
Agda
1201 lines
83 KiB
Agda
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 | ()
|
||
|
||
|
||
PartialAbsorb : ∀ {a} {A : Set a} (_≈_ : A → A → Set a) (_⊗₁_ : A → A → Maybe A) (_⊗₂_ : A → A → Maybe A) → Set a
|
||
PartialAbsorb {a} {A} _≈_ _⊗₁_ _⊗₂_ = ∀ (x y : A) → maybe (λ x⊗₂y → lift-≈ _≈_ (x ⊗₁ x⊗₂y) (just x)) (Trivial _) (x ⊗₂ y)
|
||
|
||
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-⊔-⊓ : PartialAbsorb _≈_ _⊔?_ _⊓?_
|
||
absorb-⊓-⊔ : PartialAbsorb _≈_ _⊓?_ _⊔?_
|
||
|
||
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
|
||
constructor mkPartialLatticeType
|
||
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 (?)
|
||
|
||
greatestPath : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls)) → Path' Ls
|
||
greatestPath Ls greatest
|
||
with head Ls | greatest | valueAtHead Ls
|
||
... | _ | MkLayerGreatest {{hasGreatest = hasGreatest}} | vah
|
||
= vah (inj₁ (IsPartialSemilattice.HasAbsorbingElement.x hasGreatest))
|
||
|
||
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 = just (inj₂ (greatestPath ls greatest))
|
||
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
|
||
|
||
eqPath'-pathMeet'-cong : ∀ {a} {Ls : Layers a} {a₁ a₂ a₃ a₄} → eqPath' Ls a₁ a₂ → eqPath' Ls a₃ a₄ → lift-≈ (eqPath' Ls) (pathMeet' Ls a₁ a₃) (pathMeet' Ls a₂ a₄)
|
||
eqPath'-pathMeet'-cong {Ls = single l} {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄ = eqLv-lvMeet-cong l {lv₁} {lv₂} {lv₃} {lv₄} lv₁≈lv₂ lv₃≈lv₄
|
||
eqPath'-pathMeet'-cong {Ls = add-via-least l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} {inj₁ lv₄} lv₁≈lv₂ lv₃≈lv₄
|
||
with lvMeet (toList l) lv₁ lv₃ | lvMeet (toList l) lv₂ lv₄ | eqLv-lvMeet-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'-pathMeet'-cong {Ls = add-via-least l ls} {inj₂ p₁} {inj₂ p₂} {inj₁ lv₃} {inj₁ lv₄} p₁≈p₂ lv₃≈lv₄ = ≈-just p₁≈p₂
|
||
eqPath'-pathMeet'-cong {Ls = add-via-least l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₂ p₃} {inj₂ p₄} lv₁≈lv₂ p₃≈p₄ = ≈-just p₃≈p₄
|
||
eqPath'-pathMeet'-cong {Ls = add-via-least l {{least}} ls} {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} {inj₂ p₄} p₁≈p₂ p₃≈p₄
|
||
with pathMeet' ls p₁ p₃ | pathMeet' ls p₂ p₄ | eqPath'-pathMeet'-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
|
||
eqPath'-pathMeet'-cong {Ls = add-via-greatest l ls {{greatest}}} {inj₁ lv₁} {inj₁ lv₂} {inj₁ lv₃} {inj₁ lv₄} lv₁≈lv₂ lv₃≈lv₄
|
||
with lvMeet (toList l) lv₁ lv₃ | lvMeet (toList l) lv₂ lv₄ | eqLv-lvMeet-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 = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
|
||
eqPath'-pathMeet'-cong {Ls = add-via-greatest l ls} {inj₂ p₁} {inj₂ p₂} {inj₁ lv₃} {inj₁ lv₄} p₁≈p₂ lv₃≈lv₄ = ≈-just p₁≈p₂
|
||
eqPath'-pathMeet'-cong {Ls = add-via-greatest l ls} {inj₁ lv₁} {inj₁ lv₂} {inj₂ p₃} {inj₂ p₄} lv₁≈lv₂ p₃≈p₄ = ≈-just p₃≈p₄
|
||
eqPath'-pathMeet'-cong {Ls = add-via-greatest l ls {{greatest}}} {inj₂ p₁} {inj₂ p₂} {inj₂ p₃} {inj₂ p₄} p₁≈p₂ p₃≈p₄
|
||
with pathMeet' ls p₁ p₃ | pathMeet' ls p₂ p₄ | eqPath'-pathMeet'-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₂)
|
||
|
||
PartialAbsorb-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₂) →
|
||
∀ (_⊕₁_ : A → A → Maybe A) (_⊕₂_ : A → A → Maybe A)
|
||
(_⊗₁_ : B → B → Maybe B) (_⊗₂_ : B → B → Maybe B) →
|
||
PartiallySubHomo f _⊕₁_ _⊗₁_ →
|
||
PartiallySubHomo f _⊕₂_ _⊗₂_ →
|
||
PartialAbsorb _≈ᵃ_ _⊕₁_ _⊕₂_ →
|
||
∀ (x y : A) → maybe (λ x⊗₂y → lift-≈ _≈ᵇ_ (f x ⊗₁ x⊗₂y) (just (f x))) (Trivial _) (f x ⊗₂ f y)
|
||
PartialAbsorb-map f _≈ᵃ_ _≈ᵇ_ ≈ᵃ⇒≈ᵇ _⊕₁_ _⊕₂_ _⊗₁_ _⊗₂_ psh₁ psh₂ absorbᵃ x y
|
||
with x ⊕₂ y | f x ⊗₂ f y | psh₂ x y | absorbᵃ x y
|
||
... | nothing | nothing | refl | _ = mkTrivial
|
||
... | just x⊕₂y | just fx⊗₂fy | refl | x⊕₁xy≈?x
|
||
with x ⊕₁ x⊕₂y | f x ⊗₁ (f x⊕₂y) | psh₁ x x⊕₂y | x⊕₁xy≈?x
|
||
... | just x⊕₁xy | just fx⊗₁fx⊕₂y | refl | ≈-just x⊕₁xy≈x = ≈-just (≈ᵃ⇒≈ᵇ _ _ x⊕₁xy≈x)
|
||
|
||
|
||
-- 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)
|
||
|
||
pathMeet'-homo-least₁ : ∀ {a} (l : Layer a) (ls : Layers a) least (e : Expr (LayerValue l)) → eval (pathMeet' (add-via-least l {{least}} ls)) (map inj₁ e) ≡ Maybe.map inj₁ (eval (lvMeet (toList l)) e)
|
||
pathMeet'-homo-least₁ l ls least e = eval-subHomo inj₁ (lvMeet (toList l)) (pathMeet' (add-via-least l {{least}} ls)) 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
|
||
|
||
lvCombine-absorb : ∀ {a} (f₁ f₂ : CombineForPLT a) →
|
||
(∀ plt → PartialAbsorb (PartialLatticeType._≈_ plt) (f₁ plt) (f₂ plt)) →
|
||
∀ (L : List (PartialLatticeType a)) →
|
||
PartialAbsorb (eqL L) (lvCombine f₁ L) (lvCombine f₂ L)
|
||
lvCombine-absorb f₁ f₂ absorb-f₁-f₂ [] ()
|
||
lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₁ v₁) (inj₁ v₂)
|
||
= PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (f₁ plt) (f₂ plt)
|
||
(lvCombine f₁ (plt ∷ plts)) (lvCombine f₂ (plt ∷ plts))
|
||
(λ _ _ → refl) (λ _ _ → refl)
|
||
(absorb-f₁-f₂ plt) v₁ v₂
|
||
lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₂ lv₁) (inj₁ v₂) = mkTrivial
|
||
lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₁ v₁) (inj₂ lv₂) = mkTrivial
|
||
lvCombine-absorb f₁ f₂ absorb-f₁-f₂ (plt ∷ plts) (inj₂ lv₁) (inj₂ lv₂)
|
||
= PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (lvCombine f₁ plts) (lvCombine f₂ plts)
|
||
(lvCombine f₁ (plt ∷ plts)) (lvCombine f₂ (plt ∷ plts))
|
||
(λ _ _ → refl) (λ _ _ → refl)
|
||
(lvCombine-absorb f₁ f₂ absorb-f₁-f₂ plts) lv₁ lv₂
|
||
|
||
absorb-lvJoin-lvMeet : ∀ {a} (L : List (PartialLatticeType a)) → PartialAbsorb (eqL L) (lvJoin L) (lvMeet L)
|
||
absorb-lvJoin-lvMeet = lvCombine-absorb PartialLatticeType._⊔?_ PartialLatticeType._⊓?_ PartialLatticeType.absorb-⊔-⊓
|
||
|
||
absorb-lvMeet-lvJoin : ∀ {a} (L : List (PartialLatticeType a)) → PartialAbsorb (eqL L) (lvMeet L) (lvJoin L)
|
||
absorb-lvMeet-lvJoin = lvCombine-absorb PartialLatticeType._⊓?_ PartialLatticeType._⊔?_ PartialLatticeType.absorb-⊓-⊔
|
||
|
||
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
|
||
|
||
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₃=?)
|
||
|
||
pathJoin'-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (eqPath' Ls) (pathJoin' Ls)
|
||
pathJoin'-idemp {Ls = single l} lv = lvJoin-idemp (toList l) lv
|
||
pathJoin'-idemp {Ls = add-via-least l ls} (inj₁ lv) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-idemp (toList l) lv)
|
||
pathJoin'-idemp {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p)
|
||
with pathJoin' ls p p | pathJoin'-idemp {Ls = ls} p
|
||
... | just p⊔p | ≈-just p⊔p≈p = ≈-just p⊔p≈p
|
||
pathJoin'-idemp {Ls = add-via-greatest l ls} (inj₁ lv) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvJoin-idemp (toList l) lv)
|
||
pathJoin'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathJoin'-idemp {Ls = ls} 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₂)
|
||
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₁)
|
||
|
||
greatestPath-pathMeet'-identˡ : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls))
|
||
(p : Path' Ls) →
|
||
let pᵍ = greatestPath Ls greatest
|
||
in lift-≈ (eqPath' Ls) (pathMeet' Ls pᵍ p) (just p)
|
||
greatestPath-pathMeet'-identˡ (single (plt ∷⁺ []) ) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ v)
|
||
= lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (PartialLatticeType.greatest-⊓-identˡ plt hasGreatest v)
|
||
greatestPath-pathMeet'-identˡ (add-via-least (plt ∷⁺ []) ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ (inj₁ v))
|
||
= lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _
|
||
(lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (PartialLatticeType.greatest-⊓-identˡ plt hasGreatest v))
|
||
greatestPath-pathMeet'-identˡ (add-via-least l ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₂ p) = ≈-just (eqPath'-refl ls p)
|
||
greatestPath-pathMeet'-identˡ {a = a} (add-via-greatest (plt ∷⁺ []) ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₁ (inj₁ v))
|
||
with PartialLatticeType._⊓?_ plt (PartialLatticeType.HasGreatestElement.x {a = a} {plt} hasGreatest) v | PartialLatticeType.greatest-⊓-identˡ plt hasGreatest v
|
||
... | just vᵍ⊔v | ≈-just vᵍ⊔v≈v = ≈-just vᵍ⊔v≈v
|
||
greatestPath-pathMeet'-identˡ (add-via-greatest l ls) (MkLayerGreatest {{hasGreatest = hasGreatest}}) (inj₂ p) = ≈-just (eqPath'-refl ls p)
|
||
|
||
greatestPath-pathMeet'-identʳ : ∀ {a} (Ls : Layers a) (greatest : LayerGreatest (head Ls))
|
||
(p : Path' Ls) →
|
||
let pᵍ = greatestPath Ls greatest
|
||
in lift-≈ (eqPath' Ls) (pathMeet' Ls p pᵍ) (just p)
|
||
greatestPath-pathMeet'-identʳ Ls greatest p
|
||
= IsEquivalence.≈-trans (lift-≈-Equivalence {{eqPath'-Equivalence {Ls = Ls}}})
|
||
(pathMeet'-comm {Ls = Ls} p (greatestPath Ls greatest))
|
||
(greatestPath-pathMeet'-identˡ Ls greatest p)
|
||
|
||
pathMeet'-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (eqPath' Ls) (pathMeet' Ls)
|
||
pathMeet'-assoc {Ls = single l} lv₁ lv₂ lv₃ = lvMeet-assoc (toList l) lv₁ lv₂ lv₃
|
||
pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
|
||
rewrite pathMeet'-homo-least₁ l ls least (((` lv₁) ∨ (` lv₂)) ∨ (` lv₃))
|
||
rewrite pathMeet'-homo-least₁ l ls least ((` lv₁) ∨ ((` lv₂) ∨ (` lv₃)))
|
||
= lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-assoc (toList l) lv₁ lv₂ lv₃)
|
||
pathMeet'-assoc {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₁ (inj₁ v₂)) (inj₁ (inj₁ v₃))
|
||
with PartialLatticeType._⊓?_ plt v₂ v₃ | IsPartialLattice.HasLeastElement.not-partial (PartialLatticeType.isPartialLattice plt) hasLeast v₂ v₃
|
||
... | just v₂⊓l₃ | (_ , refl) = ≈-just (eqPath'-refl ls p₁)
|
||
pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂) (inj₁ lv₃)
|
||
= ≈-just (eqPath'-refl ls p₂)
|
||
pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₂ p₂) (inj₁ lv₃)
|
||
with pathMeet' ls p₁ p₂
|
||
... | just p₁⊓p₂ = ≈-just (eqPath'-refl ls p₁⊓p₂)
|
||
... | nothing = ≈-nothing
|
||
pathMeet'-assoc {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₁ (inj₁ v₁)) (inj₁ (inj₁ v₂)) (inj₂ p₃)
|
||
with PartialLatticeType._⊓?_ plt v₁ v₂ | IsPartialLattice.HasLeastElement.not-partial (PartialLatticeType.isPartialLattice plt) hasLeast v₁ v₂
|
||
... | just _ | (_ , refl) = ≈-just (eqPath'-refl ls p₃)
|
||
pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂) (inj₂ p₃)
|
||
with pathMeet' ls p₁ p₃
|
||
... | just p₁⊓p₃ = ≈-just (eqPath'-refl ls p₁⊓p₃)
|
||
... | nothing = ≈-nothing
|
||
pathMeet'-assoc {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂) (inj₂ p₃)
|
||
with pathMeet' ls p₂ p₃
|
||
... | just p₂⊓p₃ = ≈-just (eqPath'-refl ls p₂⊓p₃)
|
||
... | nothing = ≈-nothing
|
||
pathMeet'-assoc {Ls = add-via-least l ls} (inj₂ p₁) (inj₂ p₂) (inj₂ p₃)
|
||
with pathMeet' ls p₁ p₂ in p₁⊓?p₂=? | pathMeet' ls p₂ p₃ in p₂⊓?p₃=? | pathMeet'-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 | nothing | _ = ≈-nothing
|
||
... | nothing | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁ p₂⊓p₃ = ≈-nothing
|
||
... | just p₁⊓p₂ | nothing | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁⊓p₂ p₃ = ≈-nothing
|
||
-- begin dumb: due to annoying nested with-abstractions, we have several written-out cases here
|
||
-- for the same inj₁/inj₁/inj₁ combination.
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
|
||
with lvMeet (toList l) lv₁ lv₂ | lvMeet (toList l) lv₂ lv₃ | lvMeet-assoc (toList l) lv₁ lv₂ lv₃
|
||
... | just lv₁⊓lv₂ | just lv₂⊓lv₃ | p₁⊓?p₂p₃≈p₁p₂⊓?p₃
|
||
with lvMeet (toList l) lv₁⊓lv₂ lv₃ | lvMeet (toList l) lv₁ lv₂⊓lv₃ | p₁⊓?p₂p₃≈p₁p₂⊓?p₃
|
||
... | just _ | just _ | ≈-just p₁⊓p₂p₃≈p₁p₂⊓p₃ = ≈-just p₁⊓p₂p₃≈p₁p₂⊓p₃
|
||
... | nothing | nothing | ≈-nothing = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
|
||
| nothing | nothing | _ = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
|
||
| just lv₁⊓lv₂ | nothing | p₁⊓?p₂p₃≈p₁p₂⊓?p₃
|
||
with nothing <- lvMeet (toList l) lv₁⊓lv₂ lv₃ = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₁ lv₃)
|
||
| nothing | just lv₂⊓lv₃ | p₁⊓?p₂p₃≈p₁p₂⊓?p₃
|
||
with nothing <- lvMeet (toList l) lv₁ lv₂⊓lv₃ = ≈-just (eqPath'-refl ls (greatestPath ls greatest))
|
||
-- end dumb
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₁ lv₂) (inj₁ lv₃)
|
||
with lvMeet (toList l) lv₂ lv₃
|
||
... | just _ = ≈-just (eqPath'-refl ls p₁)
|
||
... | nothing = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (IsEquivalence.≈-sym (lift-≈-Equivalence {{eqPath'-Equivalence {Ls = ls}}}) (greatestPath-pathMeet'-identʳ ls greatest p₁))
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂) (inj₁ lv₃)
|
||
= ≈-just (eqPath'-refl ls p₂)
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p₂) (inj₁ lv₃)
|
||
with pathMeet' ls p₁ p₂
|
||
... | just p₁⊓p₂ = ≈-just (eqPath'-refl ls p₁⊓p₂)
|
||
... | nothing = ≈-nothing
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂) (inj₂ p₃)
|
||
with lvMeet (toList l) lv₁ lv₂
|
||
... | just _ = ≈-just (eqPath'-refl ls p₃)
|
||
... | nothing = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (greatestPath-pathMeet'-identˡ ls greatest p₃)
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₁ lv₂) (inj₂ p₃)
|
||
with pathMeet' ls p₁ p₃
|
||
... | just p₁⊓p₃ = ≈-just (eqPath'-refl ls p₁⊓p₃)
|
||
... | nothing = ≈-nothing
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂) (inj₂ p₃)
|
||
with pathMeet' ls p₂ p₃
|
||
... | just p₂⊓p₃ = ≈-just (eqPath'-refl ls p₂⊓p₃)
|
||
... | nothing = ≈-nothing
|
||
pathMeet'-assoc {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ p₂) (inj₂ p₃)
|
||
with pathMeet' ls p₁ p₂ in p₁⊓?p₂=? | pathMeet' ls p₂ p₃ in p₂⊓?p₃=? | pathMeet'-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 | nothing | _ = ≈-nothing
|
||
... | nothing | just p₂⊓p₃ | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁ p₂⊓p₃ = ≈-nothing
|
||
... | just p₁⊓p₂ | nothing | p₁⊓p₂p₃≈p₁p₂⊓p₃ with nothing ← pathMeet' ls p₁⊓p₂ p₃ = ≈-nothing
|
||
|
||
pathMeet'-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (eqPath' Ls) (pathMeet' Ls)
|
||
pathMeet'-idemp {Ls = single l} lv = lvMeet-idemp (toList l) lv
|
||
pathMeet'-idemp {Ls = add-via-least l ls} (inj₁ lv) = lift-≈-map inj₁ _ _ (λ _ _ x → x) _ _ (lvMeet-idemp (toList l) lv)
|
||
pathMeet'-idemp {Ls = add-via-least l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p)
|
||
pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₁ lv)
|
||
with lvMeet (toList l) lv lv | lvMeet-idemp (toList l) lv
|
||
... | just lv⊔lv | ≈-just lv⊔lv≈lv = ≈-just lv⊔lv≈lv
|
||
pathMeet'-idemp {Ls = add-via-greatest l ls} (inj₂ p) = lift-≈-map inj₂ _ _ (λ _ _ x → x) _ _ (pathMeet'-idemp {Ls = ls} p)
|
||
|
||
absorb-pathJoin'-pathMeet' : ∀ {a} {Ls : Layers a} → PartialAbsorb (eqPath' Ls) (pathJoin' Ls) (pathMeet' Ls)
|
||
absorb-pathJoin'-pathMeet' {Ls = single l} lv₁ lv₂ = absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
|
||
absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-least l ls)} (inj₁ lv₁) (inj₁ lv₂)
|
||
= PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (lvJoin (toList l)) (lvMeet (toList l))
|
||
(pathJoin' Ls) (pathMeet' Ls)
|
||
(λ _ _ → refl) (λ _ _ → refl)
|
||
(absorb-lvJoin-lvMeet (toList l)) lv₁ lv₂
|
||
absorb-pathJoin'-pathMeet' {Ls = add-via-least l {{least}} ls} (inj₂ p₁) (inj₁ lv₂)
|
||
= pathJoin'-idemp {Ls = add-via-least l {{least}} ls} (inj₂ p₁)
|
||
absorb-pathJoin'-pathMeet' {Ls = add-via-least l ls} (inj₁ lv₁) (inj₂ p₂)
|
||
= ≈-just (eqLv-refl l lv₁)
|
||
absorb-pathJoin'-pathMeet' {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
|
||
with pathMeet' ls p₁ p₂ | absorb-pathJoin'-pathMeet' {Ls = ls} p₁ p₂
|
||
... | nothing | _ = mkTrivial
|
||
... | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
|
||
with pathJoin' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
|
||
... | just _ | ≈-just p₁⊔p₁p₂≈p₁ = ≈-just p₁⊔p₁p₂≈p₁
|
||
absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
|
||
with lvMeet (toList l) lv₁ lv₂ | absorb-lvJoin-lvMeet (toList l) lv₁ lv₂
|
||
... | nothing | _ = ≈-just (eqLv-refl l lv₁)
|
||
... | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
|
||
with lvJoin (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
|
||
... | just _ | ≈-just lv₁⊔lv₁lv₂≈lv₁ = ≈-just lv₁⊔lv₁lv₂≈lv₁
|
||
absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls {{greatest}} } (inj₂ p₁) (inj₁ lv₂)
|
||
= pathJoin'-idemp {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁)
|
||
absorb-pathJoin'-pathMeet' {Ls = add-via-greatest l ls} (inj₁ lv₁) (inj₂ p₂)
|
||
= ≈-just (eqLv-refl l lv₁)
|
||
absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj₂ p₂)
|
||
= PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (pathJoin' ls) (pathMeet' ls)
|
||
(pathJoin' Ls) (pathMeet' Ls)
|
||
(λ _ _ → refl) (λ _ _ → refl)
|
||
(absorb-pathJoin'-pathMeet' {Ls = ls}) p₁ p₂
|
||
|
||
absorb-pathMeet'-pathJoin' : ∀ {a} {Ls : Layers a} → PartialAbsorb (eqPath' Ls) (pathMeet' Ls) (pathJoin' Ls)
|
||
absorb-pathMeet'-pathJoin' {Ls = single l} lv₁ lv₂ = absorb-lvMeet-lvJoin (toList l) lv₁ lv₂
|
||
absorb-pathMeet'-pathJoin' {Ls = Ls@(add-via-least l ls)} (inj₁ lv₁) (inj₁ lv₂)
|
||
= PartialAbsorb-map inj₁ _ _ (λ _ _ x → x) (lvMeet (toList l)) (lvJoin (toList l))
|
||
(pathMeet' Ls) (pathJoin' Ls)
|
||
(λ _ _ → refl) (λ _ _ → refl)
|
||
(absorb-lvMeet-lvJoin (toList l)) lv₁ lv₂
|
||
absorb-pathMeet'-pathJoin' {Ls = add-via-least l ls} (inj₂ p₁) (inj₁ lv₂)
|
||
= ≈-just (eqPath'-refl ls p₁)
|
||
absorb-pathMeet'-pathJoin' {Ls = add-via-least l {{least}} ls} (inj₁ lv₁) (inj₂ p₂)
|
||
= pathMeet'-idemp {Ls = add-via-least l {{least}} ls} (inj₁ lv₁)
|
||
absorb-pathMeet'-pathJoin' {Ls = add-via-least l@(plt ∷⁺ []) {{MkLayerLeast {{hasLeast = hasLeast}}}} ls} (inj₂ p₁) (inj₂ p₂)
|
||
with pathJoin' ls p₁ p₂ | absorb-pathMeet'-pathJoin' {Ls = ls} p₁ p₂
|
||
... | nothing | _ = ≈-just (eqPath'-refl ls p₁)
|
||
... | just p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
|
||
with pathMeet' ls p₁ p₁⊓p₂ | p₁⊔p₁p₂≈?p₁
|
||
... | just _ | ≈-just p₁⊔p₁p₂≈p₁ = ≈-just p₁⊔p₁p₂≈p₁
|
||
absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₁ lv₂)
|
||
with lvJoin (toList l) lv₁ lv₂ | absorb-lvMeet-lvJoin (toList l) lv₁ lv₂
|
||
... | nothing | _ = mkTrivial
|
||
... | just lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
|
||
with lvMeet (toList l) lv₁ lv₁⊓lv₂ | lv₁⊔lv₁lv₂≈?lv₁
|
||
... | just _ | ≈-just lv₁⊔lv₁lv₂≈lv₁ = ≈-just lv₁⊔lv₁lv₂≈lv₁
|
||
absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls} (inj₂ p₁) (inj₁ lv₂)
|
||
= ≈-just (eqPath'-refl ls p₁)
|
||
absorb-pathMeet'-pathJoin' {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁) (inj₂ p₂)
|
||
= pathMeet'-idemp {Ls = add-via-greatest l ls {{greatest}}} (inj₁ lv₁)
|
||
absorb-pathMeet'-pathJoin' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj₂ p₂)
|
||
= PartialAbsorb-map inj₂ _ _ (λ _ _ x → x) (pathMeet' ls) (pathJoin' ls)
|
||
(pathMeet' Ls) (pathJoin' Ls)
|
||
(λ _ _ → refl) (λ _ _ → refl)
|
||
(absorb-pathMeet'-pathJoin' {Ls = ls}) p₁ p₂
|
||
|
||
|
||
record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
|
||
constructor mk-≈
|
||
field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)
|
||
|
||
instance
|
||
≈-Equivalence : ∀ {a} {Ls : Layers a} → IsEquivalence (Path Ls) (_≈_ {Ls = Ls})
|
||
≈-Equivalence {Ls = Ls} =
|
||
record
|
||
{ ≈-refl = λ {(MkPath p)} → mk-≈ (eqPath'-refl Ls p)
|
||
; ≈-sym = λ (mk-≈ p≈p') → mk-≈ (eqPath'-sym Ls p≈p')
|
||
; ≈-trans = λ (mk-≈ p₁≈p₂) (mk-≈ p₂≈p₃) → mk-≈ (eqPath'-trans Ls p₁≈p₂ p₂≈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₂))
|
||
|
||
_⊔̇_-subHomo : ∀ {a} (Ls : Layers a) (e : Expr (Path' Ls)) → eval (_⊔̇_ {Ls = Ls}) (map MkPath e) ≡ Maybe.map MkPath (eval (pathJoin' Ls) e)
|
||
_⊔̇_-subHomo Ls e = eval-subHomo MkPath (pathJoin' Ls) _⊔̇_ e (λ a₁ a₂ → refl)
|
||
|
||
_⊔̇_-comm : ∀ {a} {Ls : Layers a} → PartialComm (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
|
||
_⊔̇_-comm {Ls = Ls} (MkPath p₁) (MkPath p₂)
|
||
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathJoin'-comm {Ls = Ls} p₁ p₂)
|
||
|
||
_⊔̇_-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
|
||
_⊔̇_-assoc {Ls = Ls} (MkPath p₁) (MkPath p₂) (MkPath p₃)
|
||
rewrite _⊔̇_-subHomo Ls (((` p₁) ∨ (` p₂)) ∨ (` p₃))
|
||
rewrite _⊔̇_-subHomo Ls ((` p₁) ∨ ((` p₂) ∨ (` p₃)))
|
||
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathJoin'-assoc {Ls = Ls} p₁ p₂ p₃)
|
||
|
||
_⊔̇_-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
|
||
_⊔̇_-idemp {Ls = Ls} (MkPath p)
|
||
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathJoin'-idemp {Ls = Ls} p)
|
||
|
||
≈-⊔̇-cong : ∀ {a} {Ls : Layers a} → PartialCong (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
|
||
≈-⊔̇-cong {Ls = Ls} (mk-≈ p₁≈p₂) (mk-≈ p₃≈p₄) =
|
||
lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (eqPath'-pathJoin'-cong {Ls = Ls} p₁≈p₂ p₃≈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₂))
|
||
|
||
_⊓̇_-subHomo : ∀ {a} (Ls : Layers a) (e : Expr (Path' Ls)) → eval (_⊓̇_ {Ls = Ls}) (map MkPath e) ≡ Maybe.map MkPath (eval (pathMeet' Ls) e)
|
||
_⊓̇_-subHomo Ls e = eval-subHomo MkPath (pathMeet' Ls) _⊓̇_ e (λ a₁ a₂ → refl)
|
||
|
||
_⊓̇_-comm : ∀ {a} {Ls : Layers a} → PartialComm (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
|
||
_⊓̇_-comm {Ls = Ls} (MkPath p₁) (MkPath p₂)
|
||
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathMeet'-comm {Ls = Ls} p₁ p₂)
|
||
|
||
_⊓̇_-assoc : ∀ {a} {Ls : Layers a} → PartialAssoc (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
|
||
_⊓̇_-assoc {Ls = Ls} (MkPath p₁) (MkPath p₂) (MkPath p₃)
|
||
rewrite _⊓̇_-subHomo Ls (((` p₁) ∨ (` p₂)) ∨ (` p₃))
|
||
rewrite _⊓̇_-subHomo Ls ((` p₁) ∨ ((` p₂) ∨ (` p₃)))
|
||
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathMeet'-assoc {Ls = Ls} p₁ p₂ p₃)
|
||
|
||
_⊓̇_-idemp : ∀ {a} {Ls : Layers a} → PartialIdemp (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
|
||
_⊓̇_-idemp {Ls = Ls} (MkPath p)
|
||
= lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (pathMeet'-idemp {Ls = Ls} p)
|
||
|
||
≈-⊓̇-cong : ∀ {a} {Ls : Layers a} → PartialCong (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
|
||
≈-⊓̇-cong {Ls = Ls} (mk-≈ p₁≈p₂) (mk-≈ p₃≈p₄) =
|
||
lift-≈-map MkPath _ (_≈_ {Ls = Ls}) (λ _ _ → mk-≈) _ _ (eqPath'-pathMeet'-cong {Ls = Ls} p₁≈p₂ p₃≈p₄)
|
||
|
||
instance
|
||
Path-IsPartialJoinSemilattice : ∀ {a} {Ls : Layers a} → IsPartialSemilattice (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
|
||
Path-IsPartialJoinSemilattice {Ls = Ls} =
|
||
record
|
||
{ ⊔-assoc = _⊔̇_-assoc {Ls = Ls}
|
||
; ⊔-comm = _⊔̇_-comm {Ls = Ls}
|
||
; ⊔-idemp = _⊔̇_-idemp {Ls = Ls}
|
||
; ≈-⊔-cong = ≈-⊔̇-cong {Ls = Ls}
|
||
}
|
||
|
||
Path-IsPartialMeetSemilattice : ∀ {a} {Ls : Layers a} → IsPartialSemilattice (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
|
||
Path-IsPartialMeetSemilattice {Ls = Ls} =
|
||
record
|
||
{ ⊔-assoc = _⊓̇_-assoc {Ls = Ls}
|
||
; ⊔-comm = _⊓̇_-comm {Ls = Ls}
|
||
; ⊔-idemp = _⊓̇_-idemp {Ls = Ls}
|
||
; ≈-⊔-cong = ≈-⊓̇-cong {Ls = Ls}
|
||
}
|
||
|
||
⊔̇-⊓̇-absorb : ∀ {a} {Ls : Layers a} → PartialAbsorb (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
|
||
⊔̇-⊓̇-absorb {Ls = Ls} (MkPath p₁) (MkPath p₂)
|
||
= PartialAbsorb-map MkPath _ _ (λ _ _ → mk-≈) (pathJoin' Ls) (pathMeet' Ls)
|
||
(_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
|
||
(λ _ _ → refl) (λ _ _ → refl)
|
||
(absorb-pathJoin'-pathMeet' {Ls = Ls}) p₁ p₂
|
||
|
||
⊓̇-⊔̇-absorb : ∀ {a} {Ls : Layers a} → PartialAbsorb (_≈_ {Ls = Ls}) (_⊓̇_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
|
||
⊓̇-⊔̇-absorb {Ls = Ls} (MkPath p₁) (MkPath p₂)
|
||
= PartialAbsorb-map MkPath _ _ (λ _ _ → mk-≈) (pathMeet' Ls) (pathJoin' Ls)
|
||
(_⊓̇_ {Ls = Ls}) (_⊔̇_ {Ls = Ls})
|
||
(λ _ _ → refl) (λ _ _ → refl)
|
||
(absorb-pathMeet'-pathJoin' {Ls = Ls}) p₁ p₂
|
||
|
||
instance
|
||
Path-IsPartialLattice : ∀ {a} {Ls : Layers a} → IsPartialLattice (_≈_ {Ls = Ls}) (_⊔̇_ {Ls = Ls}) (_⊓̇_ {Ls = Ls})
|
||
Path-IsPartialLattice {Ls = Ls} =
|
||
record
|
||
{ absorb-⊔-⊓ = ⊔̇-⊓̇-absorb {Ls = Ls}
|
||
; absorb-⊓-⊔ = ⊓̇-⊔̇-absorb {Ls = Ls}
|
||
}
|
||
|
||
instance
|
||
-- IsLattice-IsPartialLattice : ∀ {a} {A : Set a}
|
||
-- {_≈_ : A → A → Set a} {_⊔_ : A → A → A} {_⊓_ : A → A → A}
|
||
-- {{lA : IsLattice A _≈_ _⊔_ _⊓_}} → IsPartialLattice _≈_ _⊔_ _⊓_
|
||
-- IsLattice-IsPartialLattice = {!!}
|
||
|
||
Lattice-PartialLattice : ∀ {a} {A : Set a}
|
||
{{lA : Lattice A }} → PartialLattice A
|
||
Lattice-PartialLattice = {!!}
|
||
|
||
Lattice-Least : ∀ {a} {A : Set a}
|
||
{{lA : Lattice A }} → PartialLattice.HasLeastElement (Lattice-PartialLattice {{lA = lA}})
|
||
Lattice-Least = {!!}
|
||
|
||
open import Lattice.Unit
|
||
|
||
ThreeElements : Set
|
||
ThreeElements = Path (add-via-least ((mkPartialLatticeType ⊤) ∷⁺ []) (add-via-least ((mkPartialLatticeType ⊤) ∷⁺ []) (single ((mkPartialLatticeType ⊤) ∷⁺ []))))
|
||
|
||
e₁ : ThreeElements
|
||
e₁ = MkPath (inj₁ (inj₁ tt))
|
||
|
||
e₂ : ThreeElements
|
||
e₂ = MkPath (inj₂ (inj₁ (inj₁ tt)))
|
||
|
||
e₃ : ThreeElements
|
||
e₃ = MkPath (inj₂ (inj₂ (inj₁ tt)))
|
||
|
||
ex1 : e₁ ⊔̇ e₂ ≡ just e₁
|
||
ex1 = refl
|
||
|
||
-- 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)
|