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.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′)
·-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