open import Graded.Modality
module Graded.Modality.Properties.Multiplication
{a} {M : Set a} (𝕄 : Semiring-with-meet M) where
open Semiring-with-meet 𝕄
open import Graded.Modality.Properties.Meet 𝕄
open import Graded.Modality.Properties.PartialOrder 𝕄
open import Tools.Algebra M
open import Tools.Function
open import Tools.Product
open import Tools.PropositionalEquality
import Tools.Reasoning.PartialOrder
private
variable
p p′ q q′ r r′ : M
·-monotoneˡ : p ≤ q → p · r ≤ q · r
·-monotoneˡ {p} {q} {r} p≤q = trans (·-congʳ p≤q) (·-distribʳ-∧ r p q)
·-monotoneʳ : p ≤ q → r · p ≤ r · q
·-monotoneʳ {p} {q} {r} p≤q = trans (·-congˡ p≤q) (·-distribˡ-∧ r p q)
·-monotone : p ≤ p′ → q ≤ q′ → p · q ≤ p′ · q′
·-monotone p≤p′ q≤q′ = ≤-trans (·-monotoneˡ p≤p′) (·-monotoneʳ q≤q′)
opaque
≤𝟘⇔𝟙≤𝟘 : (∀ {p} → p ≤ 𝟘) ⇔ 𝟙 ≤ 𝟘
≤𝟘⇔𝟙≤𝟘 =
(λ ≤𝟘 → ≤𝟘)
, (λ 𝟙≤𝟘 {p = p} → begin
p ≡˘⟨ ·-identityʳ _ ⟩
p · 𝟙 ≤⟨ ·-monotoneʳ 𝟙≤𝟘 ⟩
p · 𝟘 ≡⟨ ·-zeroʳ _ ⟩
𝟘 ∎)
where
open Tools.Reasoning.PartialOrder ≤-poset
ω·-decreasing : ω · p ≤ p
ω·-decreasing {p = p} = begin
ω · p ≤⟨ ·-monotoneˡ ω≤𝟙 ⟩
𝟙 · p ≡⟨ ·-identityˡ _ ⟩
p ∎
where
open Tools.Reasoning.PartialOrder ≤-poset
opaque
·ω-decreasing : p · ω ≤ p
·ω-decreasing {p = p} = begin
p · ω ≤⟨ ·-monotoneʳ ω≤𝟙 ⟩
p · 𝟙 ≡⟨ ·-identityʳ _ ⟩
p ∎
where
open Tools.Reasoning.PartialOrder ≤-poset
·-order-reflectingˡ :
(∀ q r → p · q ≡ p · r → q ≡ r) →
p · q ≤ p · r → q ≤ r
·-order-reflectingˡ {p = p} {q = q} {r = r} inj =
p · q ≤ p · r →⟨ idᶠ ⟩
p · q ≡ p · q ∧ p · r →⟨ flip trans (sym (·-distribˡ-∧ _ _ _)) ⟩
p · q ≡ p · (q ∧ r) →⟨ inj _ _ ⟩
q ≡ q ∧ r →⟨ idᶠ ⟩
q ≤ r □
·-order-reflectingʳ :
(∀ q r → q · p ≡ r · p → q ≡ r) →
q · p ≤ r · p → q ≤ r
·-order-reflectingʳ {p = p} {q = q} {r = r} inj =
q · p ≤ r · p →⟨ idᶠ ⟩
q · p ≡ q · p ∧ r · p →⟨ flip trans (sym (·-distribʳ-∧ _ _ _)) ⟩
q · p ≡ (q ∧ r) · p →⟨ inj _ _ ⟩
q ≡ q ∧ r →⟨ idᶠ ⟩
q ≤ r □
·-sub-interchangeable-∧ : _·_ SubInterchangeable _∧_ by _≤_
·-sub-interchangeable-∧ p q p′ q′ = begin
(p ∧ q) · (p′ ∧ q′) ≈⟨ ·-distribˡ-∧ _ _ _ ⟩
((p ∧ q) · p′) ∧ ((p ∧ q) · q′) ≈⟨ ∧-cong (·-distribʳ-∧ _ _ _) (·-distribʳ-∧ _ _ _) ⟩
((p · p′) ∧ (q · p′)) ∧ ((p · q′) ∧ (q · q′)) ≤⟨ ∧-monotone (∧-decreasingˡ _ _) (∧-decreasingʳ _ _) ⟩
(p · p′) ∧ (q · q′) ∎
where
open Tools.Reasoning.PartialOrder ≤-poset