------------------------------------------------------------------------
-- Some examples related to the erasure modality and extraction
------------------------------------------------------------------------

open import Tools.Level

open import Graded.Modality.Instances.Erasure
open import Graded.Modality.Variant lzero
open import Graded.Usage.Restrictions
open import Definition.Typed.Restrictions

module Graded.Erasure.Examples
  {p q r}
  (variant : Modality-variant)
  (TR : Type-restrictions Erasure)
  (open Type-restrictions TR)
  (UR : Usage-restrictions Erasure)
  -- It is assumed that "Π 𝟘 , p" is allowed.
  (Π-𝟘-ok : Π-allowed 𝟘 p)
  -- It is assumed that "Π ω , q" is allowed.
  (Π-ω-ok : Π-allowed ω q)
  -- It is assumed that "Σₚ ω , r" is allowed.
  (Σₚ-ω-ok : Σₚ-allowed ω r)
  -- It is assumed that Unit is allowed.
  (Unit-ok : Unit-allowed)
  where

open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.Nat using (Nat; 1+)
open import Tools.Nullary
open import Tools.Product
import Tools.PropositionalEquality as PE
import Tools.Reasoning.PartialOrder
import Tools.Reasoning.PropositionalEquality
open import Tools.Sum as ⊎ using (_⊎_; inj₁; inj₂)

open import Definition.Typed TR as DT hiding (id)
open import Definition.Typed.Consequences.Reduction TR
open import Definition.Typed.Consequences.Substitution TR
open import Definition.Typed.Consequences.Syntactic TR
open import Definition.Typed.EqRelInstance TR
open import Definition.Typed.Eta-long-normal-form TR
open import Definition.Typed.Properties TR
import Definition.Typed.Weakening TR as W
open import Definition.Untyped Erasure as U hiding (id; head; _∷_)
open import Definition.Untyped.Properties Erasure

open import Graded.Modality.Instances.Erasure.Modality

private

  EM : Modality
  EM = ErasureModality variant

  module EM = Modality EM

open import Graded.Modality.Instances.Erasure.Properties variant

open import Graded.Context EM
open import Graded.Erasure.Consequences.Soundness
  EM TR UR erasure-has-well-behaved-zero
open import Graded.Erasure.Extraction
  EM (Has-well-behaved-zero.is-𝟘? erasure-has-well-behaved-zero)
import Graded.Erasure.SucRed TR as S
import Graded.Erasure.Target as T
import Graded.Erasure.Target.Properties as TP
open import Graded.Mode EM
open import Graded.Usage EM UR
open import Graded.Usage.Inversion EM UR
open import Graded.Usage.Properties EM UR
open import Graded.Usage.Weakening EM UR

private variable
  n       : Nat
  Γ       : Con Term _
  A t u v : Term _
  γ       : Conₘ _

private

  -- Some lemmas used below.

  ⊢ℕ : ⊢ ε ∙ ℕ
  ⊢ℕ = ε ∙ ℕⱼ ε

  ⊢U : ⊢ ε ∙ U
  ⊢U = ε ∙ Uⱼ ε

  U⊢0 : ε ∙ U ⊢ var x0
  U⊢0 = univ (var ⊢U here)

  ⊢U0 : ⊢ ε ∙ U ∙ var x0
  ⊢U0 = ⊢U ∙ U⊢0

  U⊢id : ε ∙ U ⊢ lam ω (var x0) ∷ Π ω , q ▷ var x0 ▹ var x1
  U⊢id = lamⱼ U⊢0 (var ⊢U0 here) Π-ω-ok

  ΓU⊢id : ⊢ Γ → Γ ∙ U ⊢ lam ω (var x0) ∷ Π ω , q ▷ var x0 ▹ var x1
  ΓU⊢id ε = U⊢id
  ΓU⊢id (⊢Γ ∙ ⊢A) =
    W.wkTerm (W.lift (W.step W.id))
             (⊢Γ ∙ ⊢A ∙ Uⱼ (⊢Γ ∙ ⊢A))
             (ΓU⊢id ⊢Γ)

  U⊢ℕ : ε ∙ U ⊢ ℕ
  U⊢ℕ = ℕⱼ ⊢U

  ⊢Uℕ : ⊢ ε ∙ U ∙ ℕ
  ⊢Uℕ = ⊢U ∙ U⊢ℕ

  ⊢Uℕℕ : ⊢ ε ∙ U ∙ ℕ ∙ ℕ
  ⊢Uℕℕ = ⊢Uℕ ∙ ℕⱼ ⊢Uℕ

  Uℕℕ⊢U : ε ∙ U ∙ ℕ ∙ ℕ ⊢ U
  Uℕℕ⊢U = Uⱼ ⊢Uℕℕ

  ⊢UℕℕU : ⊢ ε ∙ U ∙ ℕ ∙ ℕ ∙ U
  ⊢UℕℕU = ⊢Uℕℕ ∙ Uℕℕ⊢U

  UℕℕU⊢3 : ε ∙ U ∙ ℕ ∙ ℕ ∙ U ⊢ var x3 ∷ U
  UℕℕU⊢3 = var ⊢UℕℕU (there (there (there here)))

  ⊢UℕℕU3 : ⊢ ε ∙ U ∙ ℕ ∙ ℕ ∙ U ∙ var x3
  ⊢UℕℕU3 = ⊢UℕℕU ∙ univ UℕℕU⊢3

  ⊢ℕℕ : ⊢ ε ∙ ℕ ∙ ℕ
  ⊢ℕℕ = ⊢ℕ ∙ ℕⱼ ⊢ℕ

  ℕℕ⊢U : ε ∙ ℕ ∙ ℕ ⊢ U
  ℕℕ⊢U = Uⱼ ⊢ℕℕ

  ⊢ℕℕU : ⊢ ε ∙ ℕ ∙ ℕ ∙ U
  ⊢ℕℕU = ⊢ℕℕ ∙ ℕℕ⊢U

------------------------------------------------------------------------
-- A polymorphic identity function

-- A polymorphic identity function with an erased type argument.

id : Term n
id = lam 𝟘 (lam ω (var x0))

-- The polymorphic identity function is well-typed (in a well-formed
-- context).

⊢id : ⊢ Γ → Γ ⊢ id ∷ Π 𝟘 , p ▷ U ▹ Π ω , q ▷ var x0 ▹ var x1
⊢id ⊢Γ = lamⱼ (Uⱼ ⊢Γ) (ΓU⊢id ⊢Γ) Π-𝟘-ok

-- The polymorphic identity function is well-resourced (with respect
-- to the zero usage context).

▸id : 𝟘ᶜ {n} ▸[ 𝟙ᵐ ] id
▸id = lamₘ (lamₘ var)

-- The polymorphic identity function applied to two free variables

id-x1-x0 : Term 
id-x1-x0 = id ∘⟨ 𝟘 ⟩ var x1 ∘⟨ ω ⟩ var x0

-- The term id-x0-x1 is well-typed (in a certain context)

⊢id-x1-x0 : ε ∙ U ∙ var x0 ⊢ id-x1-x0 ∷ var x1
⊢id-x1-x0 = (⊢id ⊢Γ ∘ⱼ var ⊢Γ (there here)) ∘ⱼ var ⊢Γ here
  where
  ⊢Γ = ε ∙ Uⱼ ε ∙ univ (var (ε ∙ Uⱼ ε) here)

-- The term id-x1-x0 is well-resourced (with respect to a specific
-- usage context).

▸id-x1-x0 : ε ∙ 𝟘 ∙ ω ▸[ 𝟙ᵐ ] id-x1-x0
▸id-x1-x0 = PE.subst
  (λ γ → γ ▸[ 𝟙ᵐ ] id-x1-x0)
  (≈ᶜ→≡ (ε ∙ PE.refl ∙ PE.cong ⌜_⌝ (ᵐ·-identityʳ {m = 𝟙ᵐ})))
  ((▸id ∘ₘ var) ∘ₘ var)

-- The polymorphic identity function applied to two arguments.

id-ℕ-zero : Term 
id-ℕ-zero = id ∘⟨ 𝟘 ⟩ ℕ ∘⟨ ω ⟩ zero

-- The erasure of id-ℕ-zero includes an erased part (T.↯).

erase-id-ℕ-zero :
  erase id-ℕ-zero PE.≡ T.lam (T.lam (T.var x0)) T.∘ T.↯ T.∘ T.zero
erase-id-ℕ-zero = PE.refl

-- The term id-ℕ-zero is well-typed (in the empty context).

⊢id-ℕ-zero : ε ⊢ id-ℕ-zero ∷ ℕ
⊢id-ℕ-zero = (⊢id ε ∘ⱼ ℕⱼ ε) ∘ⱼ zeroⱼ ε

-- The term id-ℕ-zero is well-resourced (with respect to the empty
-- usage context).

▸id-ℕ-zero : ε ▸[ 𝟙ᵐ ] id-ℕ-zero
▸id-ℕ-zero = (▸id ∘ₘ ℕₘ) ∘ₘ zeroₘ

-- The term id-ℕ-zero reduces to zero.

id-ℕ-zero⇒*zero : ε ⊢ id-ℕ-zero ⇒* zero ∷ ℕ
id-ℕ-zero⇒*zero =
  app-subst
    (β-red (Uⱼ ε) (ΠΣⱼ U⊢0 (univ (var ⊢U0 (there here))) Π-ω-ok)
       U⊢id (ℕⱼ ε) PE.refl Π-𝟘-ok)
    (zeroⱼ ε) ⇨
  (β-red (ℕⱼ ε) (ℕⱼ ⊢ℕ) (var ⊢ℕ here) (zeroⱼ ε) PE.refl Π-ω-ok ⇨
   DT.id (zeroⱼ ε))

-- The erasure of id-ℕ-zero reduces to zero.

erase-id-ℕ-zero⇒*zero : erase id-ℕ-zero T.⇒* T.zero
erase-id-ℕ-zero⇒*zero =
  T.trans (T.app-subst T.β-red) (T.trans T.β-red T.refl)

------------------------------------------------------------------------
-- A function that uses an erased argument in a non-erased position

-- A (closed) identity function that takes an erased argument.

id₀ : Term 
id₀ = lam 𝟘 (var x0)

-- The function id₀ is well-typed (in the empty context).

⊢id₀ : ε ⊢ id₀ ∷ Π 𝟘 , p ▷ ℕ ▹ ℕ
⊢id₀ = lamⱼ (ℕⱼ ε) (var (ε ∙ ℕⱼ ε) here) Π-𝟘-ok

-- The function id₀ is not well-resourced.

¬▸id₀ : ¬ γ ▸[ 𝟙ᵐ ] id₀
¬▸id₀ ▸id₀ =
  case inv-usage-lam ▸id₀ of λ {
    (invUsageLam ▸0 _) →
  case inv-usage-var ▸0 of λ {
    (_ ∙ ()) }}

-- The function id₀ applied to an argument.

id₀-zero : Term 
id₀-zero = id₀ ∘⟨ 𝟘 ⟩ zero

-- The erasure of id₀-zero includes an erased part (T.↯).

erase-id₀-zero : erase id₀-zero PE.≡ T.lam (T.var x0) T.∘ T.↯
erase-id₀-zero = PE.refl

-- The term id₀-zero is well-typed (in the empty context).

⊢id₀-zero : ε ⊢ id₀-zero ∷ ℕ
⊢id₀-zero = ⊢id₀ ∘ⱼ zeroⱼ ε

-- The term id₀-zero is not well-resourced.

¬▸id₀-zero : ¬ γ ▸[ 𝟙ᵐ ] id₀-zero
¬▸id₀-zero ▸id₀-zero =
  case inv-usage-app ▸id₀-zero of λ {
    (invUsageApp ▸id₀ _ _) →
  ¬▸id₀ ▸id₀ }

-- The term id₀-zero reduces to zero.

id₀-zero⇒*zero : ε ⊢ id₀-zero ⇒* zero ∷ ℕ
id₀-zero⇒*zero =
  β-red (ℕⱼ ε) (ℕⱼ ⊢ℕ) (var ⊢ℕ here) (zeroⱼ ε) PE.refl Π-𝟘-ok ⇨
  DT.id (zeroⱼ ε)

-- The erasure of id₀-zero reduces to T.↯.

erase-id₀-zero⇒*↯ : erase id₀-zero T.⇒* T.↯
erase-id₀-zero⇒*↯ = T.trans T.β-red T.refl

-- The erasure of id₀-zero does not reduce to T.zero.

¬erase-id₀-zero⇒*zero : ¬ erase id₀-zero T.⇒* T.zero
¬erase-id₀-zero⇒*zero =
  erase id₀-zero T.⇒* T.zero         →⟨ TP.red*Det erase-id₀-zero⇒*↯ ⟩
  T.↯ T.⇒* T.zero ⊎ T.zero T.⇒* T.↯  →⟨ ⊎.map TP.↯-noRed TP.zero-noRed ⟩
  T.zero PE.≡ T.↯ ⊎ T.↯ PE.≡ T.zero  →⟨ (λ { (inj₁ ()); (inj₂ ()) }) ⟩
  ⊥                                  □

------------------------------------------------------------------------
-- A larger example, which makes use of the fact that uses in the
-- arguments of the eliminator for the empty type can be "ignored"

private

  -- Parts of the implementation of Vec.

  Vec-body₂ : Term (1+ (1+ n))
  Vec-body₂ =
    natrec 𝟘 𝟘 ω
      U
      Unit
      (Σₚ ω , r ▷ var x3 ▹ var x1)
      (var x0)

  Vec-body₁ : Term (1+ n)
  Vec-body₁ = lam ω Vec-body₂

-- Vectors (lists of a fixed length).

Vec : Term 
Vec = lam ω Vec-body₁

-- Vec is well-resourced.

▸Vec : ε ▸[ 𝟙ᵐ ] Vec
▸Vec =
  lamₘ $
  lamₘ $
  natrec-star-or-no-starₘ Unitₘ
    (ΠΣₘ var $
     sub var $
     let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
       𝟘ᶜ ∙ ω ∙ r  ≤⟨ ≤ᶜ-refl ∙ greatest-elem _ ⟩
       𝟘ᶜ ∙ ω ∙ 𝟘  ∎)
    (sub (var {x = x0} {m = 𝟙ᵐ}) $
     let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
       ε ∙ ω ∙ ω  ≤⟨ ≤ᶜ-refl ⟩
       ε ∙ 𝟘 ∙ ω  ∎)
    (sub Uₘ $
     let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
       𝟘ᶜ ∙ ⌜ 𝟘ᵐ? ⌝ · 𝟘  ≈⟨ ≈ᶜ-refl ∙ EM.·-zeroʳ _ ⟩
       𝟘ᶜ                ∎)
    ≤ᶜ-refl
    ≤ᶜ-refl

private

  -- A typing rule for Vec-body₂.

  ⊢Vec-body₂ : ε ∙ U ∙ ℕ ⊢ Vec-body₂ ∷ U
  ⊢Vec-body₂ =
    natrecⱼ Uℕℕ⊢U (Unitⱼ ⊢Uℕ Unit-ok)
      (ΠΣⱼ UℕℕU⊢3 (var ⊢UℕℕU3 (there here)) Σₚ-ω-ok)
      (var ⊢Uℕ here)

  -- A typing rule for Vec-body₁.

  ⊢Vec-body₁ : ε ∙ U ⊢ Vec-body₁ ∷ Π ω , q ▷ ℕ ▹ U
  ⊢Vec-body₁ = lamⱼ U⊢ℕ ⊢Vec-body₂ Π-ω-ok

-- A typing rule for Vec.

⊢Vec : ε ⊢ Vec ∷ Π ω , q ▷ U ▹ Π ω , q ▷ ℕ ▹ U
⊢Vec = lamⱼ (Uⱼ ε) ⊢Vec-body₁ Π-ω-ok

-- Some lemmas used below.

private module Vec-lemmas (⊢A : Γ ⊢ A ∷ U) where

  open Tools.Reasoning.PropositionalEquality

  ⊢Γ : ⊢ Γ
  ⊢Γ = wfTerm ⊢A

  ⊢ΓA : ⊢ Γ ∙ A
  ⊢ΓA = ⊢Γ ∙ univ ⊢A

  ⊢ΓAℕ : ⊢ Γ ∙ A ∙ ℕ
  ⊢ΓAℕ = ⊢ΓA ∙ ℕⱼ ⊢ΓA

  ⊢Γℕ : ⊢ Γ ∙ ℕ
  ⊢Γℕ = ⊢Γ ∙ ℕⱼ ⊢Γ

  Γℕ⊢U : Γ ∙ ℕ ⊢ U
  Γℕ⊢U = Uⱼ ⊢Γℕ

  ⊢ΓℕU : ⊢ Γ ∙ ℕ ∙ U
  ⊢ΓℕU = ⊢Γℕ ∙ Γℕ⊢U

  wk2≡ :
    ∀ A →
    wk (step (step U.id)) A PE.≡
    wk1 (wk1 (wk1 A)) [ liftSubst (liftSubst (sgSubst t)) ]
  wk2≡ {t = t} A =
    wk (step (step U.id)) A                                   ≡⟨ wk≡subst _ _ ⟩
    A [ wk1Subst (wk1Subst (sgSubst (suc t))) ₛ• step U.id ]  ≡˘⟨ subst-wk A ⟩
    wk1 A [ wk1Subst (wk1Subst (sgSubst t)) ]                 ≡˘⟨ wk2-tail (wk1 A) ⟩
    wk1 (wk1 (wk1 A)) [ liftSubst (liftSubst (sgSubst t)) ]   ∎

  ≡wk3[][] :
    ∀ A →
    A PE.≡
    wk1 (wk1 (wk1 A)) [ liftSubst (liftSubst (sgSubst t)) ]
      [ consSubst (sgSubst u) v ]
  ≡wk3[][] {t = t} {u = u} {v = v} A =
    A                                                        ≡˘⟨ subst-id _ ⟩

    A [ consSubst (sgSubst u) v ₛ• step (step U.id) ]        ≡˘⟨ subst-wk A ⟩

    wk (step (step U.id)) A [ consSubst (sgSubst u) v ]      ≡⟨ PE.cong _[ _ ] $ wk2≡ A ⟩

    wk1 (wk1 (wk1 A)) [ liftSubst (liftSubst (sgSubst t)) ]
      [ consSubst (sgSubst u) v ]                            ∎

  wk3[]≡ :
    ∀ A →
    wk1 (wk1 (wk1 (wk1 A))) [ liftSubst (liftSubst (sgSubst t)) ] PE.≡
    wk (lift (lift (step U.id)))
      (wk1 (wk1 (wk1 A)) [ liftSubst (liftSubst (sgSubst u)) ])
  wk3[]≡ {t = t} {u = u} A =
    wk1 (wk1 (wk1 (wk1 A))) [ liftSubst (liftSubst (sgSubst t)) ]  ≡˘⟨ wk2≡ _ ⟩

    wk (step (step U.id)) (wk1 A)                                  ≡⟨ wk-comp _ _ _ ⟩

    wk (step (step (step U.id))) A                                 ≡˘⟨ wk-comp _ _ _ ⟩

    wk (lift (lift (step U.id))) (wk (step (step U.id)) A)         ≡⟨ PE.cong (wk _) $ wk2≡ _ ⟩

    wk (lift (lift (step U.id)))
      (wk1 (wk1 (wk1 A)) [ liftSubst (liftSubst (sgSubst u)) ])    ∎

  ΓℕU⊢A :
    Γ ∙ ℕ ∙ U ⊢
    wk1 (wk1 (wk1 A)) [ liftSubst (liftSubst (sgSubst t)) ] ∷ U
  ΓℕU⊢A =
    PE.subst (_ ⊢_∷ _) (wk2≡ _) $
    W.wkTerm (W.step (W.step W.id)) ⊢ΓℕU ⊢A

  ⊢Vec-body₁′ : Γ ∙ U ⊢ Vec-body₁ ∷ Π ω , q ▷ ℕ ▹ U
  ⊢Vec-body₁′ = W.wkTerm
    (W.lift W.wk₀∷⊇)
    (⊢Γ ∙ Uⱼ ⊢Γ)
    ⊢Vec-body₁

  ⊢Vec-body₁″ : Γ ∙ A ∙ U ⊢ Vec-body₁ ∷ Π ω , q ▷ ℕ ▹ U
  ⊢Vec-body₁″ = W.wkTerm
    (W.lift (W.step W.wk₀∷⊇))
    (⊢ΓA ∙ Uⱼ ⊢ΓA)
    ⊢Vec-body₁

  ⊢Vec-body₂′ :
    Γ ∙ ℕ ⊢ Vec-body₂ [ liftSubst (consSubst (toSubst wk₀) A) ] ∷ U
  ⊢Vec-body₂′ = substitutionTerm
    {σ = liftSubst (consSubst (toSubst wk₀) A)}
    ⊢Vec-body₂
    (liftSubst′ ⊢U ⊢Γ U⊢ℕ (DT.id , ⊢A))
    ⊢Γℕ

  ⊢Vec-body₂″ :
    Γ ∙ A ∙ ℕ ⊢
    Vec-body₂ [ liftSubst (consSubst (toSubst wk₀) (wk1 A)) ] ∷ U
  ⊢Vec-body₂″ = substitutionTerm
    {σ = liftSubst (consSubst (toSubst wk₀) (wk1 A))}
    ⊢Vec-body₂
    (liftSubst′ ⊢U ⊢ΓA U⊢ℕ
       (DT.id , W.wkTerm (W.step W.id) ⊢ΓA ⊢A))
    ⊢ΓAℕ

-- A computation rule for Vec.

Vec∘zero⇒* :
  Γ ⊢ A ∷ U →
  Γ ⊢ wk wk₀ Vec ∘⟨ ω ⟩ A ∘⟨ ω ⟩ zero ⇒* Unit ∷ U
Vec∘zero⇒* {A = A} ⊢A =
  app-subst
    (β-red (Uⱼ ⊢Γ) (syntacticTerm ⊢Vec-body₁′)
       ⊢Vec-body₁′ ⊢A PE.refl Π-ω-ok)
    (zeroⱼ ⊢Γ) ⇨
  (β-red (ℕⱼ ⊢Γ) Γℕ⊢U ⊢Vec-body₂′ (zeroⱼ ⊢Γ) PE.refl Π-ω-ok ⇨
   (redMany $
    _⊢_⇒_∷_.natrec-zero Γℕ⊢U (Unitⱼ ⊢Γ Unit-ok) $
    ΠΣⱼ ΓℕU⊢A (var (⊢ΓℕU ∙ univ ΓℕU⊢A) (there here)) Σₚ-ω-ok))
  where
  open Vec-lemmas ⊢A

-- An equality rule for Vec.

Vec∘suc≡ :
  Γ ⊢ A ∷ U →
  Γ ⊢ t ∷ ℕ →
  Γ ⊢
    wk wk₀ Vec ∘⟨ ω ⟩ A ∘⟨ ω ⟩ suc t ≡
    Σₚ ω , r ▷ A ▹ (wk wk₀ Vec ∘⟨ ω ⟩ wk1 A ∘⟨ ω ⟩ wk1 t) ∷ U
Vec∘suc≡ {Γ = Γ} {A = A} {t = t} ⊢A ⊢t =
  _⊢_≡_∷_.trans
    (app-cong
       (β-red (Uⱼ ⊢Γ) (syntacticTerm ⊢Vec-body₁′)
          ⊢Vec-body₁′ ⊢A PE.refl Π-ω-ok)
       (refl (sucⱼ ⊢t))) $
  _⊢_≡_∷_.trans
    (β-red (ℕⱼ ⊢Γ) Γℕ⊢U ⊢Vec-body₂′ (sucⱼ ⊢t) PE.refl Π-ω-ok) $
  _⊢_≡_∷_.trans
    (flip (_⊢_≡_∷_.natrec-suc Γℕ⊢U (Unitⱼ ⊢Γ Unit-ok)) ⊢t $
     ΠΣⱼ ΓℕU⊢A (var (⊢ΓℕU ∙ univ ΓℕU⊢A) (there here)) Σₚ-ω-ok) $
  _⊢_≡_∷_.trans
    (_⊢_≡_∷_.sym $
     ΠΣ-cong (univ ⊢A)
       (PE.subst (_ ⊢ _ ≡_∷ _) (≡wk3[][] A) (refl ⊢A))
       (PE.subst (Γ ∙ A ⊢ (Vec-body₁ [ wk1 A ]₀) ∘⟨ ω ⟩ wk1 t ≡_∷ U)
          (PE.cong (flip (natrec 𝟘 𝟘 ω U Unit) _) $
           PE.cong (Σₚ _ , _ ▷_▹ _) $
           wk3[]≡ A) $
        β-red (ℕⱼ ⊢ΓA) (Uⱼ ⊢ΓAℕ) ⊢Vec-body₂″
          (W.wkTerm (W.step W.id) ⊢ΓA ⊢t) PE.refl Π-ω-ok)
       Σₚ-ω-ok) $
  _⊢_≡_∷_.sym $
  flip (_⊢_≡_∷_.ΠΣ-cong (univ ⊢A) (refl ⊢A)) Σₚ-ω-ok $
  app-cong
    (β-red (Uⱼ ⊢ΓA) (syntacticTerm ⊢Vec-body₁″)
      ⊢Vec-body₁″ (W.wkTerm (W.step W.id) ⊢ΓA ⊢A) PE.refl Π-ω-ok) $
  _⊢_≡_∷_.refl $
  W.wkTerm (W.step W.id) ⊢ΓA ⊢t
  where
  open Vec-lemmas ⊢A

private

  -- Parts of the implementation of Non-zero.

  Non-zero-body : Term (1+ n)
  Non-zero-body =
    natrec 𝟘 𝟘 𝟘
      U
      Empty
      Unit
      (var x0)

-- A natural number predicate that holds for non-zero numbers.

Non-zero : Term 
Non-zero = lam ω Non-zero-body

-- Non-zero is well-resourced.

▸Non-zero : ε ▸[ 𝟙ᵐ ] Non-zero
▸Non-zero =
  lamₘ $
  natrec-star-or-no-starₘ Emptyₘ
    Unitₘ
    var
    (sub Uₘ $
     let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
       𝟘ᶜ ∙ ⌜ 𝟘ᵐ? ⌝ · 𝟘  ≈⟨ ≈ᶜ-refl ∙ EM.·-zeroʳ _ ⟩
       𝟘ᶜ                ∎)
    ≤ᶜ-refl
    ≤ᶜ-refl

private

  -- A typing rule for Non-zero-body.

  ⊢Non-zero-body : ε ∙ ℕ ⊢ Non-zero-body ∷ U
  ⊢Non-zero-body =
    natrecⱼ ℕℕ⊢U (Emptyⱼ ⊢ℕ) (Unitⱼ ⊢ℕℕU Unit-ok)
      (var ⊢ℕ here)

-- A typing rule for Non-zero.

⊢Non-zero : ε ⊢ Non-zero ∷ Π ω , q ▷ ℕ ▹ U
⊢Non-zero = lamⱼ (ℕⱼ ε) ⊢Non-zero-body Π-ω-ok

-- A computation rule for Non-zero.

Non-zero∘zero⇒* :
  ⊢ Γ →
  Γ ⊢ wk wk₀ Non-zero ∘⟨ ω ⟩ zero ⇒* Empty ∷ U
Non-zero∘zero⇒* ⊢Γ =
  β-red (ℕⱼ ⊢Γ) (Uⱼ ⊢Γℕ)
    (W.wkTerm (W.lift W.wk₀∷⊇) ⊢Γℕ ⊢Non-zero-body)
    (zeroⱼ ⊢Γ) PE.refl Π-ω-ok ⇨
  (redMany $
   natrec-zero (Uⱼ ⊢Γℕ) (Emptyⱼ ⊢Γ)
     (Unitⱼ (⊢Γℕ ∙ Uⱼ ⊢Γℕ) Unit-ok))
  where
  ⊢Γℕ = ⊢Γ ∙ ℕⱼ ⊢Γ

-- Another computation rule for Non-zero.

Non-zero∘suc⇒* :
  Γ ⊢ t ∷ ℕ →
  Γ ⊢ wk wk₀ Non-zero ∘⟨ ω ⟩ suc t ⇒* Unit ∷ U
Non-zero∘suc⇒* ⊢t =
  β-red (ℕⱼ ⊢Γ) (Uⱼ ⊢Γℕ)
    (W.wkTerm (W.lift W.wk₀∷⊇) ⊢Γℕ ⊢Non-zero-body)
    (sucⱼ ⊢t) PE.refl Π-ω-ok ⇨
  (redMany $
   natrec-suc (Uⱼ ⊢Γℕ) (Emptyⱼ ⊢Γ)
     (Unitⱼ (⊢Γℕ ∙ Uⱼ ⊢Γℕ) Unit-ok) ⊢t)
  where
  ⊢Γ  = wfTerm ⊢t
  ⊢Γℕ = ⊢Γ ∙ ℕⱼ ⊢Γ

-- A safe head function for vectors.

head : Term 
head =
  lam 𝟘 $
  lam ω $
  natrec
    𝟘 ω 𝟘
    (Π ω , q ▷ wk wk₀ Vec ∘⟨ ω ⟩ var x2 ∘⟨ ω ⟩ var x0 ▹
     Π 𝟘 , p ▷ wk wk₀ Non-zero ∘⟨ ω ⟩ var x1 ▹
     var x4)
    (lam ω $ lam 𝟘 $
     emptyrec 𝟘 (var x3) (var x0))
    (lam ω $ lam 𝟘 $ fst ω (var x1))
    (var x0)

-- The erasure of head includes an erased part (T.↯).

erase-head :
  erase head PE.≡
  (T.lam $ T.lam $
   T.natrec
     (T.lam (T.lam T.↯))
     (T.lam (T.lam (T.fst (T.var x1))))
     (T.var x0))
erase-head = PE.refl

-- The term head is well-resourced.

▸head : ε ▸[ 𝟙ᵐ ] head
▸head =
  lamₘ $
  lamₘ $
  natrec-star-or-no-starₘ
    (lamₘ $
     lamₘ $
     sub (emptyrecₘ var var) $
     let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
       𝟘ᶜ ∙ ω ∙ 𝟘  ≤⟨ ≤ᶜ-refl ⟩
       𝟘ᶜ          ∎)
    (lamₘ $
     lamₘ $
     fstₘ 𝟙ᵐ
       (sub var $
        let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
          𝟘ᶜ ∙ ω ∙ 𝟘  ≤⟨ ≤ᶜ-refl ⟩
          𝟘ᶜ          ∎)
       (≢𝟘→⌞⌟≡𝟙ᵐ {p = ω} (λ ()))
       (λ _ → PE.refl))
    var
    (sub
       (ΠΣₘ ((𝟘ᶜ▸[𝟙ᵐ]→ (wkUsage wk₀ ▸Vec) ∘ₘ var) ∘ₘ var) $
        sub
          (ΠΣₘ (𝟘ᶜ▸[𝟙ᵐ]→ (wkUsage wk₀ ▸Non-zero) ∘ₘ var) $
           sub var $
           let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
             ε ∙ ⌜ 𝟘ᵐ? ⌝ ∙ 𝟘 ∙ 𝟘 ∙ 𝟘 ∙ ⌜ 𝟘ᵐ? ⌝ · p  ≤⟨ ≤ᶜ-refl ∙ greatest-elem _ ⟩
             ε ∙ ⌜ 𝟘ᵐ? ⌝ ∙ 𝟘 ∙ 𝟘 ∙ 𝟘 ∙ 𝟘            ∎) $
        let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
          ε ∙ ⌜ 𝟘ᵐ? ⌝ ∙ 𝟘 ∙ ⌜ (𝟘ᵐ? ᵐ· 𝟘) ᵐ· ω ⌝     ∙ ⌜ 𝟘ᵐ? ⌝ · q  ≤⟨ ≤ᶜ-refl ∙
                                                                      ≤-reflexive (PE.sym (EM.+-identityʳ _)) ∙
                                                                      greatest-elem _ ⟩
          ε ∙ ⌜ 𝟘ᵐ? ⌝ ∙ 𝟘 ∙ ⌜ (𝟘ᵐ? ᵐ· 𝟘) ᵐ· ω ⌝ + 𝟘 ∙ 𝟘            ∎) $
     let open Tools.Reasoning.PartialOrder ≤ᶜ-poset in begin
       ε ∙ ⌜ (𝟘ᵐ? ᵐ· ω) ᵐ· ω ⌝ + 𝟘 + ⌜ 𝟘ᵐ? ⌝ ∙ 𝟘 ∙ ⌜ 𝟘ᵐ? ⌝ · ω  ≈⟨ ≈ᶜ-refl ∙ lemma ⟩

       ε ∙ ⌜ (𝟘ᵐ? ᵐ· ω) ᵐ· ω ⌝ + 𝟘 + ⌜ 𝟘ᵐ? ⌝ ∙ 𝟘 ∙
         ⌜ (𝟘ᵐ? ᵐ· ω) ᵐ· ω ⌝ + ⌜ (𝟘ᵐ? ᵐ· 𝟘) ᵐ· ω ⌝              ∎)
    ≤ᶜ-refl
    ≤ᶜ-refl
  where
  lemma : ⌜ 𝟘ᵐ? ⌝ · ω PE.≡ ⌜ (𝟘ᵐ? ᵐ· ω) ᵐ· ω ⌝ + ⌜ (𝟘ᵐ? ᵐ· 𝟘) ᵐ· ω ⌝
  lemma = 𝟘ᵐ?-elim
    (λ m → ⌜ m ⌝ · ω PE.≡ ⌜ (m ᵐ· ω) ᵐ· ω ⌝ + ⌜ (m ᵐ· 𝟘) ᵐ· ω ⌝)
    PE.refl
    (λ not-ok →
       ω                                ≡⟨ PE.sym $
                                           PE.cong₂ (λ m₁ m₂ → ⌜ m₁ ⌝ + ⌜ m₂ ⌝)
                                             {x = ⌞ ω ⌟ ᵐ· ω} {u = ⌞ 𝟘 ⌟ ᵐ· ω}
                                             (only-𝟙ᵐ-without-𝟘ᵐ not-ok)
                                             (only-𝟙ᵐ-without-𝟘ᵐ not-ok) ⟩
       ⌜ ⌞ ω ⌟ ᵐ· ω ⌝ + ⌜ ⌞ 𝟘 ⌟ ᵐ· ω ⌝  ∎)
    where
    open Tools.Reasoning.PropositionalEquality

-- A typing rule for head.

⊢head :
  ε ⊢
  head ∷
  Π 𝟘 , p ▷ U ▹
  Π ω , q ▷ ℕ ▹
  Π ω , q ▷ wk wk₀ Vec ∘⟨ ω ⟩ var x1 ∘⟨ ω ⟩ var x0 ▹
  Π 𝟘 , p ▷ wk wk₀ Non-zero ∘⟨ ω ⟩ var x1 ▹
  var x3
⊢head =
  flip (lamⱼ (Uⱼ ε)) Π-𝟘-ok $
  flip (lamⱼ U⊢ℕ) Π-ω-ok $
  natrecⱼ (univ Uℕℕ⊢ΠΠ∷U)
    (flip (lamⱼ (univ ⊢Vec-1-0)) Π-ω-ok $
     flip (lamⱼ (univ ⊢Non-zero-zero)) Π-𝟘-ok $
     emptyrecⱼ
       (univ (var ⊢Uℕ∙Vec∙Non-zero (there (there (there here)))))
       (_⊢_∷_.conv (var ⊢Uℕ∙Vec∙Non-zero here) $
        _⊢_≡_.univ $
        subset*Term $
        Non-zero∘zero⇒* ⊢Uℕ∙Vec∙Non-zero))
    (flip (lamⱼ (univ ⊢Vec-3-1+1)) Π-ω-ok $
     flip (lamⱼ (univ ⊢Non-zero-1+2)) Π-𝟘-ok $
     fstⱼ (univ ⊢5) (univ ⊢Vec-6-4) $
     _⊢_∷_.conv (var ⊢Uℕℕ∙ΠΠ∙Vec∙Non-zero (there here)) $
     _⊢_≡_.univ $
     Vec∘suc≡ ⊢5
       (var ⊢Uℕℕ∙ΠΠ∙Vec∙Non-zero (there (there (there here)))))
    (var ⊢Uℕ here)
  where
  ⊢Vec-2-0 :
    ε ∙ U ∙ ℕ ∙ ℕ ⊢ wk wk₀ Vec ∘⟨ ω ⟩ var x2 ∘⟨ ω ⟩ var x0 ∷ U
  ⊢Vec-2-0 =
    (W.wkTerm (W.step (W.step (W.step W.id))) ⊢Uℕℕ ⊢Vec ∘ⱼ
     var ⊢Uℕℕ (there (there here))) ∘ⱼ
    var ⊢Uℕℕ here

  ⊢Vec-1-0 :
    ε ∙ U ∙ ℕ ⊢ wk wk₀ Vec ∘⟨ ω ⟩ var x1 ∘⟨ ω ⟩ zero ∷ U
  ⊢Vec-1-0 = substTerm ⊢Vec-2-0 (zeroⱼ ⊢Uℕ)

  ⊢Non-zero-0 :
    ε ∙ U ∙ ℕ ∙ ℕ ⊢ wk wk₀ Non-zero ∘⟨ ω ⟩ var x0 ∷ U
  ⊢Non-zero-0 =
    W.wkTerm (W.step (W.step (W.step W.id))) ⊢Uℕℕ ⊢Non-zero ∘ⱼ
    var ⊢Uℕℕ here

  ⊢Uℕℕ∙Vec = ⊢Uℕℕ ∙ univ ⊢Vec-2-0

  ⊢Non-zero-1 :
    ε ∙ U ∙ ℕ ∙ ℕ ∙ wk wk₀ Vec ∘⟨ ω ⟩ var x2 ∘⟨ ω ⟩ var x0 ⊢
    wk wk₀ Non-zero ∘⟨ ω ⟩ var x1 ∷ U
  ⊢Non-zero-1 =
    W.wkTerm (W.step W.id) ⊢Uℕℕ∙Vec ⊢Non-zero-0

  ⊢Uℕ∙Vec = ⊢Uℕ ∙ univ ⊢Vec-1-0

  ⊢Non-zero-zero :
    ε ∙ U ∙ ℕ ∙ wk wk₀ Vec ∘⟨ ω ⟩ var x1 ∘⟨ ω ⟩ zero ⊢
    wk wk₀ Non-zero ∘⟨ ω ⟩ zero ∷ U
  ⊢Non-zero-zero = substitutionTerm
    ⊢Non-zero-1
    (liftSubst′ ⊢Uℕℕ ⊢Uℕ (univ ⊢Vec-2-0) (singleSubst (zeroⱼ ⊢Uℕ)))
    ⊢Uℕ∙Vec

  ⊢Uℕ∙Vec∙Non-zero  = ⊢Uℕ∙Vec ∙ univ ⊢Non-zero-zero
  ⊢Uℕℕ∙Vec∙Non-zero = ⊢Uℕℕ∙Vec ∙ univ ⊢Non-zero-1

  Uℕℕ⊢ΠΠ∷U :
    ε ∙ U ∙ ℕ ∙ ℕ ⊢
    Π ω , q ▷ wk wk₀ Vec ∘⟨ ω ⟩ var x2 ∘⟨ ω ⟩ var x0 ▹
      Π 𝟘 , p ▷ wk wk₀ Non-zero ∘⟨ ω ⟩ var x1 ▹ var x4 ∷
    U
  Uℕℕ⊢ΠΠ∷U =
    ΠΣⱼ ⊢Vec-2-0
      (ΠΣⱼ ⊢Non-zero-1
         (var ⊢Uℕℕ∙Vec∙Non-zero
            (there (there (there (there here)))))
         Π-𝟘-ok)
      Π-ω-ok

  Uℕℕ∙ΠΠ =
    ε ∙ U ∙ ℕ ∙ ℕ ∙
    Π ω , q ▷ wk wk₀ Vec ∘⟨ ω ⟩ var x2 ∘⟨ ω ⟩ var x0 ▹
      Π 𝟘 , p ▷ wk wk₀ Non-zero ∘⟨ ω ⟩ var x1 ▹ var x4
  ⊢Uℕℕ∙ΠΠ = ⊢Uℕℕ ∙ univ Uℕℕ⊢ΠΠ∷U

  ⊢Vec-3-1+1 :
    Uℕℕ∙ΠΠ ⊢ wk wk₀ Vec ∘⟨ ω ⟩ var x3 ∘⟨ ω ⟩ suc (var x1) ∷ U
  ⊢Vec-3-1+1 = substitutionTerm
    ⊢Vec-2-0
    (wk1Subst′ ⊢Uℕℕ ⊢Uℕℕ (univ Uℕℕ⊢ΠΠ∷U)
       (singleSubst↑ (sucⱼ (var ⊢Uℕℕ here))))
    ⊢Uℕℕ∙ΠΠ

  Uℕℕ∙ΠΠ∙Vec  = Uℕℕ∙ΠΠ ∙ wk wk₀ Vec ∘⟨ ω ⟩ var x3 ∘⟨ ω ⟩ suc (var x1)
  ⊢Uℕℕ∙ΠΠ∙Vec = ⊢Uℕℕ∙ΠΠ ∙ univ ⊢Vec-3-1+1

  ⊢Non-zero-1+2 :
    Uℕℕ∙ΠΠ∙Vec ⊢ wk wk₀ Non-zero ∘⟨ ω ⟩ suc (var x2) ∷ U
  ⊢Non-zero-1+2 = substitutionTerm
    ⊢Non-zero-0
    (wk1Subst′ ⊢Uℕℕ ⊢Uℕℕ∙ΠΠ (univ ⊢Vec-3-1+1)
       (wk1Subst′ ⊢Uℕℕ ⊢Uℕℕ (univ Uℕℕ⊢ΠΠ∷U)
          (singleSubst↑ (sucⱼ (var ⊢Uℕℕ here)))))
    ⊢Uℕℕ∙ΠΠ∙Vec

  Uℕℕ∙ΠΠ∙Vec∙Non-zero =
    Uℕℕ∙ΠΠ∙Vec ∙ wk wk₀ Non-zero ∘⟨ ω ⟩ suc (var x2)
  ⊢Uℕℕ∙ΠΠ∙Vec∙Non-zero = ⊢Uℕℕ∙ΠΠ∙Vec ∙ univ ⊢Non-zero-1+2

  ⊢5 : Uℕℕ∙ΠΠ∙Vec∙Non-zero ⊢ var x5 ∷ U
  ⊢5 = var
    ⊢Uℕℕ∙ΠΠ∙Vec∙Non-zero
    (there (there (there (there (there here)))))

  Uℕℕ∙ΠΠ∙Vec∙Non-zero∙5  = Uℕℕ∙ΠΠ∙Vec∙Non-zero ∙ var x5
  ⊢Uℕℕ∙ΠΠ∙Vec∙Non-zero∙5 = ⊢Uℕℕ∙ΠΠ∙Vec∙Non-zero ∙ univ ⊢5

  ⊢Vec-6-4 :
    Uℕℕ∙ΠΠ∙Vec∙Non-zero∙5 ⊢
    wk wk₀ Vec ∘⟨ ω ⟩ var x6 ∘⟨ ω ⟩ var x4 ∷ U
  ⊢Vec-6-4 = W.wkTerm
    (W.step (W.step (W.step (W.step W.id))))
    ⊢Uℕℕ∙ΠΠ∙Vec∙Non-zero∙5
    ⊢Vec-2-0

-- A concrete vector which contains a single natural number.

[0] : Term 
[0] = prodₚ ω zero star

-- [0] is well-resourced.

▸[0] : ε ▸[ 𝟙ᵐ ] [0]
▸[0] = prodₚₘ zeroₘ starₘ

-- [0] is in η-long normal form.

[0]-normal : ε ⊢nf [0] ∷ Vec ∘⟨ ω ⟩ ℕ ∘⟨ ω ⟩ suc zero
[0]-normal =
  _⊢nf_∷_.convₙ
    (prodₙ (ℕⱼ ε) (Unitⱼ ⊢ℕ Unit-ok) (zeroₙ ε)
       (starₙ ε Unit-ok) Σₚ-ω-ok) $
  _⊢_≡_.univ $
  _⊢_≡_∷_.sym $
  _⊢_≡_∷_.trans (Vec∘suc≡ (ℕⱼ ε) (zeroⱼ ε)) $
  ΠΣ-cong (ℕⱼ ε) (refl (ℕⱼ ε))
    (subset*Term (Vec∘zero⇒* (ℕⱼ (ε ∙ ℕⱼ ε)))) Σₚ-ω-ok

-- A typing rule for [0].

⊢[0] : ε ⊢ [0] ∷ Vec ∘⟨ ω ⟩ ℕ ∘⟨ ω ⟩ suc zero
⊢[0] = ⊢nf∷→⊢∷ [0]-normal

-- An application of head to [0] and some other arguments.

head-[0] : Term 
head-[0] = head ∘⟨ 𝟘 ⟩ ℕ ∘⟨ ω ⟩ suc zero ∘⟨ ω ⟩ [0] ∘⟨ 𝟘 ⟩ star

-- The erasure of head-[0] includes several erased parts (T.↯).

erase-head-[0] :
  erase head-[0] PE.≡
  (T.lam
     (T.lam $
      T.natrec (T.lam (T.lam T.↯))
        (T.lam (T.lam (T.fst (T.var x1))))
        (T.var x0)) T.∘
   T.↯ T.∘ T.suc T.zero T.∘ T.prod T.zero T.star T.∘ T.↯)
erase-head-[0] = PE.refl

-- The term head-[0] is well-resourced.

▸head-[0] : ε ▸[ 𝟙ᵐ ] head-[0]
▸head-[0] = (((▸head ∘ₘ ℕₘ) ∘ₘ sucₘ zeroₘ) ∘ₘ 𝟘ᶜ▸[𝟙ᵐ]→ ▸[0]) ∘ₘ starₘ

-- The term head-[0] is well-typed.

⊢head-[0] : ε ⊢ head-[0] ∷ ℕ
⊢head-[0] =
  (((⊢head ∘ⱼ ℕⱼ ε) ∘ⱼ sucⱼ (zeroⱼ ε)) ∘ⱼ ⊢[0]) ∘ⱼ
  conv (starⱼ ε Unit-ok)
    (_⊢_≡_.univ $
     _⊢_≡_∷_.sym $
     subset*Term (Non-zero∘suc⇒* (zeroⱼ ε)))

-- The erasure of head-[0] reduces to T.zero.

erase-head-[0]⇒*zero : erase head-[0] T.⇒* T.zero
erase-head-[0]⇒*zero =
  T.trans (T.app-subst (T.app-subst (T.app-subst T.β-red))) $
  T.trans (T.app-subst (T.app-subst T.β-red)) $
  T.trans (T.app-subst (T.app-subst T.natrec-suc)) $
  T.trans (T.app-subst T.β-red) $
  T.trans T.β-red $
  T.trans T.Σ-β₁
  T.refl

-- The term head-[0] reduces to zero.
--
-- Note that this is proved using the fact that the erasure of
-- head-[0] reduces to T.zero.

head-[0]⇒*zero : ε ⊢ head-[0] ⇒* zero ∷ ℕ
head-[0]⇒*zero =
  case Soundness₀.soundness-ℕ ⊢head-[0] ▸head-[0] of λ where
    ( , head-[0]⇒*zero , _) →
      S.⇒ˢ*zero∷ℕ→⇒*zero head-[0]⇒*zero
    (1+ _ , _ , erase-head-[0]⇒*suc) →
      case TP.red*Det erase-head-[0]⇒*zero
              (S.⇒ˢ*suc→⇒*suc erase-head-[0]⇒*suc .proj₂)
      of λ where
        (inj₁ zero⇒*suc) → case TP.zero-noRed zero⇒*suc of λ ()
        (inj₂ suc⇒*zero) → case TP.suc-noRed  suc⇒*zero of λ ()