Prove associativity of meet
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
parent
7b2114cd0f
commit
6243326665
@ -517,6 +517,9 @@ pathJoin'-homo-greatest₁ l ls greatest e = eval-subHomo inj₁ (lvJoin (toList
|
||||
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)) →
|
||||
@ -803,6 +806,108 @@ pathMeet'-comm {Ls = add-via-greatest l ls {{greatest}}} (inj₂ p₁) (inj₂ 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
|
||||
|
||||
record _≈_ {a} {Ls : Layers a} (p₁ p₂ : Path Ls) : Set a where
|
||||
field pathEq : eqPath' Ls (Path.path p₁) (Path.path p₂)
|
||||
|
||||
|
||||
Loading…
Reference in New Issue
Block a user