open import Graded.Modality
module Graded.Modality.Properties.Meet
{a} {M : Set a} (𝕄 : Semiring-with-meet M) where
open Semiring-with-meet 𝕄
open import Graded.Modality.Properties.PartialOrder 𝕄
open import Tools.Function
open import Tools.Product
open import Tools.PropositionalEquality
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
open import Tools.Sum using (_⊎_; inj₁; inj₂)
private
variable
p p′ q q′ r r′ : M
∧-monotoneˡ : p ≤ q → p ∧ r ≤ q ∧ r
∧-monotoneˡ {p} {q} {r} p≤q = begin
p ∧ r ≡⟨ ∧-cong p≤q (sym (∧-idem r)) ⟩
(p ∧ q) ∧ r ∧ r ≡⟨ ∧-assoc p q (r ∧ r) ⟩
p ∧ q ∧ r ∧ r ≡⟨ ∧-congˡ (∧-comm q (r ∧ r)) ⟩
p ∧ (r ∧ r) ∧ q ≡⟨ ∧-congˡ (∧-assoc r r q) ⟩
p ∧ r ∧ r ∧ q ≡˘⟨ ∧-assoc p r (r ∧ q) ⟩
(p ∧ r) ∧ r ∧ q ≡⟨ ∧-congˡ (∧-comm r q) ⟩
(p ∧ r) ∧ (q ∧ r) ∎
where open Tools.Reasoning.PropositionalEquality
∧-monotoneʳ : p ≤ q → r ∧ p ≤ r ∧ q
∧-monotoneʳ {p} {q} {r} p≤q = begin
r ∧ p ≡⟨ ∧-cong (sym (∧-idem r)) p≤q ⟩
(r ∧ r) ∧ (p ∧ q) ≡⟨ ∧-assoc r r (p ∧ q) ⟩
r ∧ r ∧ p ∧ q ≡⟨ ∧-congˡ (∧-comm r (p ∧ q)) ⟩
r ∧ (p ∧ q) ∧ r ≡⟨ ∧-congˡ (∧-assoc p q r) ⟩
r ∧ p ∧ (q ∧ r) ≡˘⟨ ∧-assoc r p (q ∧ r) ⟩
(r ∧ p) ∧ (q ∧ r) ≡⟨ ∧-congˡ (∧-comm q r) ⟩
(r ∧ p) ∧ (r ∧ q) ∎
where open Tools.Reasoning.PropositionalEquality
∧-monotone : p ≤ p′ → q ≤ q′ → p ∧ q ≤ p′ ∧ q′
∧-monotone p≤p′ q≤q′ = ≤-trans (∧-monotoneˡ p≤p′) (∧-monotoneʳ q≤q′)
∧-decreasingˡ : (p q : M) → p ∧ q ≤ p
∧-decreasingˡ p q = begin
p ∧ q ≡˘⟨ ∧-congʳ (∧-idem p) ⟩
(p ∧ p) ∧ q ≡⟨ ∧-assoc p p q ⟩
p ∧ (p ∧ q) ≡⟨ ∧-comm p (p ∧ q) ⟩
(p ∧ q) ∧ p ∎
where open Tools.Reasoning.PropositionalEquality
∧-decreasingʳ : (p q : M) → p ∧ q ≤ q
∧-decreasingʳ p q = begin
p ∧ q ≡˘⟨ ∧-congˡ (∧-idem q) ⟩
p ∧ (q ∧ q) ≡˘⟨ ∧-assoc p q q ⟩
(p ∧ q) ∧ q ∎
where open Tools.Reasoning.PropositionalEquality
∧-greatest-lower-bound : p ≤ q → p ≤ r → p ≤ q ∧ r
∧-greatest-lower-bound {p = p} {q = q} {r = r} p≤q p≤r = begin
p ≡⟨ p≤q ⟩
p ∧ q ≡⟨ ∧-congʳ p≤r ⟩
(p ∧ r) ∧ q ≡⟨ ∧-assoc _ _ _ ⟩
p ∧ (r ∧ q) ≡⟨ ∧-congˡ (∧-comm _ _) ⟩
p ∧ (q ∧ r) ∎
where
open Tools.Reasoning.PropositionalEquality
∧≤⇔ :
(∀ p q → p ≤ q ⊎ q ≤ p) →
p ∧ q ≤ r ⇔ (p ≤ r ⊎ q ≤ r)
∧≤⇔ {p = p} {q = q} {r = r} total =
(λ p∧q≤r →
case total p q of λ where
(inj₁ p≤q) → inj₁ $ begin
p ≤⟨ ∧-greatest-lower-bound ≤-refl p≤q ⟩
p ∧ q ≤⟨ p∧q≤r ⟩
r ∎
(inj₂ q≤p) → inj₂ $ begin
q ≤⟨ ∧-greatest-lower-bound q≤p ≤-refl ⟩
p ∧ q ≤⟨ p∧q≤r ⟩
r ∎)
, (λ where
(inj₁ p≤r) → begin
p ∧ q ≤⟨ ∧-decreasingˡ _ _ ⟩
p ≤⟨ p≤r ⟩
r ∎
(inj₂ q≤r) → begin
p ∧ q ≤⟨ ∧-decreasingʳ _ _ ⟩
q ≤⟨ q≤r ⟩
r ∎)
where
open Tools.Reasoning.PartialOrder ≤-poset
largest→∧≡ʳ : (∀ q → q ≤ p) → p ∧ q ≡ q
largest→∧≡ʳ ≤p = ≤-antisym
(∧-decreasingʳ _ _)
(∧-greatest-lower-bound (≤p _) ≤-refl)
largest→∧≡ˡ : (∀ q → q ≤ p) → q ∧ p ≡ q
largest→∧≡ˡ {p = p} {q = q} ≤p =
q ∧ p ≡⟨ ∧-comm _ _ ⟩
p ∧ q ≡⟨ largest→∧≡ʳ ≤p ⟩
q ∎
where
open Tools.Reasoning.PropositionalEquality
<∧ˡ : p < q ∧ r → p < q
<∧ˡ {p = p} {q = q} {r = r} (p≤q∧r , p≢q∧r) =
(let open Tools.Reasoning.PartialOrder ≤-poset in begin
p ≤⟨ p≤q∧r ⟩
q ∧ r ≤⟨ ∧-decreasingˡ _ _ ⟩
q ∎)
, (let open Tools.Reasoning.PropositionalEquality in λ p≡q →
p≢q∧r (
p ≡⟨ p≤q∧r ⟩
p ∧ (q ∧ r) ≡˘⟨ ∧-assoc _ _ _ ⟩
(p ∧ q) ∧ r ≡⟨ cong (λ p → (p ∧ _) ∧ _) p≡q ⟩
(q ∧ q) ∧ r ≡⟨ cong (_∧ _) (∧-idem _) ⟩
q ∧ r ∎))
<∧ʳ : p < q ∧ r → p < r
<∧ʳ p<q∧r = <∧ˡ (subst (_ <_) (∧-comm _ _) p<q∧r)
+≤∧→≤𝟘 :
(∀ p q → p + q ≤ p ∧ q) →
(∀ p → p ≤ 𝟘)
+≤∧→≤𝟘 +≤∧ p =
p ≡˘⟨ +-identityʳ _ ⟩
p + 𝟘 ≡⟨ +≤∧ _ _ ⟩
(p + 𝟘) ∧ (p ∧ 𝟘) ≡⟨ ∧-congʳ (+-identityʳ _) ⟩
p ∧ (p ∧ 𝟘) ≡˘⟨ ∧-assoc _ _ _ ⟩
(p ∧ p) ∧ 𝟘 ≡⟨ ∧-congʳ (∧-idem _) ⟩
p ∧ 𝟘 ∎
where
open Tools.Reasoning.PropositionalEquality
opaque
·[𝟘∧𝟙]≡𝟘∧ : p · (𝟘 ∧ 𝟙) ≡ 𝟘 ∧ p
·[𝟘∧𝟙]≡𝟘∧ {p} =
p · (𝟘 ∧ 𝟙) ≡⟨ ·-distribˡ-∧ _ _ _ ⟩
p · 𝟘 ∧ p · 𝟙 ≡⟨ ∧-cong (·-zeroʳ _) (·-identityʳ _) ⟩
𝟘 ∧ p ∎
where
open Tools.Reasoning.PropositionalEquality