open import Tools.Level
open import Tools.Relation
module Graded.Modality {a} (M : Set a) where
open import Tools.Algebra M
open import Tools.Bool using (T)
open import Tools.Nullary
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Sum
open import Graded.Modality.Variant a
record Semiring-with-meet : Set a where
infixr 40 _+_
infixr 40 _∧_
infixr 45 _·_
infix 10 _≤_ _<_
field
_+_ : Op₂ M
_·_ : Op₂ M
_∧_ : Op₂ M
𝟘 : M
𝟙 : M
+-·-Semiring : IsSemiring _+_ _·_ 𝟘 𝟙
∧-Semilattice : IsSemilattice _∧_
·-distrib-∧ : _·_ DistributesOver _∧_
+-distrib-∧ : _+_ DistributesOver _∧_
_≤_ : Rel M a
p ≤ q = p ≡ p ∧ q
_<_ : Rel M a
p < q = p ≤ q × p ≢ q
·-distribˡ-∧ : _·_ DistributesOverˡ _∧_
·-distribˡ-∧ = proj₁ ·-distrib-∧
·-distribʳ-∧ : _·_ DistributesOverʳ _∧_
·-distribʳ-∧ = proj₂ ·-distrib-∧
+-distribˡ-∧ : _+_ DistributesOverˡ _∧_
+-distribˡ-∧ = proj₁ +-distrib-∧
+-distribʳ-∧ : _+_ DistributesOverʳ _∧_
+-distribʳ-∧ = proj₂ +-distrib-∧
+-·-Semiring′ : Semiring a a
+-·-Semiring′ = record
{ Carrier = M
; _≈_ = _≡_
; _+_ = _+_
; _*_ = _·_
; 0# = 𝟘
; 1# = 𝟙
; isSemiring = +-·-Semiring
}
open IsSemiring +-·-Semiring public
using (
+-assoc;
+-cong;
+-congˡ;
+-congʳ;
+-identity;
+-identityˡ;
+-identityʳ;
+-comm
)
renaming (
*-assoc to ·-assoc;
*-cong to ·-cong;
*-congˡ to ·-congˡ;
*-congʳ to ·-congʳ;
*-identity to ·-identity;
*-identityˡ to ·-identityˡ;
*-identityʳ to ·-identityʳ;
distrib to ·-distrib-+;
distribˡ to ·-distribˡ-+;
distribʳ to ·-distribʳ-+;
zero to ·-zero;
zeroˡ to ·-zeroˡ;
zeroʳ to ·-zeroʳ
)
open IsSemilattice ∧-Semilattice public
using (∧-cong; ∧-congˡ; ∧-congʳ)
renaming (comm to ∧-comm;
idem to ∧-idem;
assoc to ∧-assoc
)
record Has-well-behaved-zero (𝕄 : Semiring-with-meet) : Set a where
open Semiring-with-meet 𝕄
field
𝟙≢𝟘 : 𝟙 ≢ 𝟘
is-𝟘? : (p : M) → Dec (p ≡ 𝟘)
zero-product : {p q : M} → p · q ≡ 𝟘 → p ≡ 𝟘 ⊎ q ≡ 𝟘
+-positiveˡ : {p q : M} → p + q ≡ 𝟘 → p ≡ 𝟘
∧-positiveˡ : {p q : M} → p ∧ q ≡ 𝟘 → p ≡ 𝟘
record Has-star (r : Semiring-with-meet) : Set a where
open Semiring-with-meet r
infix 50 _⊛_▷_
field
_⊛_▷_ : Op₃ M
⊛-ineq : ((p q r : M) → p ⊛ q ▷ r ≤ q + r · p ⊛ q ▷ r)
× ((p q r : M) → p ⊛ q ▷ r ≤ p)
+-sub-interchangeable-⊛ : (r : M) → _+_ SubInterchangeable (_⊛_▷ r) by _≤_
·-sub-distribʳ-⊛ : (r : M) → _·_ SubDistributesOverʳ (_⊛_▷ r) by _≤_
⊛-sub-distrib-∧ : (r : M) → (_⊛_▷ r) SubDistributesOver _∧_ by _≤_
⊛-ineq₁ : (p q r : M) → p ⊛ q ▷ r ≤ q + r · (p ⊛ q ▷ r)
⊛-ineq₁ = proj₁ ⊛-ineq
⊛-ineq₂ : (p q r : M) → p ⊛ q ▷ r ≤ p
⊛-ineq₂ = proj₂ ⊛-ineq
⊛-sub-distribˡ-∧ : (r : M) → (_⊛_▷ r) SubDistributesOverˡ _∧_ by _≤_
⊛-sub-distribˡ-∧ r = proj₁ (⊛-sub-distrib-∧ r)
⊛-sub-distribʳ-∧ : (r : M) → (_⊛_▷ r) SubDistributesOverʳ _∧_ by _≤_
⊛-sub-distribʳ-∧ r = proj₂ (⊛-sub-distrib-∧ r)
record Modality : Set (lsuc a) where
field
variant : Modality-variant
semiring-with-meet : Semiring-with-meet
open Semiring-with-meet semiring-with-meet public
open Modality-variant variant public
field
𝟘-well-behaved : T 𝟘ᵐ-allowed → Has-well-behaved-zero semiring-with-meet
has-star : ⊛-available → Has-star semiring-with-meet
+-decreasingˡ : T 𝟘ᵐ-allowed → ¬ ⊛-available → ∀ p q → p + q ≤ p