import Graded.Modality
import Tools.Algebra as A
open import Tools.PropositionalEquality
open import Tools.Sum
open import Tools.Bool hiding (_∧_)
module Graded.Modality.Instances.BoundedStar
{a} {M : Set a}
(open Graded.Modality M)
(𝕄 : Semiring-with-meet)
(open Semiring-with-meet 𝕄)
(_* : A.Op₁ M)
(*-rec : (p : M) → ((p *) ≡ 𝟙 + p · (p *)))
(bounds : (p : M) → (p *) ≤ 𝟘 ⊎ (p *) ≤ 𝟙)
where
open import Graded.Modality.Properties.PartialOrder 𝕄
open import Graded.Modality.Properties.Addition 𝕄
open import Graded.Modality.Properties.Meet 𝕄
open import Graded.Modality.Properties.Multiplication 𝕄
open import Graded.Modality.Variant a
open import Tools.Nullary
import Tools.Reasoning.Equivalence
import Tools.Reasoning.PartialOrder
open import Tools.Product
open import Tools.Algebra M
private
variable
p p′ q q′ r r′ : M
_⊛_▷_ : Op₃ M
p ⊛ q ▷ r = (r *) · (p ∧ q)
⊛-ineq₁ : (p q r : M) → (p ⊛ q ▷ r) ≤ q + r · (p ⊛ q ▷ r)
⊛-ineq₁ p q r = begin
p ⊛ q ▷ r ≡⟨⟩
(r *) · (p ∧ q)
≈⟨ ·-congʳ (*-rec r) ⟩
(𝟙 + r · (r *)) · (p ∧ q)
≈⟨ ·-distribʳ-+ (p ∧ q) 𝟙 (r · (r *)) ⟩
𝟙 · (p ∧ q) + (r · (r *)) · (p ∧ q)
≈⟨ +-cong (·-identityˡ (p ∧ q)) (·-assoc r (r *) (p ∧ q)) ⟩
(p ∧ q) + r · ((r *) · (p ∧ q))
≤⟨ +-monotoneˡ (∧-decreasingʳ p q) ⟩
q + r · (p ⊛ q ▷ r) ∎
where
open Tools.Reasoning.PartialOrder ≤-poset
⊛-ineq₂ : (p q r : M) → p ⊛ q ▷ r ≤ p
⊛-ineq₂ p q r with bounds r
... | inj₁ r*≤𝟘 = begin
p ⊛ q ▷ r ≈⟨⟩
(r *) · (p ∧ q) ≤⟨ ·-monotoneʳ (∧-decreasingˡ p q) ⟩
(r *) · p ≈⟨ ·-congʳ (*-rec r) ⟩
(𝟙 + r · (r *)) · p ≈⟨ ·-distribʳ-+ p 𝟙 _ ⟩
𝟙 · p + (r · (r *)) · p ≈⟨ +-congʳ (·-identityˡ p) ⟩
p + (r · (r *)) · p ≤⟨ +-monotoneʳ (·-monotoneˡ (·-monotoneʳ r*≤𝟘)) ⟩
p + (r · 𝟘) · p ≈⟨ +-congˡ (·-congʳ (·-zeroʳ r)) ⟩
p + 𝟘 · p ≈⟨ +-congˡ (·-zeroˡ p) ⟩
p + 𝟘 ≈⟨ +-identityʳ p ⟩
p ∎
where
open Tools.Reasoning.PartialOrder ≤-poset
... | inj₂ r*≤𝟙 = begin
(r *) · (p ∧ q) ≤⟨ ·-monotone r*≤𝟙 (∧-decreasingˡ p q) ⟩
𝟙 · p ≈⟨ ·-identityˡ p ⟩
p ∎
where
open Tools.Reasoning.PartialOrder ≤-poset
⊛-cong : p ≡ p′ → q ≡ q′ → r ≡ r′ → p ⊛ q ▷ r ≡ p′ ⊛ q′ ▷ r′
⊛-cong p≡p′ q≡q′ r≡r′ = ·-cong (cong _* r≡r′) (∧-cong p≡p′ q≡q′)
+-sub-interchangeable-⊛ : (r : M) → _+_ SubInterchangeable _⊛_▷ r by _≤_
+-sub-interchangeable-⊛ r p q p′ q′ = begin
(p ⊛ q ▷ r) + (p′ ⊛ q′ ▷ r) ≡⟨⟩
(r *) · (p ∧ q) + (r *) · (p′ ∧ q′)
≈˘⟨ ·-distribˡ-+ (r *) _ _ ⟩
(r *) · ((p ∧ q) + (p′ ∧ q′))
≈⟨ ·-congˡ (+-distribˡ-∧ (p ∧ q) p′ q′) ⟩
(r *) · (((p ∧ q) + p′) ∧ ((p ∧ q) + q′))
≈⟨ ·-congˡ (∧-cong (+-distribʳ-∧ p′ p q) (+-distribʳ-∧ q′ p q)) ⟩
(r *) · (((p + p′) ∧ (q + p′)) ∧ ((p + q′) ∧ (q + q′)))
≤⟨ ·-monotoneʳ (∧-monotone (∧-decreasingˡ _ _) (∧-decreasingʳ _ _)) ⟩
(r *) · ((p + p′) ∧ (q + q′)) ≡⟨⟩
(p + p′) ⊛ (q + q′) ▷ r ∎
where
open Tools.Reasoning.PartialOrder ≤-poset
·-sub-distribʳ-⊛ : (r : M) → _·_ SubDistributesOverʳ _⊛_▷ r by _≤_
·-sub-distribʳ-⊛ r q p p′ = begin
(p ⊛ p′ ▷ r) · q ≡⟨⟩
((r *) · (p ∧ p′)) · q ≈⟨ ·-assoc (r *) (p ∧ p′) q ⟩
(r *) · (p ∧ p′) · q ≈⟨ ·-congˡ (·-distribʳ-∧ q p p′) ⟩
(r *) · (p · q ∧ p′ · q) ≡⟨⟩
(p · q) ⊛ (p′ · q) ▷ r ∎
where
open Tools.Reasoning.PartialOrder ≤-poset
⊛-sub-distribˡ-∧ : (r : M) → (_⊛_▷ r) SubDistributesOverˡ _∧_ by _≤_
⊛-sub-distribˡ-∧ r p q q′ = begin
p ⊛ (q ∧ q′) ▷ r ≡⟨⟩
(r *) · (p ∧ (q ∧ q′))
≈˘⟨ ·-congˡ (∧-congʳ (∧-idem p)) ⟩
(r *) · ((p ∧ p) ∧ q ∧ q′)
≈˘⟨ ·-congˡ (∧-assoc (p ∧ p) q q′) ⟩
(r *) · (((p ∧ p) ∧ q) ∧ q′)
≈⟨ ·-congˡ (∧-congʳ (∧-assoc p p q)) ⟩
(r *) · ((p ∧ (p ∧ q)) ∧ q′)
≈⟨ ·-congˡ (∧-congʳ (∧-congˡ (∧-comm p q))) ⟩
(r *) · ((p ∧ (q ∧ p)) ∧ q′)
≈˘⟨ ·-congˡ (∧-congʳ (∧-assoc p q p)) ⟩
(r *) · (((p ∧ q) ∧ p) ∧ q′)
≈⟨ ·-congˡ (∧-assoc (p ∧ q) p q′) ⟩
(r *) · ((p ∧ q) ∧ (p ∧ q′))
≈⟨ ·-distribˡ-∧ (r *) (p ∧ q) (p ∧ q′) ⟩
(r *) · (p ∧ q) ∧ (r *) · (p ∧ q′) ≡⟨⟩
(p ⊛ q ▷ r) ∧ (p ⊛ q′ ▷ r) ∎
where
open Tools.Reasoning.PartialOrder ≤-poset
⊛-sub-distribʳ-∧ : (r : M) → (_⊛_▷ r) SubDistributesOverʳ _∧_ by _≤_
⊛-sub-distribʳ-∧ r q p p′ = begin
(p ∧ p′) ⊛ q ▷ r ≡⟨⟩
(r *) · ((p ∧ p′) ∧ q) ≈˘⟨ ·-congˡ (∧-congˡ (∧-idem q)) ⟩
(r *) · ((p ∧ p′) ∧ q ∧ q) ≈˘⟨ ·-congˡ (∧-assoc (p ∧ p′) q q) ⟩
(r *) · (((p ∧ p′) ∧ q) ∧ q) ≈⟨ ·-congˡ (∧-congʳ (∧-assoc p p′ q)) ⟩
(r *) · ((p ∧ p′ ∧ q) ∧ q) ≈⟨ ·-congˡ (∧-congʳ (∧-congˡ (∧-comm p′ q))) ⟩
(r *) · ((p ∧ q ∧ p′) ∧ q) ≈˘⟨ ·-congˡ (∧-congʳ (∧-assoc p q p′)) ⟩
(r *) · (((p ∧ q) ∧ p′) ∧ q) ≈⟨ ·-congˡ (∧-assoc (p ∧ q) p′ q) ⟩
(r *) · ((p ∧ q) ∧ (p′ ∧ q)) ≈⟨ ·-distribˡ-∧ (r *) (p ∧ q) (p′ ∧ q) ⟩
(r *) · (p ∧ q) ∧ (r *) · (p′ ∧ q) ≡⟨⟩
(p ⊛ q ▷ r) ∧ (p′ ⊛ q ▷ r) ∎
where
open Tools.Reasoning.PartialOrder ≤-poset
has-star : Has-star 𝕄
has-star = record
{ _⊛_▷_ = _⊛_▷_
; ⊛-ineq = ⊛-ineq₁ , ⊛-ineq₂
; +-sub-interchangeable-⊛ = +-sub-interchangeable-⊛
; ·-sub-distribʳ-⊛ = ·-sub-distribʳ-⊛
; ⊛-sub-distrib-∧ = λ r → ⊛-sub-distribˡ-∧ r , ⊛-sub-distribʳ-∧ r
}
isModality :
(variant : Modality-variant) →
let open Modality-variant variant in
(T 𝟘ᵐ-allowed → Has-well-behaved-zero 𝕄) →
(T 𝟘ᵐ-allowed → ¬ ⊛-available → ∀ p q → p + q ≤ p) →
Modality
isModality variant 𝟘-well-behaved +-decreasingˡ = record
{ variant = variant
; semiring-with-meet = 𝕄
; 𝟘-well-behaved = 𝟘-well-behaved
; has-star = λ _ → has-star
; +-decreasingˡ = +-decreasingˡ
}
module LowerBounded (∞ : M) (∞-min : (p : M) → ∞ ≤ p) where
open import Graded.Modality.Instances.LowerBounded 𝕄 ∞ ∞-min
using () renaming (_⊛_▷_ to _⊛′_▷_)
⊛′≤⊛ : (p q r : M) → p ⊛′ q ▷ r ≤ p ⊛ q ▷ r
⊛′≤⊛ p q r = ·-monotoneˡ (∞-min (r *))