module Graded.Modality.Instances.Erasure.Modality where
open import Tools.Level
open import Tools.Product
open import Tools.PropositionalEquality
open import Tools.Relation
open import Tools.Sum
open import Graded.Modality.Instances.Erasure
import Graded.Modality.Properties.Star as Star
open import Graded.Modality.Variant lzero
open import Graded.Modality Erasure public
erasure-semiring-with-meet : Semiring-with-meet
erasure-semiring-with-meet = record
{ _+_ = _+_
; _·_ = _·_
; _∧_ = _∧_
; 𝟘 = 𝟘
; 𝟙 = ω
; ω = ω
; ω·+≤ω·ʳ = λ {p = p} → +-decreasingʳ p
; ω≤𝟙 = refl
; is-𝟘? = _≟ 𝟘
; +-·-Semiring = +-·-Semiring
; ∧-Semilattice = +-Semilattice
; ·-distrib-∧ = ·-distrib-+
; +-distrib-∧ = +-distrib-+
}
instance
erasure-has-well-behaved-zero :
Has-well-behaved-zero erasure-semiring-with-meet
erasure-has-well-behaved-zero = record
{ non-trivial = λ ()
; zero-product = λ where
{p = 𝟘} {q = 𝟘} _ → inj₁ refl
{p = 𝟘} {q = ω} _ → inj₁ refl
{p = ω} {q = 𝟘} _ → inj₂ refl
{p = ω} {q = ω} ()
; +-positiveˡ = λ where
{p = 𝟘} _ → refl
{p = ω} {q = 𝟘} ()
{p = ω} {q = ω} ()
; ∧-positiveˡ = λ where
{p = 𝟘} _ → refl
{p = ω} ()
}
instance
erasure-has-star : Has-star erasure-semiring-with-meet
erasure-has-star = record
{ _⊛_▷_ = _⊛_▷_
; ⊛-ineq = ⊛-ineq₁ , ⊛-ineq₂
; +-sub-interchangeable-⊛ = +-sub-interchangeable-⊛
; ·-sub-distribʳ-⊛ = ·-sub-distribʳ-⊛
; ⊛-sub-distrib-∧ = λ r → ⊛-sub-distribˡ-∧ r , ⊛-sub-distribʳ-∧ r
}
erasure-has-nr : Has-nr erasure-semiring-with-meet
erasure-has-nr = Star.has-nr erasure-semiring-with-meet
nr : Erasure → Erasure → Erasure → Erasure → Erasure → Erasure
nr = Has-nr.nr erasure-has-nr
ErasureModality : Modality-variant → Modality
ErasureModality variant = record
{ variant = variant
; semiring-with-meet = erasure-semiring-with-meet
; has-nr = λ _ → erasure-has-nr
; 𝟘-well-behaved = λ _ → erasure-has-well-behaved-zero
}