module Graded.Modality.Instances.Erasure where
open import Tools.Product
open import Tools.PropositionalEquality
data Erasure : Set where
𝟘 ω : Erasure
open import Tools.Algebra Erasure
infixl 40 _+_
infixl 40 _∧_
infixl 45 _·_ _/_
infix 10 _≤_
infix 50 _⊛_▷_
_+_ : Op₂ Erasure
𝟘 + q = q
ω + q = ω
_·_ : Op₂ Erasure
𝟘 · q = 𝟘
ω · q = q
_∧_ : Op₂ Erasure
_∧_ = _+_
_⊛_▷_ : Op₃ Erasure
p ⊛ q ▷ r = p + q
_/_ : Op₂ Erasure
p / ω = p
_ / 𝟘 = ω
_≤_ : (p q : Erasure) → Set
p ≤ q = p ≡ p ∧ q
+-Commutative : Commutative _+_
+-Commutative 𝟘 𝟘 = refl
+-Commutative 𝟘 ω = refl
+-Commutative ω 𝟘 = refl
+-Commutative ω ω = refl
+-Associative : Associative _+_
+-Associative 𝟘 q r = refl
+-Associative ω q r = refl
+-Idempotent : Idempotent _+_
+-Idempotent 𝟘 = refl
+-Idempotent ω = refl
+-LeftIdentity : LeftIdentity 𝟘 _+_
+-LeftIdentity p = refl
+-RightIdentity : RightIdentity 𝟘 _+_
+-RightIdentity 𝟘 = refl
+-RightIdentity ω = refl
+-Identity : Identity 𝟘 _+_
+-Identity = +-LeftIdentity , +-RightIdentity
+-decreasingˡ : (p q : Erasure) → (p + q) ≤ p
+-decreasingˡ 𝟘 𝟘 = refl
+-decreasingˡ 𝟘 ω = refl
+-decreasingˡ ω 𝟘 = refl
+-decreasingˡ ω ω = refl
·-Associative : Associative _·_
·-Associative 𝟘 q r = refl
·-Associative ω q r = refl
·-LeftZero : LeftZero 𝟘 _·_
·-LeftZero p = refl
·-RightZero : RightZero 𝟘 _·_
·-RightZero 𝟘 = refl
·-RightZero ω = refl
·-zero : Zero 𝟘 _·_
·-zero = ·-LeftZero , ·-RightZero
·-LeftIdentity : LeftIdentity ω _·_
·-LeftIdentity p = refl
·-RightIdentity : RightIdentity ω _·_
·-RightIdentity 𝟘 = refl
·-RightIdentity ω = refl
·-Identity : Identity ω _·_
·-Identity = ·-LeftIdentity , ·-RightIdentity
⊛-ineq₁ : (p q r : Erasure) → p ⊛ q ▷ r ≤ q + r · p ⊛ q ▷ r
⊛-ineq₁ 𝟘 𝟘 𝟘 = refl
⊛-ineq₁ 𝟘 𝟘 ω = refl
⊛-ineq₁ 𝟘 ω r = refl
⊛-ineq₁ ω q r = refl
⊛-ineq₂ : (p q r : Erasure) → p ⊛ q ▷ r ≤ p
⊛-ineq₂ 𝟘 𝟘 r = refl
⊛-ineq₂ 𝟘 ω r = refl
⊛-ineq₂ ω q r = refl
+-sub-interchangeable-⊛ : (r : Erasure) → _+_ SubInterchangeable (_⊛_▷ r) by _≤_
+-sub-interchangeable-⊛ r 𝟘 𝟘 𝟘 𝟘 = refl
+-sub-interchangeable-⊛ r 𝟘 𝟘 𝟘 ω = refl
+-sub-interchangeable-⊛ r 𝟘 𝟘 ω q′ = refl
+-sub-interchangeable-⊛ r 𝟘 ω p′ q′ = refl
+-sub-interchangeable-⊛ r ω q p′ q′ = refl
·-sub-distribʳ-⊛ : (r : Erasure) → _·_ SubDistributesOverʳ (_⊛_▷ r) by _≤_
·-sub-distribʳ-⊛ r q 𝟘 p′ = sym (+-Idempotent (p′ · q))
·-sub-distribʳ-⊛ r 𝟘 ω 𝟘 = refl
·-sub-distribʳ-⊛ r 𝟘 ω ω = refl
·-sub-distribʳ-⊛ r ω ω p′ = refl
⊛-sub-distribˡ-∧ : (r : Erasure) → (_⊛_▷ r) SubDistributesOverˡ _∧_ by _≤_
⊛-sub-distribˡ-∧ r 𝟘 q q′ = sym (+-Idempotent (q + q′))
⊛-sub-distribˡ-∧ r ω q q′ = refl
⊛-sub-distribʳ-∧ : (r : Erasure) → (_⊛_▷ r) SubDistributesOverʳ _∧_ by _≤_
⊛-sub-distribʳ-∧ r q ω p′ = refl
⊛-sub-distribʳ-∧ r q 𝟘 ω = refl
⊛-sub-distribʳ-∧ r 𝟘 𝟘 𝟘 = refl
⊛-sub-distribʳ-∧ r ω 𝟘 𝟘 = refl
·-distribˡ-+ : _·_ DistributesOverˡ _+_
·-distribˡ-+ 𝟘 q r = refl
·-distribˡ-+ ω q r = refl
·-distribʳ-+ : _·_ DistributesOverʳ _+_
·-distribʳ-+ p 𝟘 r = refl
·-distribʳ-+ 𝟘 ω 𝟘 = refl
·-distribʳ-+ 𝟘 ω ω = refl
·-distribʳ-+ ω ω r = refl
·-distrib-+ : _·_ DistributesOver _+_
·-distrib-+ = ·-distribˡ-+ , ·-distribʳ-+
+-distribˡ-+ : _+_ DistributesOverˡ _+_
+-distribˡ-+ 𝟘 q r = refl
+-distribˡ-+ ω q r = refl
+-distribʳ-+ : _+_ DistributesOverʳ _+_
+-distribʳ-+ p ω r = refl
+-distribʳ-+ 𝟘 𝟘 r = refl
+-distribʳ-+ ω 𝟘 𝟘 = refl
+-distribʳ-+ ω 𝟘 ω = refl
+-distrib-+ : _+_ DistributesOver _+_
+-distrib-+ = +-distribˡ-+ , +-distribʳ-+
+-Magma : IsMagma _+_
+-Magma = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ _+_
}
+-Semigroup : IsSemigroup _+_
+-Semigroup = record
{ isMagma = +-Magma
; assoc = +-Associative
}
+-Monoid : IsMonoid _+_ 𝟘
+-Monoid = record
{ isSemigroup = +-Semigroup
; identity = +-Identity
}
+-CommutativeMonoid : IsCommutativeMonoid _+_ 𝟘
+-CommutativeMonoid = record
{ isMonoid = +-Monoid
; comm = +-Commutative
}
+-Band : IsBand _+_
+-Band = record
{ isSemigroup = +-Semigroup
; idem = +-Idempotent
}
+-Semilattice : IsSemilattice _+_
+-Semilattice = record
{ isBand = +-Band
; comm = +-Commutative
}
·-Magma : IsMagma _·_
·-Magma = record
{ isEquivalence = isEquivalence
; ∙-cong = cong₂ _·_
}
·-Semigroup : IsSemigroup _·_
·-Semigroup = record
{ isMagma = ·-Magma
; assoc = ·-Associative
}
·-Monoid : IsMonoid _·_ ω
·-Monoid = record
{ isSemigroup = ·-Semigroup
; identity = ·-Identity
}
+-·-SemiringWithoutAnnihilatingZero : IsSemiringWithoutAnnihilatingZero _+_ _·_ 𝟘 ω
+-·-SemiringWithoutAnnihilatingZero = record
{ +-isCommutativeMonoid = +-CommutativeMonoid
; *-isMonoid = ·-Monoid
; distrib = ·-distrib-+
}
+-·-Semiring : IsSemiring _+_ _·_ 𝟘 ω
+-·-Semiring = record
{ isSemiringWithoutAnnihilatingZero = +-·-SemiringWithoutAnnihilatingZero
; zero = ·-zero
}