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)
(Π-𝟘-ok : Π-allowed 𝟘 p)
(Π-ω-ok : Π-allowed ω q)
(Σₚ-ω-ok : Σₚ-allowed ω r)
(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
⊢ℕ : ⊢ ε ∙ ℕ
⊢ℕ = ε ∙ ℕⱼ ε
⊢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
id : Term n
id = lam 𝟘 (lam ω (var x0))
⊢id : ⊢ Γ → Γ ⊢ id ∷ Π 𝟘 , p ▷ U ▹ Π ω , q ▷ var x0 ▹ var x1
⊢id ⊢Γ = lamⱼ (Uⱼ ⊢Γ) (ΓU⊢id ⊢Γ) Π-𝟘-ok
▸id : 𝟘ᶜ {n} ▸[ 𝟙ᵐ ] id
▸id = lamₘ (lamₘ var)
id-x1-x0 : Term 2
id-x1-x0 = id ∘⟨ 𝟘 ⟩ var x1 ∘⟨ ω ⟩ var x0
⊢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)
▸id-x1-x0 : ε ∙ 𝟘 ∙ ω ▸[ 𝟙ᵐ ] id-x1-x0
▸id-x1-x0 = PE.subst
(λ γ → γ ▸[ 𝟙ᵐ ] id-x1-x0)
(≈ᶜ→≡ (ε ∙ PE.refl ∙ PE.cong ⌜_⌝ (ᵐ·-identityʳ {m = 𝟙ᵐ})))
((▸id ∘ₘ var) ∘ₘ var)
id-ℕ-zero : Term 0
id-ℕ-zero = id ∘⟨ 𝟘 ⟩ ℕ ∘⟨ ω ⟩ zero
erase-id-ℕ-zero :
erase id-ℕ-zero PE.≡ T.lam (T.lam (T.var x0)) T.∘ T.↯ T.∘ T.zero
erase-id-ℕ-zero = PE.refl
⊢id-ℕ-zero : ε ⊢ id-ℕ-zero ∷ ℕ
⊢id-ℕ-zero = (⊢id ε ∘ⱼ ℕⱼ ε) ∘ⱼ zeroⱼ ε
▸id-ℕ-zero : ε ▸[ 𝟙ᵐ ] id-ℕ-zero
▸id-ℕ-zero = (▸id ∘ₘ ℕₘ) ∘ₘ 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ⱼ ε))
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)
id₀ : Term 0
id₀ = lam 𝟘 (var x0)
⊢id₀ : ε ⊢ id₀ ∷ Π 𝟘 , p ▷ ℕ ▹ ℕ
⊢id₀ = lamⱼ (ℕⱼ ε) (var (ε ∙ ℕⱼ ε) here) Π-𝟘-ok
¬▸id₀ : ¬ γ ▸[ 𝟙ᵐ ] id₀
¬▸id₀ ▸id₀ =
case inv-usage-lam ▸id₀ of λ {
(invUsageLam ▸0 _) →
case inv-usage-var ▸0 of λ {
(_ ∙ ()) }}
id₀-zero : Term 0
id₀-zero = id₀ ∘⟨ 𝟘 ⟩ zero
erase-id₀-zero : erase id₀-zero PE.≡ T.lam (T.var x0) T.∘ T.↯
erase-id₀-zero = PE.refl
⊢id₀-zero : ε ⊢ id₀-zero ∷ ℕ
⊢id₀-zero = ⊢id₀ ∘ⱼ zeroⱼ ε
¬▸id₀-zero : ¬ γ ▸[ 𝟙ᵐ ] id₀-zero
¬▸id₀-zero ▸id₀-zero =
case inv-usage-app ▸id₀-zero of λ {
(invUsageApp ▸id₀ _ _) →
¬▸id₀ ▸id₀ }
id₀-zero⇒*zero : ε ⊢ id₀-zero ⇒* zero ∷ ℕ
id₀-zero⇒*zero =
β-red (ℕⱼ ε) (ℕⱼ ⊢ℕ) (var ⊢ℕ here) (zeroⱼ ε) PE.refl Π-𝟘-ok ⇨
DT.id (zeroⱼ ε)
erase-id₀-zero⇒*↯ : erase id₀-zero T.⇒* T.↯
erase-id₀-zero⇒*↯ = T.trans T.β-red T.refl
¬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₂ ()) }) ⟩
⊥ □
private
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₂
Vec : Term 0
Vec = lam ω Vec-body₁
▸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
⊢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)
⊢Vec-body₁ : ε ∙ U ⊢ Vec-body₁ ∷ Π ω , q ▷ ℕ ▹ U
⊢Vec-body₁ = lamⱼ U⊢ℕ ⊢Vec-body₂ Π-ω-ok
⊢Vec : ε ⊢ Vec ∷ Π ω , q ▷ U ▹ Π ω , q ▷ ℕ ▹ U
⊢Vec = lamⱼ (Uⱼ ε) ⊢Vec-body₁ Π-ω-ok
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ℕ
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
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
Non-zero-body : Term (1+ n)
Non-zero-body =
natrec 𝟘 𝟘 𝟘
U
Empty
Unit
(var x0)
Non-zero : Term 0
Non-zero = lam ω Non-zero-body
▸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
⊢Non-zero-body : ε ∙ ℕ ⊢ Non-zero-body ∷ U
⊢Non-zero-body =
natrecⱼ ℕℕ⊢U (Emptyⱼ ⊢ℕ) (Unitⱼ ⊢ℕℕU Unit-ok)
(var ⊢ℕ here)
⊢Non-zero : ε ⊢ Non-zero ∷ Π ω , q ▷ ℕ ▹ U
⊢Non-zero = lamⱼ (ℕⱼ ε) ⊢Non-zero-body Π-ω-ok
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
⊢Γℕ = ⊢Γ ∙ ℕⱼ ⊢Γ
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
⊢Γℕ = ⊢Γ ∙ ℕⱼ ⊢Γ
head : Term 0
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)
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
▸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
⊢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
[0] : Term 0
[0] = prodₚ ω zero star
▸[0] : ε ▸[ 𝟙ᵐ ] [0]
▸[0] = prodₚₘ zeroₘ starₘ
[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
⊢[0] : ε ⊢ [0] ∷ Vec ∘⟨ ω ⟩ ℕ ∘⟨ ω ⟩ suc zero
⊢[0] = ⊢nf∷→⊢∷ [0]-normal
head-[0] : Term 0
head-[0] = head ∘⟨ 𝟘 ⟩ ℕ ∘⟨ ω ⟩ suc zero ∘⟨ ω ⟩ [0] ∘⟨ 𝟘 ⟩ star
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
▸head-[0] : ε ▸[ 𝟙ᵐ ] head-[0]
▸head-[0] = (((▸head ∘ₘ ℕₘ) ∘ₘ sucₘ zeroₘ) ∘ₘ 𝟘ᶜ▸[𝟙ᵐ]→ ▸[0]) ∘ₘ starₘ
⊢head-[0] : ε ⊢ head-[0] ∷ ℕ
⊢head-[0] =
(((⊢head ∘ⱼ ℕⱼ ε) ∘ⱼ sucⱼ (zeroⱼ ε)) ∘ⱼ ⊢[0]) ∘ⱼ
conv (starⱼ ε Unit-ok)
(_⊢_≡_.univ $
_⊢_≡_∷_.sym $
subset*Term (Non-zero∘suc⇒* (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
head-[0]⇒*zero : ε ⊢ head-[0] ⇒* zero ∷ ℕ
head-[0]⇒*zero =
case Soundness₀.soundness-ℕ ⊢head-[0] ▸head-[0] of λ where
(0 , 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 λ ()