------------------------------------------------------------------------
-- Inversion lemmata for γ ▸[ m ] t
------------------------------------------------------------------------

import Graded.Modality
open import Graded.Usage.Restrictions

module Graded.Usage.Inversion
  {a} {M : Set a}
  (open Graded.Modality M)
  (𝕄 : Modality)
  (R : Usage-restrictions M)
  where

open Modality 𝕄
open Usage-restrictions R

open import Graded.Context 𝕄
open import Graded.Context.Properties 𝕄
open import Graded.Usage 𝕄 R
open import Graded.Modality.Dedicated-star 𝕄
open import Graded.Modality.Dedicated-star.Instance
open import Graded.Mode 𝕄
open import Definition.Untyped M hiding (_∙_)

open import Tools.Nat using (Nat; 1+)
open import Tools.Nullary
open import Tools.PropositionalEquality as PE

private
  variable
    k n : Nat
    γ χ : Conₘ n
    p q r : M
    A F t u z n' : Term n
    G : Term (1+ n)
    m : Mode
    b : BinderMode
    s : SigmaMode

-- If γ ▸[ m ] U then γ ≤ᶜ 𝟘ᶜ.

inv-usage-U : γ ▸[ m ] U → γ ≤ᶜ 𝟘ᶜ
inv-usage-U Uₘ = ≤ᶜ-refl
inv-usage-U (sub γ▸U γ≤δ) = ≤ᶜ-trans γ≤δ (inv-usage-U γ▸U)

-- If γ ▸[ m ] ℕ then γ ≤ᶜ 𝟘ᶜ.

inv-usage-ℕ : γ ▸[ m ] ℕ → γ ≤ᶜ 𝟘ᶜ
inv-usage-ℕ ℕₘ = ≤ᶜ-refl
inv-usage-ℕ (sub γ▸ℕ γ≤δ) = ≤ᶜ-trans γ≤δ (inv-usage-ℕ γ▸ℕ)

-- If γ ▸[ m ] Empty then γ ≤ᶜ 𝟘ᶜ.

inv-usage-Empty : γ ▸[ m ] Empty → γ ≤ᶜ 𝟘ᶜ
inv-usage-Empty Emptyₘ = ≤ᶜ-refl
inv-usage-Empty (sub γ▸⊥ γ≤δ) = ≤ᶜ-trans γ≤δ (inv-usage-Empty γ▸⊥)

-- If γ ▸[ m ] Unit then γ ≤ᶜ 𝟘ᶜ.

inv-usage-Unit : γ ▸[ m ] Unit → γ ≤ᶜ 𝟘ᶜ
inv-usage-Unit Unitₘ = ≤ᶜ-refl
inv-usage-Unit (sub γ▸⊤ γ≤δ) = ≤ᶜ-trans γ≤δ (inv-usage-Unit γ▸⊤)


record InvUsageΠΣ {n} (γ : Conₘ n) (m : Mode) (b : BinderMode) (p q : M)
                 (F : Term n) (G : Term (1+ n)) : Set a where
  constructor invUsageΠΣ
  field
    {δ η} : Conₘ n
    δ▸F   : δ ▸[ m ᵐ· p ] F
    η▸G   : η ∙ ⌜ m ⌝ · q ▸[ m ] G
    γ≤δ+η : γ ≤ᶜ δ +ᶜ η

-- If γ ▸[ m ] ⟨ b ⟩ p , q ▷ F ▹ G then δ ▸[ m ᵐ· p ] F,
-- η ∙ ⌜ m ⌝ · q ▸[ m ] G and γ ≤ᶜ δ +ᶜ η.

inv-usage-ΠΣ : γ ▸[ m ] ΠΣ⟨ b ⟩ p , q ▷ F ▹ G → InvUsageΠΣ γ m b p q F G
inv-usage-ΠΣ (ΠΣₘ γ▸F δ▸G) = invUsageΠΣ γ▸F δ▸G ≤ᶜ-refl
inv-usage-ΠΣ (sub γ▸Π γ≤γ′) with inv-usage-ΠΣ γ▸Π
… | invUsageΠΣ δ▸F η▸G γ′≤δ+η =
  invUsageΠΣ δ▸F η▸G (≤ᶜ-trans γ≤γ′ γ′≤δ+η)

-- If γ ▸[ m ] var x then γ ≤ᶜ (𝟘ᶜ , x ≔ ⌜ m ⌝).

inv-usage-var : ∀ {x} {γ : Conₘ n}
              → γ ▸[ m ] var x → γ ≤ᶜ (𝟘ᶜ , x ≔ ⌜ m ⌝)
inv-usage-var var = ≤ᶜ-refl
inv-usage-var (sub γ▸x γ≤γ′) with inv-usage-var γ▸x
... | γ′≤δ = ≤ᶜ-trans γ≤γ′ γ′≤δ


record InvUsageLam
         {n} (γ : Conₘ n) (m : Mode) (p : M) (t : Term (1+ n)) :
         Set a where
  constructor invUsageLam
  field
    {δ} : Conₘ n
    δ▸t : δ ∙ ⌜ m ⌝ · p ▸[ m ] t
    γ≤δ : γ ≤ᶜ δ

-- If γ ▸[ m ] lam p t then δ ∙ ⌜ m ⌝ · p ▸[ m ] t and γ ≤ᶜ δ.

inv-usage-lam : γ ▸[ m ] lam p t → InvUsageLam γ m p t
inv-usage-lam (lamₘ γ▸λpt) = invUsageLam γ▸λpt ≤ᶜ-refl
inv-usage-lam (sub γ′▸λpt γ≤γ′) with inv-usage-lam γ′▸λpt
... | invUsageLam δ▸t γ′≤δ = invUsageLam δ▸t (≤ᶜ-trans γ≤γ′ γ′≤δ)


record InvUsageApp
         {n} (γ : Conₘ n) (t : Term n) (m : Mode) (p : M) (u : Term n) :
         Set a where
  constructor invUsageApp
  field
    {δ η} : Conₘ n
    δ▸t   : δ ▸[ m ] t
    η▸u   : η ▸[ m ᵐ· p ] u
    γ≤δ+η : γ ≤ᶜ δ +ᶜ p ·ᶜ η

-- If γ ▸[ m ] t ∘⟨ p ⟩ u then δ ▸[ m ] t, η ▸[ m ᵐ· p ] u and
-- γ ≤ᶜ δ +ᶜ p ·ᶜ η.

inv-usage-app : γ ▸[ m ] t ∘⟨ p ⟩ u → InvUsageApp γ t m p u
inv-usage-app (γ▸t ∘ₘ δ▸u) = invUsageApp γ▸t δ▸u ≤ᶜ-refl
inv-usage-app (sub γ▸t∘p▷u γ′≤γ) with inv-usage-app γ▸t∘p▷u
... | invUsageApp δ▸t η▸u γ≤δ+pη = invUsageApp δ▸t η▸u (≤ᶜ-trans γ′≤γ γ≤δ+pη)


record InvUsageProdᵣ
         {n} (γ : Conₘ n) (m : Mode) (p : M) (t u : Term n) :
         Set a where
  constructor invUsageProdᵣ
  field
    {δ η} : Conₘ n
    δ▸t   : δ ▸[ m ᵐ· p ] t
    η▸u   : η ▸[ m ] u
    γ≤γ′  : γ ≤ᶜ p ·ᶜ δ +ᶜ η

-- If γ ▸[ m ] prodᵣ p t u then δ ▸[ m ᵐ· p ] t, η ▸[ m ] u and
-- γ ≤ᶜ p ·ᶜ δ +ᶜ η.

inv-usage-prodᵣ : γ ▸[ m ] prodᵣ p t u → InvUsageProdᵣ γ m p t u
inv-usage-prodᵣ (prodᵣₘ γ▸t δ▸u) = invUsageProdᵣ γ▸t δ▸u ≤ᶜ-refl
inv-usage-prodᵣ (sub γ▸tu γ≤γ′) with inv-usage-prodᵣ γ▸tu
... | invUsageProdᵣ δ▸t η▸u γ′≤γ″ =
  invUsageProdᵣ δ▸t η▸u (≤ᶜ-trans γ≤γ′ γ′≤γ″)

record InvUsageProdₚ
         {n} (γ : Conₘ n) (m : Mode) (p : M) (t u : Term n) :
         Set a where
  constructor invUsageProdₚ
  field
    {δ η}  : Conₘ n
    δ▸t    : δ ▸[ m ᵐ· p ] t
    η▸u    : η ▸[ m ] u
    γ≤pδ∧η : γ ≤ᶜ p ·ᶜ δ ∧ᶜ η

-- If γ ▸[ m ] prod p t u then δ ▸[ m ᵐ· p ] t, η ▸[ m ] u and
-- γ ≤ᶜ p ·ᶜ δ ∧ᶜ η.

inv-usage-prodₚ : γ ▸[ m ] prodₚ p t u → InvUsageProdₚ γ m p t u
inv-usage-prodₚ (prodₚₘ γ▸t γ▸u) = invUsageProdₚ γ▸t γ▸u ≤ᶜ-refl
inv-usage-prodₚ (sub δ▸tu γ≤γ′) with inv-usage-prodₚ δ▸tu
... | invUsageProdₚ δ▸t δ▸u γ′≤δ = invUsageProdₚ δ▸t δ▸u (≤ᶜ-trans γ≤γ′ γ′≤δ)


record InvUsageFst
         {n} (γ : Conₘ n) (m : Mode) (p : M) (t : Term n) :
         Set a where
  constructor invUsageFst
  field
    {δ}          : Conₘ n
    m′           : Mode
    m≡m′ᵐ·p      : m ≡ m′ ᵐ· p
    δ▸t          : δ ▸[ m ] t
    γ≤δ          : γ ≤ᶜ δ
    mp-condition : m PE.≡ 𝟙ᵐ → p ≤ 𝟙

-- If γ ▸[ m ] fst t then m ≡ m′ ᵐ· p, δ ▸[ m ] t and γ ≤ᶜ δ, and
-- furthermore if m ≡ 𝟙 then p ≤ 𝟙.

inv-usage-fst : γ ▸[ m ] fst p t → InvUsageFst γ m p t
inv-usage-fst (fstₘ m ▸t PE.refl ok) =
  invUsageFst m PE.refl ▸t ≤ᶜ-refl ok
inv-usage-fst (sub ▸t γ≤γ′) with inv-usage-fst ▸t
... | invUsageFst m m≡ ▸t γ′≤ ok =
  invUsageFst m m≡ ▸t (≤ᶜ-trans γ≤γ′ γ′≤) ok

record InvUsageSnd
         {n} (γ : Conₘ n) (m : Mode) (t : Term n) : Set a where
  constructor invUsageSnd
  field
    {δ} : Conₘ n
    δ▸t : δ ▸[ m ] t
    γ≤δ : γ ≤ᶜ δ

-- If γ ▸[ m ] snd t then δ ▸[ m ] t and γ ≤ᶜ δ.

inv-usage-snd : γ ▸[ m ] snd p t → InvUsageSnd γ m t
inv-usage-snd (sndₘ ▸t) = invUsageSnd ▸t ≤ᶜ-refl
inv-usage-snd (sub ▸t γ≤γ′) with inv-usage-snd ▸t
... | invUsageSnd ▸t γ′≤ = invUsageSnd ▸t (≤ᶜ-trans γ≤γ′ γ′≤)

record InvUsageProdrec
         {n} (γ : Conₘ n) (m : Mode) (r p q : M) (A : Term (1+ n))
         (t : Term n) (u : Term (1+ (1+ n))) : Set a where
  constructor invUsageProdrec
  field
    {δ η θ} : Conₘ n
    δ▸t : δ ▸[ m ᵐ· r ] t
    η▸u : η ∙ ⌜ m ⌝ · r · p ∙ ⌜ m ⌝ · r ▸[ m ] u
    θ▸A : θ ∙ ⌜ 𝟘ᵐ? ⌝ · q ▸[ 𝟘ᵐ? ] A
    P : Prodrec-allowed r p q
    γ≤γ′ : γ ≤ᶜ r ·ᶜ δ +ᶜ η

-- If γ ▸[ m ] prodrec r p q A t u then δ ▸[ m ᵐ· r ] t,
-- η ∙ ⌜ m ⌝ · r · p ∙ ⌜ m ⌝ · r ▸[ m ] u, θ ∙ ⌜ 𝟘ᵐ? ⌝ · q ▸[ 𝟘ᵐ? ] A,
-- Prodrec-allowed r p q and γ ≤ᶜ r ·ᶜ δ +ᶜ η.

inv-usage-prodrec :
  γ ▸[ m ] prodrec r p q A t u → InvUsageProdrec γ m r p q A t u
inv-usage-prodrec (prodrecₘ γ▸t δ▸u η▸A P) = invUsageProdrec γ▸t δ▸u η▸A P ≤ᶜ-refl
inv-usage-prodrec (sub γ▸t γ≤γ′) with inv-usage-prodrec γ▸t
... | invUsageProdrec δ▸t η▸u θ▸A P γ′≤γ″ = invUsageProdrec δ▸t η▸u θ▸A P (≤ᶜ-trans γ≤γ′ γ′≤γ″)

-- If γ ▸[ m ] zero then γ ≤ᶜ 𝟘ᶜ.

inv-usage-zero : γ ▸[ m ] zero → γ ≤ᶜ 𝟘ᶜ
inv-usage-zero zeroₘ = ≤ᶜ-refl
inv-usage-zero (sub  δ▸zero γ≤δ) = ≤ᶜ-trans γ≤δ (inv-usage-zero δ▸zero)


record InvUsageSuc
         {n} (γ : Conₘ n) (m : Mode) (t : Term n) : Set a where
  constructor invUsageSuc
  field
    {δ} : Conₘ n
    δ▸t : δ ▸[ m ] t
    γ≤δ : γ ≤ᶜ δ

-- If γ ▸[ m ] suc t then δ ▸[ m ] t and γ ≤ᶜ δ.

inv-usage-suc : γ ▸[ m ] suc t → InvUsageSuc γ m t
inv-usage-suc (sucₘ γ▸t) = invUsageSuc γ▸t ≤ᶜ-refl
inv-usage-suc (sub γ▸st γ≤γ′) with inv-usage-suc γ▸st
... | invUsageSuc δ▸t γ′≤δ = invUsageSuc δ▸t (≤ᶜ-trans γ≤γ′ γ′≤δ)


data InvUsageNatrec′ (p r : M) (γ η δ : Conₘ n) : Conₘ n → Set a where
  invUsageNatrecStar :
    ⦃ has-star : Dedicated-star ⦄ →
    InvUsageNatrec′ p r γ η δ ((γ ∧ᶜ η) ⊛ᶜ (δ +ᶜ p ·ᶜ η) ▷ r)
  invUsageNatrecNoStar :
    ⦃ no-star : No-dedicated-star ⦄ →
    χ ≤ᶜ γ ∧ᶜ η ∧ᶜ (δ +ᶜ p ·ᶜ η +ᶜ r ·ᶜ χ) →
    InvUsageNatrec′ p r γ η δ χ

data InvUsageNatrec
       (γ : Conₘ k) (m : Mode) (p q r : M) (A : Term (1+ k))
       (z : Term k) (s : Term (1+ (1+ k))) (n : Term k) : Set a where
  invUsageNatrec :
    {δ η θ φ χ : Conₘ k} →
    δ ▸[ m ] z →
    η ∙ ⌜ m ⌝ · p ∙ ⌜ m ⌝ · r ▸[ m ] s →
    θ ▸[ m ] n →
    φ ∙ ⌜ 𝟘ᵐ? ⌝ · q ▸[ 𝟘ᵐ? ] A →
    γ ≤ᶜ χ →
    InvUsageNatrec′ p r δ θ η χ →
    InvUsageNatrec γ m p q r A z s n

-- An inversion lemma for natrec.

inv-usage-natrec :
  {s : Term (1+ (1+ k))} {n : Term k} →
  γ ▸[ m ] natrec p q r G z s n → InvUsageNatrec γ m p q r G z s n
inv-usage-natrec (natrecₘ δ▸z δ▸s η▸n θ▸A) =
  invUsageNatrec δ▸z δ▸s η▸n θ▸A ≤ᶜ-refl invUsageNatrecStar
inv-usage-natrec (natrec-no-starₘ ▸z ▸s ▸n ▸A fix) =
  invUsageNatrec ▸z ▸s ▸n ▸A ≤ᶜ-refl (invUsageNatrecNoStar fix)
inv-usage-natrec (sub γ▸natrec γ≤γ′) with inv-usage-natrec γ▸natrec
... | invUsageNatrec δ▸z η▸s θ▸n φ▸A γ′≤γ″ extra =
  invUsageNatrec δ▸z η▸s θ▸n φ▸A (≤ᶜ-trans γ≤γ′ γ′≤γ″) extra

record InvUsageemptyrec
         {n} (γ : Conₘ n) (m : Mode) (p : M) (A t : Term n) :
         Set a where
  constructor invUsageemptyrec
  field
    {δ η} : Conₘ n
    δ▸t  : δ ▸[ m ᵐ· p ] t
    η▸A  : η ▸[ 𝟘ᵐ? ] A
    γ≤pδ : γ ≤ᶜ p ·ᶜ δ

-- If γ ▸[ m ] emptyrec p A t then δ ▸[ m ᵐ· p ] t, η ▸[ 𝟘ᵐ? ] A and
-- γ ≤ᶜ p ·ᶜ δ.

inv-usage-emptyrec :
  γ ▸[ m ] emptyrec p A t → InvUsageemptyrec γ m p A t
inv-usage-emptyrec (emptyrecₘ δ▸t η▸A) = invUsageemptyrec δ▸t η▸A ≤ᶜ-refl
inv-usage-emptyrec (sub γ▸et γ≤γ′) with inv-usage-emptyrec γ▸et
... | invUsageemptyrec δ▸t η▸A γ′≤δ = invUsageemptyrec δ▸t η▸A (≤ᶜ-trans γ≤γ′ γ′≤δ)

-- If γ ▸[ m ] star then γ ≤ᶜ 𝟘ᶜ.

inv-usage-star : γ ▸[ m ] star → γ ≤ᶜ 𝟘ᶜ
inv-usage-star starₘ = ≤ᶜ-refl
inv-usage-star (sub  δ▸star γ≤δ) = ≤ᶜ-trans γ≤δ (inv-usage-star δ▸star)