import Graded.Modality
module Graded.Context.Properties.Has-well-behaved-zero
{a} {M : Set a}
(open Graded.Modality M)
(𝕄 : Modality)
(open Modality 𝕄)
⦃ 𝟘-well-behaved : Has-well-behaved-zero semiring-with-meet ⦄
where
open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat)
open import Tools.Product as Σ
open import Tools.PropositionalEquality
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
open import Tools.Sum as ⊎
open import Graded.Context 𝕄
open import Graded.Context.Properties.Lookup 𝕄
open import Graded.Context.Properties.Natrec 𝕄
open import Graded.Modality.Nr-instances
open import Graded.Modality.Properties 𝕄
import Graded.Modality.Properties.Star semiring-with-meet as Star
private variable
n : Nat
x : Fin _
γ δ η χ : Conₘ _
p r : M
≤ᶜ→⟨⟩≡𝟘→⟨⟩≡𝟘 : γ ≤ᶜ δ → γ ⟨ x ⟩ ≡ 𝟘 → δ ⟨ x ⟩ ≡ 𝟘
≤ᶜ→⟨⟩≡𝟘→⟨⟩≡𝟘 {γ = γ} {δ = δ} {x = x} =
γ ≤ᶜ δ →⟨ lookup-monotone _ ⟩
γ ⟨ x ⟩ ≤ δ ⟨ x ⟩ →⟨ ≤→≡𝟘→≡𝟘 ⟩
(γ ⟨ x ⟩ ≡ 𝟘 → δ ⟨ x ⟩ ≡ 𝟘) □
opaque
≤ᶜ→≈ᶜ𝟘ᶜ→≈ᶜ𝟘ᶜ : γ ≤ᶜ δ → γ ≈ᶜ 𝟘ᶜ → δ ≈ᶜ 𝟘ᶜ
≤ᶜ→≈ᶜ𝟘ᶜ→≈ᶜ𝟘ᶜ {γ} {δ} γ≤δ =
γ ≈ᶜ 𝟘ᶜ →⟨ ≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₁ ⟩
(∀ x → γ ⟨ x ⟩ ≡ 𝟘) →⟨ ≤ᶜ→⟨⟩≡𝟘→⟨⟩≡𝟘 γ≤δ ∘→_ ⟩
(∀ x → δ ⟨ x ⟩ ≡ 𝟘) →⟨ ≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₂ ⟩
δ ≈ᶜ 𝟘ᶜ □
+ᶜ-positive-⟨⟩ : ∀ γ → (γ +ᶜ δ) ⟨ x ⟩ ≡ 𝟘 → γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘
+ᶜ-positive-⟨⟩ {δ = δ} {x = x} γ =
(γ +ᶜ δ) ⟨ x ⟩ ≡ 𝟘 ≡⟨ cong (_≡ _) (lookup-distrib-+ᶜ γ _ _) ⟩→
γ ⟨ x ⟩ + δ ⟨ x ⟩ ≡ 𝟘 →⟨ +-positive ⟩
γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘 □
opaque
+ᶜ-positive : γ +ᶜ δ ≈ᶜ 𝟘ᶜ → γ ≈ᶜ 𝟘ᶜ × δ ≈ᶜ 𝟘ᶜ
+ᶜ-positive {γ} {δ} =
γ +ᶜ δ ≈ᶜ 𝟘ᶜ →⟨ ≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₁ ⟩
(∀ x → (γ +ᶜ δ) ⟨ x ⟩ ≡ 𝟘) →⟨ +ᶜ-positive-⟨⟩ γ ∘→_ ⟩
(∀ x → γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘) →⟨ (λ hyp → proj₁ ∘→ hyp , proj₂ ∘→ hyp) ⟩
(∀ x → γ ⟨ x ⟩ ≡ 𝟘) × (∀ x → δ ⟨ x ⟩ ≡ 𝟘) →⟨ Σ.map (≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₂) (≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₂) ⟩
γ ≈ᶜ 𝟘ᶜ × δ ≈ᶜ 𝟘ᶜ □
∧ᶜ-positive-⟨⟩ : ∀ γ → (γ ∧ᶜ δ) ⟨ x ⟩ ≡ 𝟘 → γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘
∧ᶜ-positive-⟨⟩ {δ = δ} {x = x} γ =
(γ ∧ᶜ δ) ⟨ x ⟩ ≡ 𝟘 ≡⟨ cong (_≡ _) (lookup-distrib-∧ᶜ γ _ _) ⟩→
γ ⟨ x ⟩ ∧ δ ⟨ x ⟩ ≡ 𝟘 →⟨ ∧-positive ⟩
γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘 □
opaque
∧ᶜ-positive : γ ∧ᶜ δ ≈ᶜ 𝟘ᶜ → γ ≈ᶜ 𝟘ᶜ × δ ≈ᶜ 𝟘ᶜ
∧ᶜ-positive {γ} {δ} =
γ ∧ᶜ δ ≈ᶜ 𝟘ᶜ →⟨ ≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₁ ⟩
(∀ x → (γ ∧ᶜ δ) ⟨ x ⟩ ≡ 𝟘) →⟨ ∧ᶜ-positive-⟨⟩ γ ∘→_ ⟩
(∀ x → γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘) →⟨ (λ hyp → proj₁ ∘→ hyp , proj₂ ∘→ hyp) ⟩
(∀ x → γ ⟨ x ⟩ ≡ 𝟘) × (∀ x → δ ⟨ x ⟩ ≡ 𝟘) →⟨ Σ.map (≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₂) (≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₂) ⟩
γ ≈ᶜ 𝟘ᶜ × δ ≈ᶜ 𝟘ᶜ □
opaque
+ᶜ-⟨⟩-≡-𝟘-→-∧ᶜ-⟨⟩-≡-𝟘 :
∀ γ → (γ +ᶜ δ) ⟨ x ⟩ ≡ 𝟘 → (γ ∧ᶜ δ) ⟨ x ⟩ ≡ 𝟘
+ᶜ-⟨⟩-≡-𝟘-→-∧ᶜ-⟨⟩-≡-𝟘 {δ} {x} γ =
(γ +ᶜ δ) ⟨ x ⟩ ≡ 𝟘 →⟨ +ᶜ-positive-⟨⟩ γ ⟩
γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘 →⟨ uncurry $ cong₂ _∧_ ⟩
γ ⟨ x ⟩ ∧ δ ⟨ x ⟩ ≡ 𝟘 ∧ 𝟘 →⟨ trans (lookup-distrib-∧ᶜ γ _ _) ∘→
flip trans (∧-idem _) ⟩
(γ ∧ᶜ δ) ⟨ x ⟩ ≡ 𝟘 □
·ᶜ-zero-product-⟨⟩ : ∀ γ → (p ·ᶜ γ) ⟨ x ⟩ ≡ 𝟘 → p ≡ 𝟘 ⊎ γ ⟨ x ⟩ ≡ 𝟘
·ᶜ-zero-product-⟨⟩ {p = p} {x = x} γ =
(p ·ᶜ γ) ⟨ x ⟩ ≡ 𝟘 ≡⟨ cong (_≡ _) (lookup-distrib-·ᶜ γ _ _) ⟩→
p · γ ⟨ x ⟩ ≡ 𝟘 →⟨ zero-product ⟩
p ≡ 𝟘 ⊎ γ ⟨ x ⟩ ≡ 𝟘 □
opaque
·ᶜ-zero-product : p ·ᶜ γ ≈ᶜ 𝟘ᶜ → p ≡ 𝟘 ⊎ γ ≈ᶜ 𝟘ᶜ
·ᶜ-zero-product {γ = ε} ε = inj₂ ε
·ᶜ-zero-product {γ = _ ∙ _} (≈𝟘 ∙ ≡𝟘) =
case zero-product ≡𝟘 of λ where
(inj₁ ≡𝟘) → inj₁ ≡𝟘
(inj₂ ≡𝟘) → case ·ᶜ-zero-product ≈𝟘 of λ where
(inj₁ ≡𝟘) → inj₁ ≡𝟘
(inj₂ ≈𝟘) → inj₂ (≈𝟘 ∙ ≡𝟘)
nrᶜ-positive-⟨⟩ :
⦃ has-nr : Has-nr semiring-with-meet ⦄ →
∀ γ →
nrᶜ p r γ δ η ⟨ x ⟩ ≡ 𝟘 →
γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘 × η ⟨ x ⟩ ≡ 𝟘
nrᶜ-positive-⟨⟩ {p = p} {r = r} {δ = δ} {η = η} {x = x} γ =
nrᶜ p r γ δ η ⟨ x ⟩ ≡ 𝟘 ≡⟨ cong (_≡ _) (nrᶜ-⟨⟩ γ) ⟩→
nr p r (γ ⟨ x ⟩) (δ ⟨ x ⟩) (η ⟨ x ⟩) ≡ 𝟘 →⟨ nr-positive ⟩
γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘 × η ⟨ x ⟩ ≡ 𝟘 □
opaque
nrᶜ-positive :
⦃ has-nr : Has-nr semiring-with-meet ⦄ →
nrᶜ p r γ δ η ≈ᶜ 𝟘ᶜ → γ ≈ᶜ 𝟘ᶜ × δ ≈ᶜ 𝟘ᶜ × η ≈ᶜ 𝟘ᶜ
nrᶜ-positive {p} {r} {γ} {δ} {η} =
nrᶜ p r γ δ η ≈ᶜ 𝟘ᶜ →⟨ ≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₁ ⟩
(∀ x → (nrᶜ p r γ δ η) ⟨ x ⟩ ≡ 𝟘) →⟨ nrᶜ-positive-⟨⟩ γ ∘→_ ⟩
(∀ x → γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘 × η ⟨ x ⟩ ≡ 𝟘) →⟨ (λ hyp → proj₁ ∘→ hyp , proj₁ ∘→ proj₂ ∘→ hyp , proj₂ ∘→ proj₂ ∘→ hyp) ⟩
(∀ x → γ ⟨ x ⟩ ≡ 𝟘) × (∀ x → δ ⟨ x ⟩ ≡ 𝟘) × (∀ x → η ⟨ x ⟩ ≡ 𝟘) →⟨ Σ.map (≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₂) (Σ.map (≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₂) (≈ᶜ𝟘ᶜ⇔⟨⟩≡𝟘 .proj₂)) ⟩
γ ≈ᶜ 𝟘ᶜ × δ ≈ᶜ 𝟘ᶜ × η ≈ᶜ 𝟘ᶜ □
⟨⟩≡𝟘→⟨⟩≡𝟘-⊛ :
⦃ has-star : Has-star semiring-with-meet ⦄ →
∀ γ (x : Fin n) →
((γ ∧ᶜ η) ⊛ᶜ δ +ᶜ p ·ᶜ η ▷ r) ⟨ x ⟩ ≡ 𝟘 →
γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘 × η ⟨ x ⟩ ≡ 𝟘
⟨⟩≡𝟘→⟨⟩≡𝟘-⊛ {η = η} {δ = δ} {p = p} {r = r} γ x =
((γ ∧ᶜ η) ⊛ᶜ δ +ᶜ p ·ᶜ η ▷ r) ⟨ x ⟩ ≡ 𝟘 →⟨ trans lemma ⟩
nr p r (γ ⟨ x ⟩) (δ ⟨ x ⟩) (η ⟨ x ⟩) ≡ 𝟘 →⟨ nr-positive ⟩
γ ⟨ x ⟩ ≡ 𝟘 × δ ⟨ x ⟩ ≡ 𝟘 × η ⟨ x ⟩ ≡ 𝟘 □
where
open Tools.Reasoning.PropositionalEquality
instance
has-nr′ : Has-nr semiring-with-meet
has-nr′ = Star.has-nr
lemma =
nr p r (γ ⟨ x ⟩) (δ ⟨ x ⟩) (η ⟨ x ⟩) ≡⟨⟩
(γ ⟨ x ⟩ ∧ η ⟨ x ⟩) ⊛ δ ⟨ x ⟩ + p · η ⟨ x ⟩ ▷ r ≡˘⟨ ⊛ᵣ-congˡ (+-congˡ (lookup-distrib-·ᶜ η _ _)) ⟩
(γ ⟨ x ⟩ ∧ η ⟨ x ⟩) ⊛ δ ⟨ x ⟩ + (p ·ᶜ η) ⟨ x ⟩ ▷ r ≡˘⟨ cong₂ (_⊛_▷ _) (lookup-distrib-∧ᶜ γ _ _) (lookup-distrib-+ᶜ δ _ _) ⟩
(γ ∧ᶜ η) ⟨ x ⟩ ⊛ (δ +ᶜ p ·ᶜ η) ⟨ x ⟩ ▷ r ≡˘⟨ lookup-distrib-⊛ᶜ (γ ∧ᶜ _) _ _ _ ⟩
((γ ∧ᶜ η) ⊛ᶜ δ +ᶜ p ·ᶜ η ▷ r) ⟨ x ⟩ ∎
⟨⟩≡𝟘→⟨⟩≡𝟘-fixpoint :
χ ≤ᶜ δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ →
χ ⟨ x ⟩ ≡ 𝟘 → δ ⟨ x ⟩ ≡ 𝟘
⟨⟩≡𝟘→⟨⟩≡𝟘-fixpoint {χ = χ} {δ = δ} {p = p} {η = η} {r = r} {x = x}
fix ≡𝟘 =
$⟨ lemma ⟩
𝟘 ≤ δ ⟨ x ⟩ + (p ·ᶜ η +ᶜ r ·ᶜ χ) ⟨ x ⟩ →⟨ 𝟘≮ ⟩
δ ⟨ x ⟩ + (p ·ᶜ η +ᶜ r ·ᶜ χ) ⟨ x ⟩ ≡ 𝟘 →⟨ +-positiveˡ ⟩
δ ⟨ x ⟩ ≡ 𝟘 □
where
open Tools.Reasoning.PartialOrder ≤-poset
lemma = begin
𝟘 ≡˘⟨ ≡𝟘 ⟩
χ ⟨ x ⟩ ≤⟨ lookup-monotone _ fix ⟩
(δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ) ⟨ x ⟩ ≡⟨ lookup-distrib-+ᶜ δ _ _ ⟩
δ ⟨ x ⟩ + (p ·ᶜ η +ᶜ r ·ᶜ χ) ⟨ x ⟩ ∎