------------------------------------------------------------------------
-- Some examples related to the linearity modality with a "good" nr
-- function.
------------------------------------------------------------------------

open import Tools.Level

import Graded.Modality.Instances.Linearity
open import Graded.Modality.Variant lzero
open import Graded.Usage.Restrictions

module Graded.Modality.Instances.Linearity.Examples.Good.Nr
  -- The modality variant.
  (variant : Modality-variant)
  (open Graded.Modality.Instances.Linearity variant)
  (UR : Usage-restrictions linearityModality)
  where

open import Graded.Restrictions linearityModality
open import Graded.Usage.Restrictions.Natrec linearityModality
open import Graded.Modality Linearity

private
  module M = Modality linearityModality

  -- The "good" nr function is used
  UR′ = nr-available-UR zero-one-many-has-nr UR
  open Usage-restrictions UR′
  instance
    has-nr : Nr-available
    has-nr = Natrec-mode-has-nr.Nr ⦃ zero-one-many-has-nr ⦄

open import Tools.Function
open import Tools.Nat using (Nat)
import Tools.Reasoning.PartialOrder
open import Tools.Product
open import Tools.Relation

open import Definition.Untyped.Nat linearityModality
open import Definition.Untyped Linearity

open import Graded.Context linearityModality
open import Graded.Context.Properties linearityModality
open import Graded.Modality.Properties linearityModality hiding (has-nr)
open import Graded.Mode linearityModality
open import Graded.Usage linearityModality UR′
open import Graded.Usage.Inversion linearityModality UR′
open import Graded.Usage.Properties linearityModality UR′
open import Graded.Usage.Weakening linearityModality UR′

private variable
  n   : Nat
  γ δ : Conₘ _
  m   : Mode
  t u : Term _

private opaque

  -- A lemma used below

  ▸ℕ : 𝟘ᶜ {n = n} ∙ ⌜ 𝟘ᵐ? ⌝ · 𝟘 ▸[ 𝟘ᵐ? ] ℕ
  ▸ℕ = sub-≈ᶜ ℕₘ (≈ᶜ-refl ∙ M.·-zeroʳ _)

opaque

  -- The term double is not well-resourced.

  ¬▸double : ¬ ε ▸[ 𝟙ᵐ ] double
  ¬▸double ▸λ+ =
    case inv-usage-lam ▸λ+ of λ {
      (invUsageLam {δ = ε} ▸+ ε) →
    case inv-usage-natrec-has-nr ▸+ of λ {
      (_ ∙ p , _ ∙ q , _ ∙ r , _ ∙ _
             , ▸x0₁ , _ , ▸x0₂ , _ , (_ ∙ 𝟙≤nr)) →
    case inv-usage-var ▸x0₁ of λ {
      (_ ∙ p≤𝟙) →
    case inv-usage-var ▸x0₂ of λ {
      (_ ∙ r≤𝟙) →
    case begin
      𝟙                  ≤⟨ 𝟙≤nr ⟩
      𝟙 · r + ω · q + p  ≤⟨ +-monotone (·-monotoneʳ {r = 𝟙} r≤𝟙) (+-monotoneʳ p≤𝟙) ⟩
      𝟙 + ω · q + 𝟙      ≡⟨ M.+-congˡ {x = 𝟙} (M.+-comm (ω · q) _) ⟩
      𝟙 + 𝟙 + ω · q      ≡˘⟨ M.+-assoc 𝟙 𝟙 (ω · q) ⟩
      ω                  ∎
    of λ () }}}}
    where
    open Tools.Reasoning.PartialOrder ≤-poset

opaque

  -- A usage rule for plus′.

  ▸plus′ : γ ▸[ m ] t → δ ▸[ m ] u → γ +ᶜ δ ▸[ m ] plus′ t u
  ▸plus′ ▸t ▸u =
    sub (natrecₘ {δ = 𝟘ᶜ} ▸t
          (sub-≈ᶜ (sucₘ var) (≈ᶜ-refl ∙ M.·-zeroʳ _ ∙ M.·-identityʳ _))
          ▸u ▸ℕ)
        (lemma _ _)
    where
    open Tools.Reasoning.PartialOrder ≤-poset
    lemma′ : ∀ p q → p + q ≤ Has-nr.nr zero-one-many-has-nr 𝟘 𝟙 p 𝟘 q
    lemma′ p q = begin
      p + q                                    ≈⟨ M.+-comm p q ⟩
      q + p                                    ≈˘⟨ M.+-congˡ (M.+-identityˡ p) ⟩
      q + 𝟘 + p                                ≈˘⟨ M.+-congʳ (M.·-identityˡ q) ⟩
      𝟙 · q + ω · 𝟘 + p                        ≡⟨⟩
      Has-nr.nr zero-one-many-has-nr 𝟘 𝟙 p 𝟘 q ∎
    lemma : (γ δ : Conₘ n) → γ +ᶜ δ ≤ᶜ nrᶜ ⦃ has-nr = zero-one-many-has-nr ⦄ 𝟘 𝟙 γ 𝟘ᶜ δ
    lemma ε ε = ε
    lemma (γ ∙ p) (δ ∙ q) = lemma γ δ ∙ lemma′ p q

opaque

  -- The term plus is well-resourced.

  ▸plus : ε ▸[ 𝟙ᵐ ] plus
  ▸plus =
    lamₘ $
    lamₘ $
    ▸plus′ var var

opaque
  unfolding f′

  -- A usage rule for f′.

  ▸f′ : γ ▸[ m ] t → δ ▸[ m ] u → γ +ᶜ δ ▸[ m ] f′ t u
  ▸f′ {γ} ▸t ▸u =
    sub (natrecₘ {δ = γ +ᶜ 𝟘ᶜ} ▸t
          (▸plus′ (wkUsage (step (step id)) ▸t)
            (sub-≈ᶜ var (≈ᶜ-refl ∙ M.·-identityʳ _ ∙ M.·-zeroʳ _)))
          ▸u ▸ℕ)
        (lemma _ _)
    where
    open Tools.Reasoning.PartialOrder ≤-poset
    lemma′ : ∀ p q → p + q ≤ Has-nr.nr zero-one-many-has-nr 𝟙 𝟘 p (p + 𝟘) q
    lemma′ p q = begin
      p + q                                          ≡⟨ M.+-comm p q ⟩
      q + p                                          ≡˘⟨ M.∧-idem _ ⟩
      (q + p) ∧ (q + p)                              ≡˘⟨ M.∧-congʳ (M.+-cong (M.·-identityˡ q) (M.+-identityʳ p)) ⟩
      (𝟙 · q + p + 𝟘) ∧ (q + p)                      ≡⟨⟩
      Has-nr.nr zero-one-many-has-nr 𝟙 𝟘 p (p + 𝟘) q ∎
    lemma : (γ δ : Conₘ n) → γ +ᶜ δ ≤ᶜ nrᶜ ⦃ has-nr = zero-one-many-has-nr ⦄ 𝟙 𝟘 γ (γ +ᶜ 𝟘ᶜ) δ
    lemma ε ε = ε
    lemma (γ ∙ p) (δ ∙ q) = lemma γ δ ∙ lemma′ p q

opaque
  unfolding f

  -- The term f is well-resourced.

  ▸f : ε ▸[ 𝟙ᵐ ] f
  ▸f = lamₘ $ lamₘ $ ▸f′ var var

opaque

  -- A usage rule for pred′.

  ▸pred′ : γ ▸[ m ] t → γ ▸[ m ] pred′ t
  ▸pred′ ▸t =
    sub (natrecₘ {δ = 𝟘ᶜ} zeroₘ
      (sub-≈ᶜ var (≈ᶜ-refl ∙ M.·-identityʳ _ ∙ M.·-zeroʳ _))
      ▸t ▸ℕ)
      (lemma _)
    where
    open Tools.Reasoning.PartialOrder ≤-poset
    lemma′ : ∀ p → p ≤ Has-nr.nr zero-one-many-has-nr 𝟙 𝟘 𝟘 𝟘 p
    lemma′ p = begin
      p                                        ≈˘⟨ M.+-identityʳ _ ⟩
      p + 𝟘                                    ≈˘⟨ M.∧-idem _ ⟩
      (p + 𝟘) ∧ (p + 𝟘)                        ≈˘⟨ M.∧-congʳ (M.+-congʳ (M.·-identityˡ p)) ⟩
      (𝟙 · p + 𝟘) ∧ (p + 𝟘)                    ≡⟨⟩
      Has-nr.nr zero-one-many-has-nr 𝟙 𝟘 𝟘 𝟘 p ∎
    lemma : (γ : Conₘ n) → γ ≤ᶜ nrᶜ ⦃ has-nr = zero-one-many-has-nr ⦄ 𝟙 𝟘 𝟘ᶜ 𝟘ᶜ γ
    lemma ε = ε
    lemma (γ ∙ p) = lemma γ ∙ lemma′ p

opaque

  -- The term pred is well-resourced.

  ▸pred : ε ▸[ 𝟙ᵐ ] pred
  ▸pred = lamₘ $ ▸pred′ (sub-≈ᶜ var (ε ∙ M.·-identityʳ _))