open import Tools.Bool using (T; T-not⇔¬-T)
open import Tools.Level
open import Definition.Typed.Restrictions
import Graded.Modality.Dedicated-nr
open import Graded.Modality.Instances.Linear-or-affine
open import Graded.Modality.Variant lzero
open import Graded.Usage.Restrictions
module Graded.Modality.Instances.Linear-or-affine.Bad.No-dedicated-nr
(variant : Modality-variant)
(open Graded.Modality.Dedicated-nr (linear-or-affine variant))
(TR : Type-restrictions (linear-or-affine variant))
(open Type-restrictions TR)
(UR : Usage-restrictions (linear-or-affine variant))
(Π-𝟙-𝟘 : Π-allowed 𝟙 𝟘)
⦃ no-nr : No-dedicated-nr ⦄
where
open Modality-variant variant
open import Tools.Empty
open import Tools.Function
open import Tools.Product
open import Tools.PropositionalEquality
import Tools.Reasoning.PartialOrder
open import Tools.Relation
open import Graded.Modality Linear-or-affine
private
linear-or-affine′ : Modality
linear-or-affine′ = linear-or-affine variant
module M = Modality linear-or-affine′
open import Graded.Context linear-or-affine′
open import Graded.Context.Properties linear-or-affine′
open import Graded.Modality Linear-or-affine
open import Graded.Modality.Instances.Examples TR Π-𝟙-𝟘
open import Graded.Modality.Properties linear-or-affine′
open import Graded.Mode linear-or-affine′
open import Graded.Usage linear-or-affine′ UR
open import Graded.Usage.Inversion linear-or-affine′ UR
▸double : (¬ T 𝟘ᵐ-allowed) ⇔ ε ▸[ 𝟙ᵐ ] double
▸double =
(let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in
λ not-ok →
lamₘ $
natrec-no-nrₘ var (sucₘ var) var
(sub ℕₘ $ begin
𝟘ᶜ ∙ ⌜ 𝟘ᵐ? ⌝ · 𝟘 ≈⟨ ≈ᶜ-refl ∙ M.·-zeroʳ ⌜ 𝟘ᵐ? ⌝ ⟩
𝟘ᶜ ∎)
≤ᶜ-refl
(⊥-elim ∘→ not-ok)
≤ᶜ-refl
≤ᶜ-refl)
, (let open Tools.Reasoning.PartialOrder ≤-poset in
λ ▸λ+ ok →
case inv-usage-lam ▸λ+ of λ {
(invUsageLam ▸+ _) →
case inv-usage-natrec ▸+ of λ {
(invUsageNatrec _ _ _ _ _ invUsageNatrecNr) →
⊥-elim not-nr-and-no-nr;
(invUsageNatrec {η = _ ∙ p} {θ = _ ∙ q} {χ = _ ∙ r}
_ _ _ _ (_ ∙ 𝟙≤r)
(invUsageNatrecNoNr _ r≤₁ _ (_ ∙ r≤₂))) →
case r≤₁ ok of λ {
(_ ∙ r≤₁) →
case lemma p $ begin
𝟙 ≤⟨ 𝟙≤r ⟩
r ≤⟨ r≤₂ ⟩
p + 𝟘 · q + 𝟙 · r ≡⟨ cong (p +_) $
trans (cong₂ _+_ (M.·-zeroˡ q) (M.·-identityˡ _)) $
trans (M.+-identityˡ _) $
𝟙-maximal 𝟙≤r ⟩
p + 𝟙 ∎
of λ {
p≡𝟘 →
case begin
𝟙 ≤⟨ 𝟙≤r ⟩
r ≤⟨ r≤₁ ⟩
p ≡⟨ p≡𝟘 ⟩
𝟘 ∎
of λ () }}}})
where
lemma : ∀ p → 𝟙 ≤ p + 𝟙 → p ≡ 𝟘
lemma 𝟘 refl = refl
lemma 𝟙 ()
lemma ≤𝟙 ()
lemma ≤ω ()
¬▸plus : ¬ ε ▸[ 𝟙ᵐ ] plus
¬▸plus ▸λλ+ =
case inv-usage-lam ▸λλ+ of λ {
(invUsageLam ▸λ+ _) →
case inv-usage-lam ▸λ+ of λ {
(invUsageLam {δ = _ ∙ ≤ω} _ (_ ∙ ()));
(invUsageLam {δ = _ ∙ 𝟘} _ (_ ∙ ()));
(invUsageLam {δ = _ ∙ ≤𝟙} _ (_ ∙ ()));
(invUsageLam {δ = _ ∙ 𝟙} ▸+ _) →
case inv-usage-natrec ▸+ of λ {
(invUsageNatrec _ _ _ _ _ invUsageNatrecNr) →
⊥-elim not-nr-and-no-nr;
(invUsageNatrec {δ = _ ∙ p ∙ _} {χ = _ ∙ q ∙ _}
▸x0 _ _ _ (_ ∙ 𝟙≤q ∙ _)
(invUsageNatrecNoNr (_ ∙ q≤p ∙ _) _ _ _)) →
case inv-usage-var ▸x0 of λ {
(_ ∙ p≤𝟘 ∙ _) →
case begin
𝟙 ≤⟨ 𝟙≤q ⟩
q ≤⟨ q≤p ⟩
p ≤⟨ p≤𝟘 ⟩
𝟘 ∎
of λ () }}}}
where
open Tools.Reasoning.PartialOrder ≤-poset