import Graded.Modality
open import Graded.Usage.Restrictions
module Graded.Usage.Properties.Has-well-behaved-zero
{a} {M : Set a}
(open Graded.Modality M)
(𝕄 : Modality)
(R : Usage-restrictions M)
(open Modality 𝕄)
(𝟘-well-behaved : Has-well-behaved-zero semiring-with-meet)
where
open import Definition.Untyped M using (var)
open import Graded.Context 𝕄
open import Graded.Context.Properties 𝕄
open import Graded.Mode 𝕄
open import Graded.Usage 𝕄 R
open import Graded.Usage.Inversion 𝕄 R
open import Graded.Modality.Properties.Has-well-behaved-zero
semiring-with-meet 𝟘-well-behaved
open import Tools.Fin
open import Tools.Function
open import Tools.PropositionalEquality
open import Tools.Sum
private
variable
γ δ : Conₘ _
x : Fin _
p q r : M
valid-var-usage : γ ▸[ 𝟙ᵐ ] var x → γ ⟨ x ⟩ ≢ 𝟘
valid-var-usage γ▸x γ⟨x⟩≡𝟘 = 𝟘≰𝟙 (lemma _ (inv-usage-var γ▸x) γ⟨x⟩≡𝟘)
where
lemma : ∀ x → γ ≤ᶜ 𝟘ᶜ , x ≔ 𝟙 → γ ⟨ x ⟩ ≡ 𝟘 → 𝟘 ≤ 𝟙
lemma x0 (_ ∙ γ⟨x⟩≤𝟙) refl = γ⟨x⟩≤𝟙
lemma (x +1) (γ≤eᵢ ∙ _) γ⟨x⟩≡𝟘 = lemma x γ≤eᵢ γ⟨x⟩≡𝟘
x◂𝟘∈γ+δˡ : p ≡ 𝟘 → x ◂ p ∈ γ +ᶜ δ → x ◂ 𝟘 ∈ γ
x◂𝟘∈γ+δˡ {x = ()} {ε} _
x◂𝟘∈γ+δˡ {x = x0} {γ ∙ p} {δ ∙ q} p+q≡𝟘 here =
subst (λ x → x0 ◂ x ∈ (γ ∙ p)) (+-positiveˡ p+q≡𝟘) here
x◂𝟘∈γ+δˡ {x = x +1} {γ ∙ p} {δ ∙ q} eq (there d) = there (x◂𝟘∈γ+δˡ eq d)
x◂𝟘∈γ+δʳ : p ≡ 𝟘 → x ◂ p ∈ γ +ᶜ δ → x ◂ 𝟘 ∈ δ
x◂𝟘∈γ+δʳ {γ = γ} {δ} p≡𝟘 d =
x◂𝟘∈γ+δˡ p≡𝟘 (subst (λ x → _ ◂ _ ∈ x) (≈ᶜ→≡ (+ᶜ-comm γ δ)) d)
x◂𝟘∈pγ : q ≡ 𝟘 → p ≢ 𝟘 → x ◂ q ∈ p ·ᶜ γ → x ◂ 𝟘 ∈ γ
x◂𝟘∈pγ {x = ()} {ε} q≡𝟘 p≢𝟘 d
x◂𝟘∈pγ {x = x0} {γ ∙ r} pr≡𝟘 p≢𝟘 here = case zero-product pr≡𝟘 of λ where
(inj₁ p≡𝟘) → ⊥-elim (p≢𝟘 p≡𝟘)
(inj₂ refl) → here
x◂𝟘∈pγ {x = x +1} {γ ∙ r} q≡𝟘 p≢𝟘 (there d) =
there (x◂𝟘∈pγ q≡𝟘 p≢𝟘 d)
x◂𝟘∈γ∧δˡ : p ≡ 𝟘 → x ◂ p ∈ γ ∧ᶜ δ → x ◂ 𝟘 ∈ γ
x◂𝟘∈γ∧δˡ {x = ()} {ε} _
x◂𝟘∈γ∧δˡ {x = x0} {γ ∙ p} {δ ∙ q} p∧q≡𝟘 here =
subst (λ x → x0 ◂ x ∈ (γ ∙ p)) (∧-positiveˡ p∧q≡𝟘) here
x◂𝟘∈γ∧δˡ {x = x +1} {γ ∙ p} {δ ∙ q} eq (there d) =
there (x◂𝟘∈γ∧δˡ eq d)
x◂𝟘∈γ∧δʳ : p ≡ 𝟘 → x ◂ p ∈ γ ∧ᶜ δ → x ◂ 𝟘 ∈ δ
x◂𝟘∈γ∧δʳ {γ = γ} {δ} p≡𝟘 d =
x◂𝟘∈γ∧δˡ p≡𝟘 (subst (λ x → _ ◂ _ ∈ x) (≈ᶜ→≡ (∧ᶜ-comm γ δ)) d)
x◂𝟘∈γ⊛δˡ :
⦃ has-star : Has-star semiring-with-meet ⦄ →
p ≡ 𝟘 → x ◂ p ∈ γ ⊛ᶜ δ ▷ r → x ◂ 𝟘 ∈ γ
x◂𝟘∈γ⊛δˡ {x = x0} {γ ∙ p} {δ ∙ q} p⊛q≡𝟘 here =
subst (λ x → _ ◂ x ∈ γ ∙ p) (⊛≡𝟘ˡ p⊛q≡𝟘) here
x◂𝟘∈γ⊛δˡ {x = x +1} {γ ∙ p} {δ ∙ q} eq (there d) =
there (x◂𝟘∈γ⊛δˡ eq d)
x◂𝟘∈γ⊛δʳ :
⦃ has-star : Has-star semiring-with-meet ⦄ →
p ≡ 𝟘 → x ◂ p ∈ γ ⊛ᶜ δ ▷ r → x ◂ 𝟘 ∈ δ
x◂𝟘∈γ⊛δʳ {x = x0} {γ ∙ p} {δ ∙ q} p⊛q≡𝟘 here =
subst (λ x → _ ◂ x ∈ δ ∙ q) (⊛≡𝟘ʳ p⊛q≡𝟘) here
x◂𝟘∈γ⊛δʳ {x = x +1} {γ ∙ p} {δ ∙ q} eq (there d) =
there (x◂𝟘∈γ⊛δʳ eq d)
x◂𝟘∈γ≤δ : x ◂ 𝟘 ∈ γ → γ ≤ᶜ δ → x ◂ 𝟘 ∈ δ
x◂𝟘∈γ≤δ {δ = δ ∙ p} here (γ≤δ ∙ 𝟘≤p) rewrite 𝟘≮ 𝟘≤p = here
x◂𝟘∈γ≤δ {δ = δ ∙ p} (there d) (γ≤δ ∙ _) = there (x◂𝟘∈γ≤δ d γ≤δ)