From fbb98de40ffab1aca1bbecb37d4650e18fe0b4d8 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 25 Jul 2025 19:26:03 +0200 Subject: [PATCH] Prove the other absorption law Signed-off-by: Danila Fedorin --- Lattice/Builder.agda | 34 ++++++++++++++++++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/Lattice/Builder.agda b/Lattice/Builder.agda index 9742089..78d491f 100644 --- a/Lattice/Builder.agda +++ b/Lattice/Builder.agda @@ -1025,6 +1025,40 @@ absorb-pathJoin'-pathMeet' {Ls = Ls@(add-via-greatest l ls)} (inj₂ p₁) (inj (λ _ _ → 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₂)