open import Graded.Modality
module Graded.Context.Properties.Addition
{a} {M : Set a} (𝕄 : Modality M) where
open import Graded.Context 𝕄
open import Graded.Context.Properties.Equivalence 𝕄
open import Graded.Context.Properties.PartialOrder 𝕄
open import Graded.Modality.Properties 𝕄
open import Tools.Algebra
open import Tools.Bool
open import Tools.Nat using (Nat)
open import Tools.Nullary
open import Tools.Product
import Tools.PropositionalEquality as PE
open Modality 𝕄
private
variable
n : Nat
γ γ′ δ δ′ η : Conₘ n
+ᶜ-identityˡ : (γ : Conₘ n) → 𝟘ᶜ +ᶜ γ ≈ᶜ γ
+ᶜ-identityˡ ε = ≈ᶜ-refl
+ᶜ-identityˡ (γ ∙ p) = (+ᶜ-identityˡ γ) ∙ (proj₁ +-identity p)
+ᶜ-identityʳ : (γ : Conₘ n) → γ +ᶜ 𝟘ᶜ ≈ᶜ γ
+ᶜ-identityʳ ε = ≈ᶜ-refl
+ᶜ-identityʳ (γ ∙ p) = (+ᶜ-identityʳ γ) ∙ (proj₂ +-identity p)
+ᶜ-assoc : (γ δ η : Conₘ n) → (γ +ᶜ δ) +ᶜ η ≈ᶜ γ +ᶜ (δ +ᶜ η)
+ᶜ-assoc ε ε ε = ε
+ᶜ-assoc (γ ∙ p) (δ ∙ q) (η ∙ r) = (+ᶜ-assoc γ δ η) ∙ (+-assoc p q r)
+ᶜ-comm : (γ δ : Conₘ n) → γ +ᶜ δ ≈ᶜ δ +ᶜ γ
+ᶜ-comm ε ε = ≈ᶜ-refl
+ᶜ-comm (γ ∙ p) (δ ∙ q) = (+ᶜ-comm γ δ) ∙ (+-comm p q)
+ᶜ-distribˡ-∧ᶜ : (γ δ η : Conₘ n) → γ +ᶜ (δ ∧ᶜ η) ≈ᶜ (γ +ᶜ δ) ∧ᶜ (γ +ᶜ η)
+ᶜ-distribˡ-∧ᶜ ε ε ε = ≈ᶜ-refl
+ᶜ-distribˡ-∧ᶜ (γ ∙ p) (δ ∙ q) (η ∙ r) = (+ᶜ-distribˡ-∧ᶜ γ δ η) ∙ (proj₁ +-distrib-∧ p q r)
+ᶜ-distribʳ-∧ᶜ : (γ δ η : Conₘ n) → (δ ∧ᶜ η) +ᶜ γ ≈ᶜ (δ +ᶜ γ) ∧ᶜ (η +ᶜ γ)
+ᶜ-distribʳ-∧ᶜ ε ε ε = ≈ᶜ-refl
+ᶜ-distribʳ-∧ᶜ (γ ∙ p) (δ ∙ q) (η ∙ r) = (+ᶜ-distribʳ-∧ᶜ γ δ η) ∙ (proj₂ +-distrib-∧ p q r)
+ᶜ-sub-interchangeable-∧ᶜ :
_SubInterchangeable_by_ (Conₘ n) _+ᶜ_ _∧ᶜ_ _≤ᶜ_
+ᶜ-sub-interchangeable-∧ᶜ ε ε ε ε = ε
+ᶜ-sub-interchangeable-∧ᶜ (_ ∙ _) (_ ∙ _) (_ ∙ _) (_ ∙ _) =
+ᶜ-sub-interchangeable-∧ᶜ _ _ _ _ ∙ +-sub-interchangeable-∧ _ _ _ _
+ᶜ-cong : γ ≈ᶜ γ′ → δ ≈ᶜ δ′ → γ +ᶜ δ ≈ᶜ γ′ +ᶜ δ′
+ᶜ-cong ε ε = ≈ᶜ-refl
+ᶜ-cong (γ≈ᶜγ′ ∙ p≡p′) (δ≈ᶜδ′ ∙ q≡q′) =
(+ᶜ-cong γ≈ᶜγ′ δ≈ᶜδ′) ∙ (+-cong p≡p′ q≡q′)
+ᶜ-congˡ : δ ≈ᶜ δ′ → γ +ᶜ δ ≈ᶜ γ +ᶜ δ′
+ᶜ-congˡ δ≈ᶜδ′ = +ᶜ-cong ≈ᶜ-refl δ≈ᶜδ′
+ᶜ-congʳ : γ ≈ᶜ γ′ → γ +ᶜ δ ≈ᶜ γ′ +ᶜ δ
+ᶜ-congʳ γ≈ᶜγ′ = +ᶜ-cong γ≈ᶜγ′ ≈ᶜ-refl
+ᶜ-monotoneˡ : γ ≤ᶜ δ → γ +ᶜ η ≤ᶜ δ +ᶜ η
+ᶜ-monotoneˡ {γ = ε} {ε} {ε} ε = ≤ᶜ-refl
+ᶜ-monotoneˡ {γ = γ ∙ p} {δ ∙ q} {η ∙ r} (γ≤δ ∙ p≤q) = (+ᶜ-monotoneˡ γ≤δ) ∙ (+-monotoneˡ p≤q)
+ᶜ-monotoneʳ : γ ≤ᶜ δ → η +ᶜ γ ≤ᶜ η +ᶜ δ
+ᶜ-monotoneʳ {γ = ε} {ε} {ε} ε = ≤ᶜ-refl
+ᶜ-monotoneʳ {γ = γ ∙ p} {δ ∙ q} {η ∙ r} (γ≤δ ∙ p≤q) = (+ᶜ-monotoneʳ γ≤δ) ∙ (+-monotoneʳ p≤q)
+ᶜ-monotone : γ ≤ᶜ γ′ → δ ≤ᶜ δ′ → γ +ᶜ δ ≤ᶜ γ′ +ᶜ δ′
+ᶜ-monotone γ≤γ′ δ≤δ′ = ≤ᶜ-trans (+ᶜ-monotoneˡ γ≤γ′) (+ᶜ-monotoneʳ δ≤δ′)
+ᶜ-commutativeMonoid : ∀ {n} → IsCommutativeMonoid (Conₘ n) _+ᶜ_ 𝟘ᶜ
+ᶜ-commutativeMonoid = record
{ isMonoid = record
{ isSemigroup = record
{ isMagma = record
{ isEquivalence = PE.isEquivalence
; ∙-cong = PE.cong₂ _+ᶜ_
}
; assoc = λ γ δ η → ≈ᶜ→≡ (+ᶜ-assoc γ δ η)
}
; identity = (λ γ → ≈ᶜ→≡ (+ᶜ-identityˡ γ)) , λ γ → ≈ᶜ→≡ (+ᶜ-identityʳ γ)
}
; comm = λ γ δ → ≈ᶜ→≡ (+ᶜ-comm γ δ)
}
+ᶜ-decreasingˡ : T 𝟘ᵐ-allowed → ¬ ⊛-available → γ +ᶜ δ ≤ᶜ γ
+ᶜ-decreasingˡ {γ = ε} {δ = ε} _ _ = ε
+ᶜ-decreasingˡ {γ = _ ∙ _} {δ = _ ∙ _} ok no-star =
+ᶜ-decreasingˡ ok no-star ∙ +-decreasingˡ ok no-star _ _