From 8cb082e3c5e477d4a4a3a0acb7ee7e103d031c8e Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 28 Nov 2025 16:24:29 -0800 Subject: [PATCH] Delete original builder (lol) Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 1198 +----------------------------------------- 1 file changed, 10 insertions(+), 1188 deletions(-) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 1038b95..5e8e250 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -2,1199 +2,21 @@ module Lattice.Builder where open import Lattice open import Equivalence +open import Utils using (fins; fins-complete) +open import Data.Nat as Nat using (ℕ) +open import Data.Fin as Fin using (Fin; suc; zero; _≟_) 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.List.Membership.Propositional as MemProp using () renaming (_∈_ to _∈ˡ_; mapWith∈ to mapWith∈ˡ) +open import Data.List.Membership.Propositional.Properties using () renaming (∈-++⁺ʳ to ∈ˡ-++⁺ʳ) +open import Data.List.Relation.Unary.Any using (Any; here; there) +open import Data.List.Relation.Unary.All using (All; []; _∷_; map) +open import Data.List using (List; _∷_; []; cartesianProduct; cartesianProductWith; foldr) renaming (_++_ to _++ˡ_) open import Data.Sum using (_⊎_; inj₁; inj₂) -open import Data.Product using (Σ; _,_) +open import Data.Product using (Σ; _,_; _×_; proj₁; proj₂) open import Data.Empty using (⊥; ⊥-elim) +open import Relation.Nullary using (¬_; Dec; yes; no) 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)