{-# OPTIONS --safe --sized-types #-}
module Motivation.POPLMark2.GodelT where
open import Data.Var using (Var; _─Scoped; injectˡ; injectʳ)
open import Data.Var.Varlike
open import Data.Environment
open import Data.Pred as P
open import Data.Relation as R
open import Generic.Syntax
open import Generic.Semantics
open import Generic.Semantics.Syntactic
open import Generic.Identity hiding (`con)
open import Generic.Fundamental as Fdm
open import Generic.Simulation
import Generic.Simulation.Syntactic as Sim
open import Generic.Fusion
open import Generic.Fusion.Syntactic
open import Size
open import Data.Sum as Sum
open import Data.Product as Prod
open import Data.List.Base hiding ([_] ; lookup)
open import Data.Product
open import Relation.Binary.Construct.Closure.ReflexiveTransitive as S using (Star)
open import Function hiding (_∋_)
open import Relation.Binary.PropositionalEquality hiding ([_]); open ≡-Reasoning
data Type : Set where
α : Type
ℕ : Type
_+_ : Type → Type → Type
_⇒_ : Type → Type → Type
data TermC : Set where
Lam App : Type → Type → TermC
InL InR : Type → Type → TermC
Cas : Type → Type → Type → TermC
Zro Suc : TermC
Rec : Type → TermC
TermD : Desc Type
TermD = `σ TermC λ where
(Lam σ τ) → `X (σ ∷ []) τ (`∎ (σ ⇒ τ))
(App σ τ) → `X [] (σ ⇒ τ) (`X [] σ (`∎ τ))
(InL σ τ) → `X [] σ (`∎ (σ + τ))
(InR σ τ) → `X [] τ (`∎ (σ + τ))
(Cas σ τ ν) → `X [] (σ + τ) (`X (σ ∷ []) ν (`X (τ ∷ []) ν (`∎ ν)))
Zro → `∎ ℕ
Suc → `X [] ℕ (`∎ ℕ)
(Rec σ) → `X [] σ (`X (σ ∷ ℕ ∷ []) σ (`X [] ℕ (`∎ σ)))
Term : Type ─Scoped
Term = Tm TermD _
private
variable
σ σ₁ σ₂ τ ν : Type
⊡ ⊡₁ ⊡₂ : Type
Γ Δ : List Type
t t′ u u′ f g b b′ l m r s ze ze′ su su′ : Term σ Γ
ρ ρ' : (Γ ─Env) Term Δ
i : Size
infixl 10 _`∙_
pattern `λ' b = (Lam _ _ , b , refl)
pattern _`∙'_ f t = (App _ _ , f , t , refl)
pattern `i₁' t = (InL _ _ , t , refl)
pattern `i₂' t = (InR _ _ , t , refl)
pattern `case' t l r = (Cas _ _ _ , t , l , r , refl)
pattern `0' = (Zro , refl)
pattern `1+' t = (Suc , t , refl)
pattern `rec' ze su t = (Rec _ , ze , su , t , refl)
pattern `λ b = `con (`λ' b)
pattern _`∙_ f t = `con (f `∙' t)
pattern `i₁ t = `con (`i₁' t)
pattern `i₂ t = `con (`i₂' t)
pattern `case t l r = `con (`case' t l r)
pattern `0 = `con `0'
pattern `1+ t = `con (`1+' t)
pattern `rec ze su t = `con (`rec' ze su t)
{-# DISPLAY `con (Lam _ _ , b , refl) = `λ b #-}
{-# DISPLAY `con (App _ _ , f , t , refl) = f `∙ t #-}
{-# DISPLAY `con (InL _ _ , t , refl) = `i₁ t #-}
{-# DISPLAY `con (InR _ _ , t , refl) = `i₂ t #-}
{-# DISPLAY `con (Cas _ _ _ , t , l , r , refl) = `case t l r #-}
{-# DISPLAY `con (Zro , refl) = `0 #-}
{-# DISPLAY `con (Suc , t , refl) = `1+ t #-}
{-# DISPLAY `con (Rec , ze , su , t , refl) = `rec ze su t #-}
infix 3 _⊢_∋_↝_ _⊢_∋_↝⋆_
data _⊢_∋_↝_ Γ : ∀ τ → Term τ Γ → Term τ Γ → Set where
β : ∀ t (u : Term σ Γ) → Γ ⊢ τ ∋ `λ t `∙ u ↝ t [ u /0]
ι₁ : ∀ (t : Term σ Γ) l (r : Term ν (τ ∷ Γ)) → Γ ⊢ ν ∋ `case (`i₁ t) l r ↝ l [ t /0]
ι₂ : ∀ (t : Term τ Γ) (l : Term ν (σ ∷ Γ)) r → Γ ⊢ ν ∋ `case (`i₂ t) l r ↝ r [ t /0]
ιz : ∀ ze su → Γ ⊢ σ ∋ `rec ze su `0 ↝ ze
ιs : ∀ ze su t → Γ ⊢ σ ∋ `rec ze su (`1+ t) ↝ sub (base vl^Tm ∙ t ∙ `rec ze su t) su
[λ] : (σ ∷ Γ) ⊢ τ ∋ t ↝ u → Γ ⊢ σ ⇒ τ ∋ `λ t ↝ `λ u
[∙]₁ : ∀ f → Γ ⊢ σ ∋ t ↝ u → Γ ⊢ τ ∋ f `∙ t ↝ f `∙ u
[∙]₂ : Γ ⊢ σ ⇒ τ ∋ f ↝ g → ∀ t → Γ ⊢ τ ∋ f `∙ t ↝ g `∙ t
[i₁] : Γ ⊢ σ ∋ t ↝ u → Γ ⊢ σ + τ ∋ `i₁ t ↝ `i₁ u
[i₂] : Γ ⊢ τ ∋ t ↝ u → Γ ⊢ σ + τ ∋ `i₂ t ↝ `i₂ u
[1+] : Γ ⊢ ℕ ∋ t ↝ u → Γ ⊢ ℕ ∋ `1+ t ↝ `1+ u
[c]₁ : Γ ⊢ σ + τ ∋ t ↝ u → ∀ l r → Γ ⊢ ν ∋ `case t l r ↝ `case u l r
[c]₂ : ∀ t → σ ∷ Γ ⊢ ν ∋ l ↝ m → (r : Term ν (τ ∷ Γ)) → Γ ⊢ ν ∋ `case t l r ↝ `case t m r
[c]₃ : ∀ t → (l : Term ν (σ ∷ Γ)) → τ ∷ Γ ⊢ ν ∋ r ↝ s → Γ ⊢ ν ∋ `case t l r ↝ `case t l s
[r]₁ : Γ ⊢ σ ∋ ze ↝ ze′ → ∀ su t → Γ ⊢ σ ∋ `rec ze su t ↝ `rec ze′ su t
[r]₂ : ∀ ze → σ ∷ ℕ ∷ Γ ⊢ σ ∋ su ↝ su′ → ∀ t → Γ ⊢ σ ∋ `rec ze su t ↝ `rec ze su′ t
[r]₃ : ∀ ze su → Γ ⊢ ℕ ∋ t ↝ t′ → Γ ⊢ σ ∋ `rec ze su t ↝ `rec ze su t′
tgt : ∀ {Γ σ t u} → Γ ⊢ σ ∋ t ↝ u → Term σ Γ
tgt {u = u} _ = u
_⊢_∋_↝⋆_ : ∀ Γ σ → Term σ Γ → Term σ Γ → Set
Γ ⊢ σ ∋ t ↝⋆ u = Star (Γ ⊢ σ ∋_↝_) t u
th^↝ : ∀ ρ → Γ ⊢ σ ∋ t ↝ u → Δ ⊢ σ ∋ ren ρ t ↝ ren ρ u
th^↝ ρ (β t u) = subst (_ ⊢ _ ∋ ren ρ (`λ t `∙ u) ↝_) (renβ TermD t (ε ∙ u) ρ) (β _ _)
th^↝ ρ (ι₁ t l r) = subst (_ ⊢ _ ∋ ren ρ (`case (`i₁ t) l r) ↝_) (renβ TermD l (ε ∙ t) ρ) (ι₁ _ _ _)
th^↝ ρ (ι₂ t l r) = subst (_ ⊢ _ ∋ ren ρ (`case (`i₂ t) l r) ↝_) (renβ TermD r (ε ∙ t) ρ) (ι₂ _ _ _)
th^↝ ρ (ιz ze su) = ιz (ren ρ ze) (ren _ su)
th^↝ ρ (ιs ze su t) = subst (_ ⊢ _ ∋ ren ρ (`rec ze su (`1+ t)) ↝_) (renβ TermD su (ε ∙ t ∙ `rec ze su t) ρ) (ιs _ _ _)
th^↝ ρ ([λ] r) = [λ] (th^↝ _ r)
th^↝ ρ ([∙]₁ f r) = [∙]₁ (ren ρ f) (th^↝ ρ r)
th^↝ ρ ([∙]₂ r t) = [∙]₂ (th^↝ ρ r) (ren ρ t)
th^↝ ρ ([i₁] c) = [i₁] (th^↝ ρ c)
th^↝ ρ ([i₂] c) = [i₂] (th^↝ ρ c)
th^↝ ρ ([1+] c) = [1+] (th^↝ ρ c)
th^↝ ρ ([c]₁ c l r) = [c]₁ (th^↝ ρ c) (ren _ l) (ren _ r)
th^↝ ρ ([c]₂ t c r) = [c]₂ (ren ρ t) (th^↝ _ c) (ren _ r)
th^↝ ρ ([c]₃ t l c) = [c]₃ (ren ρ t) (ren _ l) (th^↝ _ c)
th^↝ ρ ([r]₁ c su t) = [r]₁ (th^↝ ρ c) (ren _ su) (ren ρ t)
th^↝ ρ ([r]₂ ze c t) = [r]₂ (ren ρ ze) (th^↝ _ c) (ren ρ t)
th^↝ ρ ([r]₃ ze su c) = [r]₃ (ren ρ ze) (ren _ su) (th^↝ ρ c)
sub^↝ : ∀ ρ → Γ ⊢ σ ∋ t ↝ u → Δ ⊢ σ ∋ sub ρ t ↝ sub ρ u
sub^↝ ρ (β t u) = subst (_ ⊢ _ ∋ sub ρ (`λ t `∙ u) ↝_) (subβ TermD t (ε ∙ u) ρ) (β _ _)
sub^↝ ρ (ι₁ t l r) = subst (_ ⊢ _ ∋ sub ρ (`case (`i₁ t) l r) ↝_) (subβ TermD l (ε ∙ t) ρ) (ι₁ _ _ _)
sub^↝ ρ (ι₂ t l r) = subst (_ ⊢ _ ∋ sub ρ (`case (`i₂ t) l r) ↝_) (subβ TermD r (ε ∙ t) ρ) (ι₂ _ _ _)
sub^↝ ρ (ιz ze su) = ιz (sub ρ ze) (sub _ su)
sub^↝ ρ (ιs ze su t) = subst (_ ⊢ _ ∋ sub ρ (`rec ze su (`1+ t)) ↝_) (subβ TermD su (ε ∙ t ∙ `rec ze su t) ρ) (ιs _ _ _)
sub^↝ ρ ([λ] r) = [λ] (sub^↝ _ r)
sub^↝ ρ ([∙]₁ f r) = [∙]₁ (sub ρ f) (sub^↝ ρ r)
sub^↝ ρ ([∙]₂ r t) = [∙]₂ (sub^↝ ρ r) (sub ρ t)
sub^↝ ρ ([i₁] c) = [i₁] (sub^↝ ρ c)
sub^↝ ρ ([i₂] c) = [i₂] (sub^↝ ρ c)
sub^↝ ρ ([1+] c) = [1+] (sub^↝ ρ c)
sub^↝ ρ ([c]₁ c l r) = [c]₁ (sub^↝ ρ c) (sub _ l) (sub _ r)
sub^↝ ρ ([c]₂ t c r) = [c]₂ (sub ρ t) (sub^↝ _ c) (sub _ r)
sub^↝ ρ ([c]₃ t l c) = [c]₃ (sub ρ t) (sub _ l) (sub^↝ _ c)
sub^↝ ρ ([r]₁ r su t) = [r]₁ (sub^↝ ρ r) (sub _ su) (sub ρ t)
sub^↝ ρ ([r]₂ ze r t) = [r]₂ (sub ρ ze) (sub^↝ _ r) (sub ρ t)
sub^↝ ρ ([r]₃ ze su r) = [r]₃ (sub ρ ze) (sub _ su) (sub^↝ ρ r)
[/0]^↝ : ∀ {σ τ Γ b b′} → (σ ∷ Γ) ⊢ τ ∋ b ↝ b′ → ∀ u → Γ ⊢ τ ∋ b [ u /0] ↝ b′ [ u /0]
[/0]^↝ r u = sub^↝ (u /0]) r
↝⋆ᴿ : Rel Term Term
rel ↝⋆ᴿ = _ ⊢_∋_↝⋆_
[v↦t↝⋆t] : ∀ {ρ : (Γ ─Env) Term Δ} → R.All ↝⋆ᴿ Γ ρ ρ
lookupᴿ [v↦t↝⋆t] k = S.ε
sub^↝⋆ : ∀ (t : Term σ Γ) {ρ ρ′} →
R.All ↝⋆ᴿ Γ ρ ρ′ → Δ ⊢ σ ∋ sub ρ t ↝⋆ sub ρ′ t
sub^↝⋆ t ρᴿ = Simulation.sim sim ρᴿ t where
sim : Simulation TermD Sub Sub ↝⋆ᴿ ↝⋆ᴿ
Simulation.thᴿ sim = λ ρ → S.gmap _ (th^↝ ρ)
Simulation.varᴿ sim = id
Simulation.algᴿ sim {ρᴬ = ρ₁} {ρᴮ = ρ₂} = λ where
(f `∙' t) ρᴿ (refl , fᴿ , tᴿ , _) → S.gmap _ (λ f → [∙]₂ f (sub ρ₁ t)) fᴿ
S.◅◅ S.gmap _ ([∙]₁ (sub ρ₂ f)) tᴿ
(`λ' b) ρᴿ (refl , bᴿ , _) → S.gmap `λ [λ] (bᴿ _ [v↦t↝⋆t])
(`i₁' t) ρᴿ (refl , tᴿ , _) → S.gmap `i₁ [i₁] tᴿ
(`i₂' t) ρᴿ (refl , tᴿ , _) → S.gmap `i₂ [i₂] tᴿ
`0' ρᴿ (refl , _) → S.ε
(`1+' t) ρᴿ (refl , tᴿ , _) → S.gmap `1+ [1+] tᴿ
(`case' t l r) ρᴿ (refl , tᴿ , lᴿ , rᴿ , _) →
S.gmap _ (λ c → [c]₁ c (sub _ l) (sub _ r)) tᴿ
S.◅◅ S.gmap _ (λ c → [c]₂ (sub ρ₂ t) c (sub _ r)) (lᴿ _ [v↦t↝⋆t])
S.◅◅ S.gmap _ ([c]₃ (sub ρ₂ t) (sub _ l)) (rᴿ _ [v↦t↝⋆t])
(`rec' ze su t) ρᴿ (refl , zeᴿ , suᴿ , tᴿ , _) →
S.gmap _ (λ c → [r]₁ c (sub _ su) (sub _ t)) zeᴿ
S.◅◅ S.gmap _ (λ c → [r]₂ (sub _ ze) c (sub _ t)) (suᴿ _ [v↦t↝⋆t])
S.◅◅ S.gmap _ ([r]₃ (sub _ ze) (sub _ su)) tᴿ
[/0]^↝⋆ : ∀ {σ τ Γ} t {u u′} → Γ ⊢ σ ∋ u ↝ u′ → Γ ⊢ τ ∋ t [ u /0] ↝⋆ t [ u′ /0]
[/0]^↝⋆ t r = sub^↝⋆ t ([v↦t↝⋆t] ∙ᴿ S.return r)
th⁻¹^`∙ : ∀ {σ τ Γ Δ} (u : Term τ Γ) {f : Term (σ ⇒ τ) Δ} {t} ρ → f `∙ t ≡ ren ρ u →
∃ λ f′ → ∃ λ t′ → f′ `∙ t′ ≡ u × f ≡ ren ρ f′ × t ≡ ren ρ t′
th⁻¹^`∙ (f′ `∙ t′) ρ refl = f′ , t′ , refl , refl , refl
th⁻¹^`λ : ∀ {σ τ Γ Δ} (u : Term (σ ⇒ τ) Γ) {b : Term τ (σ ∷ Δ)} ρ → `λ b ≡ ren ρ u →
∃ λ b′ → `λ b′ ≡ u × b ≡ ren (lift vl^Var (σ ∷ []) ρ) b′
th⁻¹^`λ (`λ b′) ρ refl = b′ , refl , refl
th⁻¹^↝ : ∀ {σ Γ Δ u′} t ρ → Δ ⊢ σ ∋ ren ρ t ↝ u′ →
∃ λ u → u′ ≡ ren ρ u × Γ ⊢ σ ∋ t ↝ u
th⁻¹^↝ (`λ b `∙ t) ρ (β _ _) = b [ t /0] , renβ TermD b (ε ∙ t) ρ , β b t
th⁻¹^↝ (`case (`i₁ t) b₁ b₂) ρ (ι₁ _ _ _) = b₁ [ t /0] , renβ TermD b₁ (ε ∙ t) ρ , ι₁ t b₁ b₂
th⁻¹^↝ (`case (`i₂ t) b₁ b₂) ρ (ι₂ _ _ _) = b₂ [ t /0] , renβ TermD b₂ (ε ∙ t) ρ , ι₂ t b₁ b₂
th⁻¹^↝ (`rec ze su `0) ρ (ιz _ _) = ze , refl , ιz ze su
th⁻¹^↝ (`rec ze su (`1+ t)) ρ (ιs _ _ _) =
sub (base vl^Tm ∙ t ∙ `rec ze su t) su , renβ TermD su (ε ∙ t ∙ `rec ze su t) ρ , ιs ze su t
th⁻¹^↝ (`λ t) ρ ([λ] r) =
let (t′ , eq , r′) = th⁻¹^↝ t _ r in `λ t′ , cong `λ eq , [λ] r′
th⁻¹^↝ (f `∙ t) ρ ([∙]₁ ._ r) =
let (t′ , eq , r′) = th⁻¹^↝ t ρ r in f `∙ t′ , cong (ren ρ f `∙_) eq , [∙]₁ _ r′
th⁻¹^↝ (f `∙ t) ρ ([∙]₂ r ._) =
let (f′ , eq , r′) = th⁻¹^↝ f ρ r in f′ `∙ t , cong (_`∙ ren ρ t) eq , [∙]₂ r′ _
th⁻¹^↝ (`i₁ t) ρ ([i₁] r) =
let (t′ , eq , r′) = th⁻¹^↝ t ρ r in (`i₁ t′ , cong `i₁ eq , [i₁] r′)
th⁻¹^↝ (`i₂ t) ρ ([i₂] r) =
let (t′ , eq , r′) = th⁻¹^↝ t ρ r in (`i₂ t′ , cong `i₂ eq , [i₂] r′)
th⁻¹^↝ (`1+ t) ρ ([1+] r) =
let (t′ , eq , r′) = th⁻¹^↝ t ρ r in (`1+ t′ , cong `1+ eq , [1+] r′)
th⁻¹^↝ (`case t b₁ b₂) ρ ([c]₁ r _ _) = let (t′ , eq , r′) = th⁻¹^↝ t ρ r in
(`case t′ b₁ b₂ , cong (λ r → `case r (ren _ b₁) (ren _ b₂)) eq , [c]₁ r′ b₁ b₂)
th⁻¹^↝ (`case t b₁ b₂) ρ ([c]₂ _ r _) = let (b₁′ , eq , r′) = th⁻¹^↝ b₁ _ r in
(`case t b₁′ b₂ , cong (λ r → `case (ren ρ t) r (ren _ b₂)) eq , [c]₂ t r′ b₂)
th⁻¹^↝ (`case t b₁ b₂) ρ ([c]₃ _ _ r) = let (b₂′ , eq , r′) = th⁻¹^↝ b₂ _ r in
(`case t b₁ b₂′ , cong (`case (ren ρ t) (ren _ b₁)) eq , [c]₃ t b₁ r′)
th⁻¹^↝ (`rec ze su t) ρ ([r]₁ r _ _) = let (ze′ , eq , r′) = th⁻¹^↝ ze _ r in
(`rec ze′ su t , cong (λ r → `rec r (ren _ su) (ren ρ t)) eq , [r]₁ r′ su t)
th⁻¹^↝ (`rec ze su t) ρ ([r]₂ _ r _) = let (su′ , eq , r′) = th⁻¹^↝ su _ r in
(`rec ze su′ t , cong (λ r → `rec (ren ρ ze) r (ren ρ t)) eq , [r]₂ ze r′ t)
th⁻¹^↝ (`rec ze su t) ρ ([r]₃ _ _ r) = let (t′ , eq , r′) = th⁻¹^↝ t _ r in
(`rec ze su t′ , cong (`rec (ren ρ ze) (ren _ su)) eq , [r]₃ ze su r′)
th⁻¹^↝⋆ : ∀ {σ Γ Δ u′} t ρ → Δ ⊢ σ ∋ ren ρ t ↝⋆ u′ →
∃ λ u → u′ ≡ ren ρ u × Γ ⊢ σ ∋ t ↝⋆ u
th⁻¹^↝⋆ {σ} t ρ rs = go t ρ refl rs where
go : ∀ {Γ Δ} t ρ → ∀ {t′ u′} → t′ ≡ ren ρ t → Δ ⊢ σ ∋ t′ ↝⋆ u′ →
∃ λ u → u′ ≡ ren ρ u × Γ ⊢ σ ∋ t ↝⋆ u
go t ρ refl Star.ε = t , refl , Star.ε
go t ρ refl (r Star.◅ rs) =
let (u , eq , r′) = th⁻¹^↝ t ρ r in
let (v , eq′ , rs′) = go u ρ eq rs in
v , eq′ , r′ Star.◅ rs′
Closed : ∀ {σ Γ} → (Term σ Γ → Term σ Γ → Set) →
(Term σ Γ → Set) → Term σ Γ → Set
Closed red R t = ∀ {u} → red t u → R u
Closed⇒Closed⋆ : ∀ {σ Γ red R} → (∀ {t : Term σ Γ} → R t → Closed red R t) →
∀ {t} → R t → Closed (Star red) R t
Closed⇒Closed⋆ cl tᴿ Star.ε = tᴿ
Closed⇒Closed⋆ cl tᴿ (r Star.◅ rs) = Closed⇒Closed⋆ cl (cl tᴿ r) rs
infix 3 _⊢sn_∋_<_ _⊢sn_∋_
data _⊢sn_∋_<_ Γ σ (t : Term σ Γ) : Size → Set where
sn : ∀ {i} → Closed (Γ ⊢ σ ∋_↝_) (Γ ⊢sn σ ∋_< i) t → Γ ⊢sn σ ∋ t < ↑ i
_⊢sn_∋_ = _⊢sn_∋_< _
Closed-sn : ∀ {σ Γ t} → Γ ⊢sn σ ∋ t → Closed (Γ ⊢ σ ∋_↝_) (Γ ⊢sn σ ∋_) t
Closed-sn (sn t^SN) = t^SN
Closed⋆-sn : ∀ {σ Γ t} → Γ ⊢sn σ ∋ t → Closed (Γ ⊢ σ ∋_↝⋆_) (Γ ⊢sn σ ∋_) t
Closed⋆-sn = Closed⇒Closed⋆ Closed-sn
th^sn : ∀ {σ Γ Δ t} ρ → Γ ⊢sn σ ∋ t → Δ ⊢sn σ ∋ ren ρ t
th^sn ρ (sn t^SN) = sn $ λ r →
let (_ , eq , r′) = th⁻¹^↝ _ ρ r
in subst (_ ⊢sn _ ∋_) (sym eq) $ th^sn ρ (t^SN r′)
th⁻¹^sn : ∀ {σ Γ Δ t} ρ → Δ ⊢sn σ ∋ ren ρ t → Γ ⊢sn σ ∋ t
th⁻¹^sn ρ (sn tρ^sn) = sn (λ r → th⁻¹^sn ρ (tρ^sn (th^↝ ρ r)))
sub⁻¹^sn : ∀ {σ Γ Δ} t ρ → Δ ⊢sn σ ∋ (sub ρ t) → Γ ⊢sn σ ∋ t
sub⁻¹^sn t ρ (sn tρ^sn) = sn (λ r → sub⁻¹^sn _ ρ (tρ^sn (sub^↝ ρ r)))
[/0]⁻¹^sn : ∀ {σ τ Γ} t u → Γ ⊢sn τ ∋ (t [ u /0]) → (σ ∷ Γ) ⊢sn τ ∋ t
[/0]⁻¹^sn t u t[u]^sn = sub⁻¹^sn t (u /0]) t[u]^sn
`λ^sn : ∀ {σ τ Γ t} → (σ ∷ Γ) ⊢sn τ ∋ t → Γ ⊢sn σ ⇒ τ ∋ `λ t
`λ^sn (sn tᴿ) = sn λ { ([λ] r) → `λ^sn (tᴿ r) }
`i₁^sn : ∀ {σ τ Γ t} → Γ ⊢sn σ ∋ t → Γ ⊢sn σ + τ ∋ `i₁ t
`i₁^sn (sn tᴿ) = sn λ { ([i₁] r) → `i₁^sn (tᴿ r) }
`i₂^sn : ∀ {σ τ Γ t} → Γ ⊢sn τ ∋ t → Γ ⊢sn σ + τ ∋ `i₂ t
`i₂^sn (sn tᴿ) = sn λ { ([i₂] r) → `i₂^sn (tᴿ r) }
`0^sn : ∀ {Γ} → Γ ⊢sn ℕ ∋ `0
`0^sn = sn (λ ())
`1+^sn : ∀ {Γ t} → Γ ⊢sn ℕ ∋ t → Γ ⊢sn ℕ ∋ `1+ t
`1+^sn (sn tᴿ) = sn λ { ([1+] r) → `1+^sn (tᴿ r) }
`∙t⁻¹^sn : ∀ {σ τ Γ f t i} → Γ ⊢sn τ ∋ (f `∙ t) < i → Γ ⊢sn σ ⇒ τ ∋ f < i
`∙t⁻¹^sn (sn ft^sn) = sn (λ r → `∙t⁻¹^sn (ft^sn ([∙]₂ r _)))
f`∙⁻¹^sn : ∀ {σ τ Γ f t i} → Γ ⊢sn τ ∋ (f `∙ t) < i → Γ ⊢sn σ ∋ t < i
f`∙⁻¹^sn (sn ft^sn) = sn (λ r → f`∙⁻¹^sn (ft^sn ([∙]₁ _ r)))
`∙⁻¹^sn : ∀ {σ τ Γ f t i} → Γ ⊢sn τ ∋ (f `∙ t) < i → Γ ⊢sn σ ⇒ τ ∋ f < i × Γ ⊢sn σ ∋ t < i
`∙⁻¹^sn ft^sn = `∙t⁻¹^sn ft^sn , f`∙⁻¹^sn ft^sn
`λ⁻¹^sn : ∀ {σ τ Γ t i} → Γ ⊢sn σ ⇒ τ ∋ `λ t < i → (σ ∷ Γ) ⊢sn τ ∋ t < i
`λ⁻¹^sn (sn λt^sn) = sn (λ r → `λ⁻¹^sn (λt^sn ([λ] r)))
`i₁⁻¹^sn : ∀ {σ τ Γ t i} → Γ ⊢sn σ + τ ∋ `i₁ t < i → Γ ⊢sn σ ∋ t < i
`i₁⁻¹^sn (sn i₁t^sn) = sn (λ r → `i₁⁻¹^sn (i₁t^sn ([i₁] r)))
`i₂⁻¹^sn : ∀ {σ τ Γ t i} → Γ ⊢sn σ + τ ∋ `i₂ t < i → Γ ⊢sn τ ∋ t < i
`i₂⁻¹^sn (sn i₂t^sn) = sn (λ r → `i₂⁻¹^sn (i₂t^sn ([i₂] r)))
`1+⁻¹^sn : ∀ {Γ t i} → Γ ⊢sn ℕ ∋ `1+ t < i → Γ ⊢sn ℕ ∋ t < i
`1+⁻¹^sn (sn st^sn) = sn (λ r → `1+⁻¹^sn (st^sn ([1+] r)))
`case₁⁻¹^sn : ∀ {σ τ ν Γ t l r i} → Γ ⊢sn ν ∋ `case t l r < i → Γ ⊢sn σ + τ ∋ t < i
`case₁⁻¹^sn (sn c^sn) = sn (λ r → `case₁⁻¹^sn (c^sn ([c]₁ r _ _)))
`case₂⁻¹^sn : ∀ {σ τ ν Γ t l i} {r : Term ν (τ ∷ Γ)} → Γ ⊢sn ν ∋ `case t l r < i → (σ ∷ Γ) ⊢sn ν ∋ l < i
`case₂⁻¹^sn (sn c^sn) = sn (λ r → `case₂⁻¹^sn (c^sn ([c]₂ _ r _)))
`case₃⁻¹^sn : ∀ {σ τ ν Γ t r i} {l : Term ν (σ ∷ Γ)} → Γ ⊢sn ν ∋ `case t l r < i → (τ ∷ Γ) ⊢sn ν ∋ r < i
`case₃⁻¹^sn (sn c^sn) = sn (λ r → `case₃⁻¹^sn (c^sn ([c]₃ _ _ r)))
`case⁻¹^sn : ∀ {σ τ ν Γ t l r i} → Γ ⊢sn ν ∋ `case t l r < i →
Γ ⊢sn σ + τ ∋ t < i × (σ ∷ Γ) ⊢sn ν ∋ l < i × (τ ∷ Γ) ⊢sn ν ∋ r < i
`case⁻¹^sn c^sn = `case₁⁻¹^sn c^sn , `case₂⁻¹^sn c^sn , `case₃⁻¹^sn c^sn
`rec₁⁻¹^sn : ∀ {σ Γ ze su t i} → Γ ⊢sn σ ∋ `rec ze su t < i → Γ ⊢sn σ ∋ ze < i
`rec₁⁻¹^sn (sn r^sn) = sn (λ r → `rec₁⁻¹^sn (r^sn ([r]₁ r _ _)))
`rec₂⁻¹^sn : ∀ {σ Γ ze su t i} → Γ ⊢sn σ ∋ `rec ze su t < i → (σ ∷ ℕ ∷ Γ) ⊢sn σ ∋ su < i
`rec₂⁻¹^sn (sn r^sn) = sn (λ r → `rec₂⁻¹^sn (r^sn ([r]₂ _ r _)))
`rec₃⁻¹^sn : ∀ {σ Γ ze su t i} → Γ ⊢sn σ ∋ `rec ze su t < i → Γ ⊢sn ℕ ∋ t < i
`rec₃⁻¹^sn (sn r^sn) = sn (λ r → `rec₃⁻¹^sn (r^sn ([r]₃ _ _ r)))
`rec⁻¹^sn : ∀ {σ Γ ze su t i} → Γ ⊢sn σ ∋ `rec ze su t < i →
Γ ⊢sn σ ∋ ze < i × (σ ∷ ℕ ∷ Γ) ⊢sn σ ∋ su < i × Γ ⊢sn ℕ ∋ t < i
`rec⁻¹^sn r^sn = `rec₁⁻¹^sn r^sn , `rec₂⁻¹^sn r^sn , `rec₃⁻¹^sn r^sn
infix 3 _∣_⊢_ _∣_⊢[_]_∋_<_ _∣_⊢[_]_∋_ _∣_⊢sn_∋_
data _∣_⊢_ Γ α : Type → Set where
<> : Γ ∣ α ⊢ α
app : ∀ {σ τ} → Γ ∣ α ⊢ σ ⇒ τ → Term σ Γ → Γ ∣ α ⊢ τ
cas : ∀ {σ τ ν} → Γ ∣ α ⊢ σ + τ → Term ν (σ ∷ Γ) → Term ν (τ ∷ Γ) → Γ ∣ α ⊢ ν
rec : ∀ {σ} → Term σ Γ → Term σ (σ ∷ ℕ ∷ Γ) → Γ ∣ α ⊢ ℕ → Γ ∣ α ⊢ σ
data _∣_⊢[_]_∋_<_ Γ α (R : ∀ Γ σ → Term σ Γ → Size → Set) : ∀ σ → Γ ∣ α ⊢ σ → Size → Set where
<> : ∀ {i} → Γ ∣ α ⊢[ R ] α ∋ <> < ↑ i
app : ∀ {i σ τ c t} → Γ ∣ α ⊢[ R ] σ ⇒ τ ∋ c < i → R Γ σ t i → Γ ∣ α ⊢[ R ] τ ∋ app c t < ↑ i
cas : ∀ {i σ τ ν c l r} → Γ ∣ α ⊢[ R ] σ + τ ∋ c < i →
R (σ ∷ Γ) ν l i → R (τ ∷ Γ) ν r i → Γ ∣ α ⊢[ R ] ν ∋ cas c l r < ↑ i
rec : ∀ {σ ze su c i} → R Γ σ ze i → R (σ ∷ ℕ ∷ Γ) σ su i →
Γ ∣ α ⊢[ R ] ℕ ∋ c < i → Γ ∣ α ⊢[ R ] σ ∋ rec ze su c < ↑ i
_∣_⊢[_]_∋_ = _∣_⊢[_]_∋_< _
_∣_⊢sn_∋_ = _∣_⊢[ _⊢sn_∋_<_ ]_∋_
cut : ∀ {Γ α σ} → Term α Γ → Γ ∣ α ⊢ σ → Term σ Γ
cut t <> = t
cut t (app c u) = cut t c `∙ u
cut t (cas c l r) = `case (cut t c) l r
cut t (rec ze su c) = `rec ze su (cut t c)
cut^↝ : ∀ {Γ α σ t u} c → Γ ⊢ α ∋ t ↝ u → Γ ⊢ σ ∋ cut t c ↝ cut u c
cut^↝ <> red = red
cut^↝ (app c t) red = [∙]₂ (cut^↝ c red) t
cut^↝ (cas c l r) red = [c]₁ (cut^↝ c red) l r
cut^↝ (rec ze su c) red = [r]₃ ze su (cut^↝ c red)
cut^↝⋆ : ∀ {Γ α σ t u} c → Γ ⊢ α ∋ t ↝⋆ u → Γ ⊢ σ ∋ cut t c ↝⋆ cut u c
cut^↝⋆ c = S.gmap (flip cut c) (cut^↝ c)
data Neutral {Γ σ} : Term σ Γ → Set where
var : ∀ v → Neutral (`var v)
app : ∀ {τ} f (t : Term τ Γ) → Neutral (f `∙ t)
cas : ∀ {σ τ} (t : Term (σ + τ) Γ) l r → Neutral (`case t l r)
rec : ∀ ze su t → Neutral (`rec ze su t)
cut⁻¹‿sn^↝ : ∀ {Γ α σ u c t} → Γ ∣ α ⊢sn σ ∋ c → Neutral t → Γ ⊢ σ ∋ cut t c ↝ u →
(∃ λ t′ → u ≡ cut t′ c × Γ ⊢ α ∋ t ↝ t′)
⊎ (∃ λ c′ → u ≡ cut t c′ × Γ ∣ α ⊢sn σ ∋ c′
× ∀ t′ → Γ ⊢ σ ∋ cut t′ c ↝ cut t′ c′)
cut⁻¹‿sn^↝ <> ne r = inj₁ (_ , refl , r)
cut⁻¹‿sn^↝ (app <> t^sn) () (β b t)
cut⁻¹‿sn^↝ (cas <> l^sn r^sn) () (ι₁ t l r)
cut⁻¹‿sn^↝ (cas <> l^sn r^sn) () (ι₂ t l r)
cut⁻¹‿sn^↝ (rec ze^sn su^sn <>) () (ιz ze su)
cut⁻¹‿sn^↝ (rec ze^sn su^sn <>) () (ιs ze su t)
cut⁻¹‿sn^↝ (app c^sn t^sn) ne ([∙]₁ _ r) =
inj₂ (_ , refl , app c^sn (Closed-sn t^sn r) , λ u → [∙]₁ _ r)
cut⁻¹‿sn^↝ (cas c^sn l^sn r^sn) ne ([c]₂ t red r) =
inj₂ (cas _ _ r , refl , cas c^sn (Closed-sn l^sn red) r^sn , λ u → [c]₂ _ red r)
cut⁻¹‿sn^↝ (cas c^sn l^sn r^sn) ne ([c]₃ t l red) =
inj₂ (cas _ l _ , refl , cas c^sn l^sn (Closed-sn r^sn red) , λ u → [c]₃ _ l red)
cut⁻¹‿sn^↝ (rec ze^sn su^sn c^sn) ne ([r]₁ red su t) =
inj₂ (rec _ su _ , refl , rec (Closed-sn ze^sn red) su^sn c^sn , λ u → [r]₁ red su _)
cut⁻¹‿sn^↝ (rec ze^sn su^sn c^sn) ne ([r]₂ ze red t) =
inj₂ (rec ze _ _ , refl , rec ze^sn (Closed-sn su^sn red) c^sn , λ u → [r]₂ ze red _)
cut⁻¹‿sn^↝ (app c^sn t^sn) ne ([∙]₂ r t) with cut⁻¹‿sn^↝ c^sn ne r
... | inj₁ (t′ , eq , r′) = inj₁ (t′ , cong (_`∙ t) eq , r′)
... | inj₂ (c′ , eq , c′^sn , r′) =
inj₂ (app c′ t , cong (_`∙ t) eq , app c′^sn t^sn , λ u → [∙]₂ (r′ u) t)
cut⁻¹‿sn^↝ (cas c^sn l^sn r^sn) ne ([c]₁ red l r) with cut⁻¹‿sn^↝ c^sn ne red
... | inj₁ (t′ , eq , r′) = inj₁ (t′ , cong (λ t → `case t l r) eq , r′)
... | inj₂ (c′ , eq , c′^sn , r′) =
inj₂ (_ , cong (λ t → `case t l r) eq , cas c′^sn l^sn r^sn , λ u → [c]₁ (r′ u) l r)
cut⁻¹‿sn^↝ (rec ze^sn su^sn c^sn) ne ([r]₃ ze su red) with cut⁻¹‿sn^↝ c^sn ne red
... | inj₁ (t′ , eq , r′) = inj₁ (t′ , cong (`rec ze su) eq , r′)
... | inj₂ (c′ , eq , c′^sn , r′) =
inj₂ (_ , cong (`rec ze su) eq , rec ze^sn su^sn c′^sn , (λ u → [r]₃ _ _ (r′ u)))
cut⁻¹^↝ : ∀ {Γ α σ u} c {v : Var α Γ} → Γ ⊢ σ ∋ cut (`var v) c ↝ u →
∃ λ c′ → u ≡ cut (`var v) c′
cut⁻¹^↝ (app <> t) ([∙]₁ _ r) = app <> _ , refl
cut⁻¹^↝ (app c t) ([∙]₁ _ r) = app c _ , refl
cut⁻¹^↝ (app c t) ([∙]₂ r _) =
let (c′ , eq) = cut⁻¹^↝ c r in app c′ _ , cong (_`∙ _) eq
cut⁻¹^↝ (cas <> l r) ([c]₂ _ _ _) = cas <> _ _ , refl
cut⁻¹^↝ (cas <> l r) ([c]₃ _ _ _) = cas <> _ _ , refl
cut⁻¹^↝ (cas c _ _) ([c]₁ r _ _) =
let (c′ , eq) = cut⁻¹^↝ c r in cas c′ _ _ , cong (λ c → `case c _ _) eq
cut⁻¹^↝ (cas c l r) ([c]₂ _ _ _) = cas c _ _ , refl
cut⁻¹^↝ (cas c l r) ([c]₃ _ _ _) = cas c _ _ , refl
cut⁻¹^↝ (rec ze su <>) ([r]₁ _ _ _) = rec _ _ <> , refl
cut⁻¹^↝ (rec ze su <>) ([r]₂ _ _ _) = rec _ _ <> , refl
cut⁻¹^↝ (rec ze su c) ([r]₁ _ _ _) = rec _ _ c , refl
cut⁻¹^↝ (rec ze su c) ([r]₂ _ _ _) = rec _ _ c , refl
cut⁻¹^↝ (rec ze su c) ([r]₃ _ _ r) =
let (c′ , eq) = cut⁻¹^↝ c r in rec _ _ c′ , cong (`rec _ _) eq
cut⁻¹^↝ <> ()
cut⁻¹^sn : ∀ {Γ α σ} t c → Γ ⊢sn σ ∋ cut t c → (Γ ∣ α ⊢sn σ ∋ c) × (Γ ⊢sn α ∋ t)
cut⁻¹^sn t <> t^sn = <> , t^sn
cut⁻¹^sn t (app c u) c[t]u^sn =
let (c[t]^sn , u^sn) = `∙⁻¹^sn c[t]u^sn in
let (c^sn , t^sn) = cut⁻¹^sn t c c[t]^sn in app c^sn u^sn , t^sn
cut⁻¹^sn t (cas c l r) c[t]lr^sn =
let (c[t]^sn , l^sn , r^sn) = `case⁻¹^sn c[t]lr^sn in
let (c^sn , t^sn) = cut⁻¹^sn t c c[t]^sn in cas c^sn l^sn r^sn , t^sn
cut⁻¹^sn t (rec su ze c) zsc[t]^sn =
let (z^sn , s^sn , c[t]^sn) = `rec⁻¹^sn zsc[t]^sn in
let (c^sn , t^sn) = cut⁻¹^sn t c c[t]^sn in rec z^sn s^sn c^sn , t^sn
`var^sne : ∀ {σ Γ} v → Γ ⊢sn σ ∋ `var v
`var^sne v = sn (λ ())
`∙^sne : ∀ {Γ α σ τ t} {v : Var α Γ} c → Γ ⊢sn σ ⇒ τ ∋ cut (`var v) c → Γ ⊢sn σ ∋ t →
Γ ⊢sn τ ∋ cut (`var v) (app c t)
`∙^sne c f^sne t^sn = sn (go c f^sne t^sn) where
go : ∀ {Γ α σ τ t} {v : Var α Γ} c → Γ ⊢sn σ ⇒ τ ∋ cut (`var v) c → Γ ⊢sn σ ∋ t →
Closed (Γ ⊢ τ ∋_↝_) (Γ ⊢sn τ ∋_) (cut (`var v) (app c t))
go <> f^sne t^sn ([∙]₂ () t)
go c f^sne (sn t^sn) ([∙]₁ _ r) = sn (go c f^sne (t^sn r))
go c (sn f^sne) t^sn ([∙]₂ r t) =
let (c′ , eq) = cut⁻¹^↝ c r in let r′ = subst (_ ⊢ _ ∋ _ ↝_) eq r in
subst (λ g → _ ⊢sn _ ∋ g `∙ t) (sym eq) (sn (go c′ (f^sne r′) t^sn))
`case^sne : ∀ {Γ α σ τ ν l r} {v : Var α Γ} c → Γ ⊢sn σ + τ ∋ cut (`var v) c →
(σ ∷ Γ) ⊢sn ν ∋ l → (τ ∷ Γ) ⊢sn ν ∋ r → Γ ⊢sn ν ∋ cut (`var v) (cas c l r)
`case^sne c s^sn l^sn r^sn = sn (go c s^sn l^sn r^sn) where
go : ∀ {Γ α σ τ ν l r} {v : Var α Γ} c → Γ ⊢sn σ + τ ∋ cut (`var v) c →
(σ ∷ Γ) ⊢sn ν ∋ l → (τ ∷ Γ) ⊢sn ν ∋ r → Closed (Γ ⊢ ν ∋_↝_) (Γ ⊢sn ν ∋_) (cut (`var v) (cas c l r))
go <> s^sne l^sn r^sn ([c]₁ () _ _)
go c s^sne (sn l^sn) r^sn ([c]₂ _ red _) = sn (go c s^sne (l^sn red) r^sn)
go c s^sne l^sn (sn r^sn) ([c]₃ _ _ red) = sn (go c s^sne l^sn (r^sn red))
go c (sn s^sne) l^sn r^sn ([c]₁ red l r) =
let (c′ , eq) = cut⁻¹^↝ c red in let red′ = subst (_ ⊢ _ ∋ _ ↝_) eq red in
subst (λ g → _ ⊢sn _ ∋ `case g l r) (sym eq) (sn (go c′ (s^sne red′) l^sn r^sn))
`rec^sne : ∀ {Γ α σ ze su} {v : Var α Γ} c → Γ ⊢sn ℕ ∋ cut (`var v) c →
Γ ⊢sn σ ∋ ze → σ ∷ ℕ ∷ Γ ⊢sn σ ∋ su → Γ ⊢sn σ ∋ cut (`var v) (rec ze su c)
`rec^sne c n^sn ze^sn su^sn = sn (go c n^sn ze^sn su^sn) where
go : ∀ {Γ α σ ze su} {v : Var α Γ} c → Γ ⊢sn ℕ ∋ cut (`var v) c → Γ ⊢sn σ ∋ ze →
σ ∷ ℕ ∷ Γ ⊢sn σ ∋ su → Closed (Γ ⊢ σ ∋_↝_) (Γ ⊢sn σ ∋_) (cut (`var v) (rec ze su c))
go <> n^sne ze^sn su^sn ([r]₃ _ _ ())
go c n^sne (sn ze^sn) su^sn ([r]₁ red _ _) = sn (go c n^sne (ze^sn red) su^sn)
go c n^sne ze^sn (sn su^sn) ([r]₂ _ red _) = sn (go c n^sne ze^sn (su^sn red))
go c (sn n^sne) ze^sn su^sn ([r]₃ _ _ red) =
let (c′ , eq) = cut⁻¹^↝ c red in let red′ = subst (_ ⊢ _ ∋ _ ↝_) eq red in
subst (λ g → _ ⊢sn _ ∋ `rec _ _ g) (sym eq) (sn (go c′ (n^sne red′) ze^sn su^sn))
cut^sn : ∀ {Γ α σ} v {c} → Γ ∣ α ⊢sn σ ∋ c → Γ ⊢sn σ ∋ cut (`var v) c
cut^sn v <> = `var^sne v
cut^sn v {app c t} (app c^sn t^sn) = `∙^sne c (cut^sn v c^sn) t^sn
cut^sn v {cas c l r} (cas c^sn l^sn r^sn) = `case^sne c (cut^sn v c^sn) l^sn r^sn
cut^sn v {rec ze su c} (rec ze^sn su^sn c^sn) = `rec^sne c (cut^sn v c^sn) ze^sn su^sn
_∘C_ : ∀ {Γ α β σ} → Γ ∣ β ⊢ σ → Γ ∣ α ⊢ β → Γ ∣ α ⊢ σ
<> ∘C c′ = c′
app c t ∘C c′ = app (c ∘C c′) t
cas c l r ∘C c′ = cas (c ∘C c′) l r
rec ze su c ∘C c′ = rec ze su (c ∘C c′)
cut-∘C : ∀ {Γ α β σ} t (c : Γ ∣ β ⊢ σ) (c′ : Γ ∣ α ⊢ β) →
cut (cut t c′) c ≡ cut t (c ∘C c′)
cut-∘C t <> c′ = refl
cut-∘C t (app c u) c′ = cong (_`∙ u) (cut-∘C t c c′)
cut-∘C t (cas c l r) c′ = cong (λ t → `case t l r) (cut-∘C t c c′)
cut-∘C t (rec ze su c) c′ = cong (`rec ze su) (cut-∘C t c c′)
∘Cᴿ : ∀ {Γ α R β σ c c′} → Γ ∣ β ⊢[ R ] σ ∋ c → Γ ∣ α ⊢[ R ] β ∋ c′ → Γ ∣ α ⊢[ R ] σ ∋ c ∘C c′
∘Cᴿ <> c′ᴿ = c′ᴿ
∘Cᴿ (app cᴿ tᴿ) c′ᴿ = app (∘Cᴿ cᴿ c′ᴿ) tᴿ
∘Cᴿ (cas cᴿ lᴿ rᴿ) c′ᴿ = cas (∘Cᴿ cᴿ c′ᴿ) lᴿ rᴿ
∘Cᴿ (rec zeᴿ suᴿ cᴿ) c′ᴿ = rec zeᴿ suᴿ (∘Cᴿ cᴿ c′ᴿ)
infix 3 _⊢↯_ _⊢↯sn_∋_
data _⊢↯_ (Γ : List Type) (τ : Type) : Set where
β : ∀ {σ} → Term τ (σ ∷ Γ) → Term σ Γ → Γ ⊢↯ τ
ι₁ : ∀ {σ₁ σ₂} → Term σ₁ Γ → Term τ (σ₁ ∷ Γ) → Term τ (σ₂ ∷ Γ) → Γ ⊢↯ τ
ι₂ : ∀ {σ₁ σ₂} → Term σ₂ Γ → Term τ (σ₁ ∷ Γ) → Term τ (σ₂ ∷ Γ) → Γ ⊢↯ τ
ιz : Term τ Γ → Term τ (τ ∷ ℕ ∷ Γ) → Γ ⊢↯ τ
ιs : Term τ Γ → Term τ (τ ∷ ℕ ∷ Γ) → Term ℕ Γ → Γ ⊢↯ τ
_⊢↯sn_∋_ : ∀ Γ τ → Γ ⊢↯ τ → Set
Γ ⊢↯sn τ ∋ β b u = (_ ∷ Γ) ⊢sn τ ∋ b × Γ ⊢sn _ ∋ u
Γ ⊢↯sn τ ∋ ι₁ t l r = Γ ⊢sn _ ∋ t × (_ ∷ Γ) ⊢sn _ ∋ l × (_ ∷ Γ) ⊢sn _ ∋ r
Γ ⊢↯sn τ ∋ ι₂ t l r = Γ ⊢sn _ ∋ t × (_ ∷ Γ) ⊢sn _ ∋ l × (_ ∷ Γ) ⊢sn _ ∋ r
Γ ⊢↯sn τ ∋ ιz ze su = Γ ⊢sn τ ∋ ze × (τ ∷ ℕ ∷ Γ) ⊢sn τ ∋ su
Γ ⊢↯sn τ ∋ ιs ze su t = Γ ⊢sn τ ∋ ze × (τ ∷ ℕ ∷ Γ) ⊢sn τ ∋ su × Γ ⊢sn ℕ ∋ t
unRed : ∀ {Γ τ} → Γ ⊢↯ τ → Term τ Γ
unRed (β b u) = `λ b `∙ u
unRed (ι₁ t l r) = `case (`i₁ t) l r
unRed (ι₂ t l r) = `case (`i₂ t) l r
unRed (ιz ze su) = `rec ze su `0
unRed (ιs ze su t) = `rec ze su (`1+ t)
unRed^Neutral : ∀ {Γ τ} (r : Γ ⊢↯ τ) → Neutral (unRed r)
unRed^Neutral (β b u) = app (`λ b) u
unRed^Neutral (ι₁ t l r) = cas (`i₁ t) l r
unRed^Neutral (ι₂ t l r) = cas (`i₂ t) l r
unRed^Neutral (ιz ze su) = rec ze su `0
unRed^Neutral (ιs ze su t) = rec ze su (`1+ t)
βιRed : ∀ {Γ τ} → Γ ⊢↯ τ → Term τ Γ
βιRed (β b u) = b [ u /0]
βιRed (ι₁ t l r) = l [ t /0]
βιRed (ι₂ t l r) = r [ t /0]
βιRed (ιz ze su) = ze
βιRed (ιs ze su t) = sub (base vl^Tm ∙ t ∙ `rec ze su t) su
fire : ∀ {Γ τ} r → Γ ⊢ τ ∋ unRed r ↝ βιRed r
fire (β b u) = β b u
fire (ι₁ t l r) = ι₁ t l r
fire (ι₂ t l r) = ι₂ t l r
fire (ιz ze su) = ιz ze su
fire (ιs ze su t) = ιs ze su t
c[fire]⁻¹^Closed-sn : ∀ {Γ α σ c} r → Γ ⊢↯sn α ∋ r → Γ ∣ α ⊢sn σ ∋ c →
Γ ⊢sn σ ∋ cut (βιRed r) c → Closed (Γ ⊢ σ ∋_↝_) (Γ ⊢sn σ ∋_) (cut (unRed r) c)
c[fire⁻¹]^Closed-sn : ∀ {Γ α σ} c r → Γ ⊢↯sn α ∋ r → Γ ∣ α ⊢sn σ ∋ c →
Γ ⊢sn σ ∋ cut (βιRed r) c → ∀ {t} → Γ ⊢ α ∋ unRed r ↝ t → Γ ⊢sn σ ∋ cut t c
c[fire]⁻¹^Closed-sn r r^sn c^sn c[r]^sn@(sn c[r]^sn′) red
with cut⁻¹‿sn^↝ c^sn (unRed^Neutral r) red
... | inj₁ (_ , refl , r′) = c[fire⁻¹]^Closed-sn _ r r^sn c^sn c[r]^sn r′
... | inj₂ (c′ , refl , c′^sn , red′) =
sn (c[fire]⁻¹^Closed-sn r r^sn c′^sn (c[r]^sn′ (red′ (βιRed r))))
c[fire⁻¹]^Closed-sn c (β _ _) _ c^sn c[r]^sn (β _ _) = c[r]^sn
c[fire⁻¹]^Closed-sn c (ι₁ _ _ _) _ c^sn c[r]^sn (ι₁ _ _ _) = c[r]^sn
c[fire⁻¹]^Closed-sn c (ι₂ _ _ _) _ c^sn c[r]^sn (ι₂ _ _ _) = c[r]^sn
c[fire⁻¹]^Closed-sn c (ιz _ _) _ c^sn c[r]^sn (ιz _ _) = c[r]^sn
c[fire⁻¹]^Closed-sn c (ιs _ _ _) _ c^sn c[r]^sn (ιs _ _ _) = c[r]^sn
c[fire⁻¹]^Closed-sn c (β b u) (b^sn , sn u^sn) c^sn c[r]^sn ([∙]₁ _ red) =
let c[r′]^sn = Closed⋆-sn c[r]^sn (cut^↝⋆ c ([/0]^↝⋆ b red)) in
sn (c[fire]⁻¹^Closed-sn (β b _) (b^sn , u^sn red) c^sn c[r′]^sn)
c[fire⁻¹]^Closed-sn c (β b u) (sn b^sn , u^sn) c^sn c[r]^sn ([∙]₂ ([λ] red) t) =
let c[r′]^sn = Closed-sn c[r]^sn (cut^↝ c ([/0]^↝ red u)) in
sn (c[fire]⁻¹^Closed-sn (β _ u) (b^sn red , u^sn) c^sn c[r′]^sn)
c[fire⁻¹]^Closed-sn c (ι₁ t l r) (sn t^sn , l^sn , r^sn) c^sn c[r]^sn ([c]₁ ([i₁] red) _ _) =
let c[r′]^sn = Closed⋆-sn c[r]^sn (cut^↝⋆ c ([/0]^↝⋆ l red)) in
sn (c[fire]⁻¹^Closed-sn (ι₁ _ l r) (t^sn red , l^sn , r^sn) c^sn c[r′]^sn)
c[fire⁻¹]^Closed-sn c (ι₁ t l r) (t^sn , sn l^sn , r^sn) c^sn c[r]^sn ([c]₂ _ red _) =
let c[r′]^sn = Closed-sn c[r]^sn (cut^↝ c ([/0]^↝ red t)) in
sn (c[fire]⁻¹^Closed-sn (ι₁ t _ r) (t^sn , l^sn red , r^sn) c^sn c[r′]^sn)
c[fire⁻¹]^Closed-sn c (ι₁ t l r) (t^sn , l^sn , sn r^sn) c^sn c[r]^sn ([c]₃ _ _ red) =
sn (c[fire]⁻¹^Closed-sn (ι₁ t l _) (t^sn , l^sn , r^sn red) c^sn c[r]^sn)
c[fire⁻¹]^Closed-sn c (ι₂ t l r) (sn t^sn , l^sn , r^sn) c^sn c[r]^sn ([c]₁ ([i₂] red) _ _) =
let c[r′]^sn = Closed⋆-sn c[r]^sn (cut^↝⋆ c ([/0]^↝⋆ r red)) in
sn (c[fire]⁻¹^Closed-sn (ι₂ _ l r) (t^sn red , l^sn , r^sn) c^sn c[r′]^sn)
c[fire⁻¹]^Closed-sn c (ι₂ t l r) (t^sn , sn l^sn , r^sn) c^sn c[r]^sn ([c]₂ _ red _) =
sn (c[fire]⁻¹^Closed-sn (ι₂ t _ r) (t^sn , l^sn red , r^sn) c^sn c[r]^sn)
c[fire⁻¹]^Closed-sn c (ι₂ t l r) (t^sn , l^sn , sn r^sn) c^sn c[r]^sn ([c]₃ _ _ red) =
let c[r′]^sn = Closed-sn c[r]^sn (cut^↝ c ([/0]^↝ red t)) in
sn (c[fire]⁻¹^Closed-sn (ι₂ t l _) (t^sn , l^sn , r^sn red) c^sn c[r′]^sn)
c[fire⁻¹]^Closed-sn c (ιz ze su) (sn ze^sn , su^sn) c^sn c[r]^sn ([r]₁ red _ _) =
let c[r′]^sn = Closed-sn c[r]^sn (cut^↝ c red) in
sn (c[fire]⁻¹^Closed-sn (ιz _ su) (ze^sn red , su^sn) c^sn c[r′]^sn)
c[fire⁻¹]^Closed-sn c (ιz ze su) (ze^sn , sn su^sn) c^sn c[r]^sn ([r]₂ _ red _) =
sn (c[fire]⁻¹^Closed-sn (ιz ze _) (ze^sn , su^sn red) c^sn c[r]^sn)
c[fire⁻¹]^Closed-sn c (ιz ze su) _ c^sn c[r]^sn ([r]₃ _ _ ())
c[fire⁻¹]^Closed-sn c (ιs ze su t) (sn ze^sn , su^sn , t^sn) c^sn c[r]^sn ([r]₁ red _ _) =
let reds = sub^↝⋆ su ([v↦t↝⋆t] ∙ᴿ S.ε ∙ᴿ S.return ([r]₁ red _ _)) in
let c[r′]^sn = Closed⋆-sn c[r]^sn (cut^↝⋆ c reds) in
sn (c[fire]⁻¹^Closed-sn (ιs _ su t) (ze^sn red , su^sn , t^sn) c^sn c[r′]^sn)
c[fire⁻¹]^Closed-sn c (ιs ze su t) (ze^sn , sn su^sn , t^sn) c^sn c[r]^sn ([r]₂ _ red _) =
let reds = S.return (sub^↝ (base vl^Tm ∙ t ∙ `rec ze su t) red)
S.◅◅ sub^↝⋆ (tgt red) ([v↦t↝⋆t] ∙ᴿ S.ε ∙ᴿ S.return ([r]₂ _ red _)) in
let c[r′]^sn = Closed⋆-sn c[r]^sn (cut^↝⋆ c reds) in
sn (c[fire]⁻¹^Closed-sn (ιs ze _ t) (ze^sn , su^sn red , t^sn) c^sn c[r′]^sn)
c[fire⁻¹]^Closed-sn c (ιs ze su t) (ze^sn , su^sn , sn t^sn) c^sn c[r]^sn ([r]₃ _ _ ([1+] red)) =
let reds = sub^↝⋆ su ([v↦t↝⋆t] ∙ᴿ S.return red ∙ᴿ S.return ([r]₃ _ _ red)) in
let c[r′]^sn = Closed⋆-sn c[r]^sn (cut^↝⋆ c reds) in
sn (c[fire]⁻¹^Closed-sn (ιs ze su _) (ze^sn , su^sn , t^sn red) c^sn c[r′]^sn)
c[fire⁻¹]^sn : ∀ {Γ α σ c} r → Γ ⊢↯sn α ∋ r → Γ ∣ α ⊢sn σ ∋ c →
Γ ⊢sn σ ∋ cut (βιRed r) c → Γ ⊢sn σ ∋ cut (unRed r) c
c[fire⁻¹]^sn r r^sn c^sn c[r]^sn = sn (c[fire]⁻¹^Closed-sn r r^sn c^sn c[r]^sn)
infix 4 _⊢[_]_∋_↝_<_
data _⊢[_]_∋_↝_<_ Γ (R : ∀ Γ σ → Term σ Γ → Size → Set) τ : (t u : Term τ Γ) → Size → Set where
β : ∀ {σ i} t u → R Γ σ u i → Γ ⊢[ R ] τ ∋ `λ t `∙ u ↝ t [ u /0] < ↑ i
ι₁ : ∀ {σ₁ σ₂ i} t l r → R Γ σ₁ t i → R (σ₂ ∷ Γ) τ r i →
Γ ⊢[ R ] τ ∋ `case (`i₁ t) l r ↝ l [ t /0] < ↑ i
ι₂ : ∀ {σ₁ σ₂ i} t l r → R Γ σ₂ t i → R (σ₁ ∷ Γ) τ l i →
Γ ⊢[ R ] τ ∋ `case (`i₂ t) l r ↝ r [ t /0] < ↑ i
ιz : ∀ {i} ze su → R (τ ∷ ℕ ∷ Γ) τ su i → Γ ⊢[ R ] τ ∋ `rec ze su `0 ↝ ze < ↑ i
ιs : ∀ {i} ze su t → R Γ τ ze i → R Γ ℕ t i →
Γ ⊢[ R ] τ ∋ `rec ze su (`1+ t) ↝ sub (base vl^Tm ∙ t ∙ `rec ze su t) su < ↑ i
[∙]₂ : ∀ {σ i f g} → Γ ⊢[ R ] σ ⇒ τ ∋ f ↝ g < i → ∀ t → Γ ⊢[ R ] τ ∋ f `∙ t ↝ g `∙ t < ↑ i
[c]₁ : ∀ {σ₁ σ₂ i t u} → Γ ⊢[ R ] σ₁ + σ₂ ∋ t ↝ u < i → ∀ l r →
Γ ⊢[ R ] τ ∋ `case t l r ↝ `case u l r < ↑ i
[r]₃ : ∀ {i t u} ze su → Γ ⊢[ R ] ℕ ∋ t ↝ u < i →
Γ ⊢[ R ] τ ∋ `rec ze su t ↝ `rec ze su u < ↑ i
infix 4 _⊢_∋_↝SN_<_ _⊢SN_∋_<_ _⊢SNe_∋_<_ _⊢_∋_↝SN_ _⊢SN_∋_ _⊢SNe_∋_
_⊢_∋_↝SN_<_ : ∀ Γ τ (t u : Term τ Γ) → Size → Set
data _⊢SN_∋_<_ (Γ : List Type) : (σ : Type) → Term σ Γ → Size → Set
data _⊢SNe_∋_<_ (Γ : List Type) : (σ : Type) → Term σ Γ → Size → Set
_⊢_∋_↝SN_<_ = _⊢[ _⊢SN_∋_<_ ]_∋_↝_<_
data _⊢SN_∋_<_ Γ where
neu : ∀ {σ t i} → Γ ⊢SNe σ ∋ t < i → Γ ⊢SN σ ∋ t < ↑ i
lam : ∀ {σ τ b i} → (σ ∷ Γ) ⊢SN τ ∋ b < i → Γ ⊢SN σ ⇒ τ ∋ `λ b < ↑ i
inl : ∀ {σ τ t i} → Γ ⊢SN σ ∋ t < i → Γ ⊢SN σ + τ ∋ `i₁ t < ↑ i
inr : ∀ {σ τ t i} → Γ ⊢SN τ ∋ t < i → Γ ⊢SN σ + τ ∋ `i₂ t < ↑ i
zro : ∀ {i} → Γ ⊢SN ℕ ∋ `0 < ↑ i
suc : ∀ {i t} → Γ ⊢SN ℕ ∋ t < i → Γ ⊢SN ℕ ∋ `1+ t < ↑ i
red : ∀ {σ t t′ i} → Γ ⊢ σ ∋ t ↝SN t′ < i → Γ ⊢SN σ ∋ t′ < i → Γ ⊢SN σ ∋ t < ↑ i
data _⊢SNe_∋_<_ Γ where
var : ∀ {σ i} v → Γ ⊢SNe σ ∋ `var v < ↑ i
app : ∀ {σ τ f t i} → Γ ⊢SNe σ ⇒ τ ∋ f < i → Γ ⊢SN σ ∋ t < i → Γ ⊢SNe τ ∋ f `∙ t < ↑ i
cas : ∀ {σ τ ν t l r i} → Γ ⊢SNe σ + τ ∋ t < i →
(σ ∷ Γ) ⊢SN ν ∋ l < i → (τ ∷ Γ) ⊢SN ν ∋ r < i → Γ ⊢SNe ν ∋ `case t l r < ↑ i
rec : ∀ {σ i ze su t} → Γ ⊢SN σ ∋ ze < i → (σ ∷ ℕ ∷ Γ) ⊢SN σ ∋ su < i →
Γ ⊢SNe ℕ ∋ t < i → Γ ⊢SNe σ ∋ `rec ze su t < ↑ i
_⊢_∋_↝SN_ = _⊢_∋_↝SN_< _
_⊢SN_∋_ = _⊢SN_∋_< _
_⊢SNe_∋_ = _⊢SNe_∋_< _
SN∋ : Pred Term
pred SN∋ = _ ⊢SN_∋_
SNe : Pred Term
pred SNe = _ ⊢SNe_∋_
[v↦v]^SNe : P.All SNe Γ (base vl^Tm)
lookupᴾ [v↦v]^SNe v rewrite lookup-base^Tm {d = TermD} v = var v
infix 4 _∣_⊢SN_∋_<_ _∣_⊢SN_∋_
_∣_⊢SN_∋_<_ = _∣_⊢[ _⊢SN_∋_<_ ]_∋_<_
_∣_⊢SN_∋_ = _∣_⊢SN_∋_< _
cut⁻¹^SNe : ∀ {Γ τ t i} → Γ ⊢SNe τ ∋ t < i →
Σ[ ctx ∈ (∃ λ σ → Γ ∣ σ ⊢ τ) ] let (σ , c) = ctx in
∃ λ v → t ≡ cut (`var v) c × Γ ∣ σ ⊢SN τ ∋ c < i
cut⁻¹^SNe (var v) = _ , v , refl , <>
cut⁻¹^SNe (app f^SNe t^SN) =
let (_ , v , eq , c^SN) = cut⁻¹^SNe f^SNe
in _ , v , cong (_`∙ _) eq , app c^SN t^SN
cut⁻¹^SNe (cas t^SNe l^SN r^SN) =
let (_ , v , eq , c^SN) = cut⁻¹^SNe t^SNe
in _ , v , cong (λ t → `case t _ _) eq , cas c^SN l^SN r^SN
cut⁻¹^SNe (rec ze^SN su^SN t^SNe) =
let (_ , v , eq , c^SN) = cut⁻¹^SNe t^SNe
in _ , v , cong (`rec _ _) eq , rec ze^SN su^SN c^SN
mutual
th^SN : ∀ {σ Γ Δ t} ρ → Γ ⊢SN σ ∋ t → Δ ⊢SN σ ∋ ren ρ t
th^SN ρ (neu n) = neu (th^SNe ρ n)
th^SN ρ (lam t) = lam (th^SN _ t)
th^SN ρ (inl t) = inl (th^SN ρ t)
th^SN ρ (inr t) = inr (th^SN ρ t)
th^SN ρ zro = zro
th^SN ρ (suc t) = suc (th^SN ρ t)
th^SN ρ (red r t) = red (th^↝SN ρ r) (th^SN ρ t)
th^SNe : ∀ {σ Γ Δ t} ρ → Γ ⊢SNe σ ∋ t → Δ ⊢SNe σ ∋ ren ρ t
th^SNe ρ (var v) = var (lookup ρ v)
th^SNe ρ (app n t) = app (th^SNe ρ n) (th^SN ρ t)
th^SNe ρ (cas n l r) = cas (th^SNe ρ n) (th^SN _ l) (th^SN _ r)
th^SNe ρ (rec ze su t) = rec (th^SN ρ ze) (th^SN _ su) (th^SNe ρ t)
th^↝SN : ∀ {σ Γ Δ t u} ρ → Γ ⊢ σ ∋ t ↝SN u → Δ ⊢ σ ∋ ren ρ t ↝SN ren ρ u
th^↝SN ρ (β t u u^SN) =
subst (_ ⊢ _ ∋ ren ρ (`λ t `∙ u) ↝SN_< _) (renβ TermD t (ε ∙ u) ρ) (β _ (ren ρ u) (th^SN ρ u^SN))
th^↝SN ρ (ι₁ t l r t^SN r^SN) =
subst (_ ⊢ _ ∋ ren ρ (`case (`i₁ t) l r) ↝SN_< _) (renβ TermD l (ε ∙ t) ρ)
$ ι₁ _ _ (ren _ r) (th^SN ρ t^SN) (th^SN _ r^SN)
th^↝SN ρ (ι₂ t l r t^SN l^SN) =
subst (_ ⊢ _ ∋ ren ρ (`case (`i₂ t) l r) ↝SN_< _) (renβ TermD r (ε ∙ t) ρ)
$ ι₂ _ (ren _ l) _ (th^SN ρ t^SN) (th^SN _ l^SN)
th^↝SN ρ (ιz ze su su^SN) = ιz (ren ρ ze) (ren _ su) (th^SN _ su^SN)
th^↝SN ρ (ιs ze su t ze^SN t^SN) =
subst (_ ⊢ _ ∋ ren ρ (`rec ze su (`1+ t)) ↝SN_< _) (renβ TermD su (ε ∙ t ∙ `rec ze su t) ρ)
$ ιs (ren ρ ze) (ren _ su) (ren ρ t) (th^SN ρ ze^SN) (th^SN ρ t^SN)
th^↝SN ρ ([∙]₂ r t) = [∙]₂ (th^↝SN ρ r) (ren ρ t)
th^↝SN ρ ([c]₁ r bl br) = [c]₁ (th^↝SN ρ r) (ren _ bl) (ren _ br)
th^↝SN ρ ([r]₃ ze su r) = [r]₃ (ren ρ ze) (ren _ su) (th^↝SN ρ r)
freshˡ^SNe : P.All SNe Γ (freshˡ vl^Tm Δ)
lookupᴾ freshˡ^SNe k = th^SNe (pack (injectˡ _)) (cast (var k))
where cast = subst (_ ⊢SNe _ ∋_) (sym (lookup-base^Tm k))
mutual
th⁻¹^SN : ∀ {σ Γ Δ t′} t ρ → t′ ≡ ren ρ t → Δ ⊢SN σ ∋ t′ → Γ ⊢SN σ ∋ t
th⁻¹^SN t ρ eq (neu pr) = neu (th⁻¹^SNe t ρ eq pr)
th⁻¹^SN (`λ t) ρ refl (lam pr) = lam (th⁻¹^SN t _ refl pr)
th⁻¹^SN (`i₁ t) ρ refl (inl pr) = inl (th⁻¹^SN t ρ refl pr)
th⁻¹^SN (`i₂ t) ρ refl (inr pr) = inr (th⁻¹^SN t ρ refl pr)
th⁻¹^SN `0 ρ refl zro = zro
th⁻¹^SN (`1+ t) ρ refl (suc pr) = suc (th⁻¹^SN t ρ refl pr)
th⁻¹^SN t ρ refl (red r pr) =
let (t′ , eq , r′) = th⁻¹^↝SN t ρ r in red r′ (th⁻¹^SN t′ ρ eq pr)
th⁻¹^SNe : ∀ {σ Γ Δ t′} t ρ → t′ ≡ ren ρ t → Δ ⊢SNe σ ∋ t′ → Γ ⊢SNe σ ∋ t
th⁻¹^SNe (`var v) ρ refl (var _) = var v
th⁻¹^SNe (f `∙ t) ρ refl (app rf rt) =
app (th⁻¹^SNe f ρ refl rf) (th⁻¹^SN t ρ refl rt)
th⁻¹^SNe (`case t l r) ρ refl (cas rt rl rr) =
cas (th⁻¹^SNe t ρ refl rt) (th⁻¹^SN l _ refl rl) (th⁻¹^SN r _ refl rr)
th⁻¹^SNe (`rec ze su t) ρ refl (rec rze rsu rt) =
rec (th⁻¹^SN ze ρ refl rze) (th⁻¹^SN su _ refl rsu) (th⁻¹^SNe t ρ refl rt)
th⁻¹^↝SN : ∀ {σ Γ Δ u} t ρ → Δ ⊢ σ ∋ ren ρ t ↝SN u → ∃ λ u′ → u ≡ ren ρ u′ × Γ ⊢ σ ∋ t ↝SN u′
th⁻¹^↝SN (`λ b `∙ t) ρ (β ._ ._ t^SN) =
b [ t /0] , renβ TermD b (ε ∙ t) ρ , β b t (th⁻¹^SN t ρ refl t^SN)
th⁻¹^↝SN (`case (`i₁ t) l r) ρ (ι₁ ._ ._ ._ t^SN r^SN) =
l [ t /0] , renβ TermD l (ε ∙ t) ρ , ι₁ t l r (th⁻¹^SN t ρ refl t^SN) (th⁻¹^SN r _ refl r^SN)
th⁻¹^↝SN (`case (`i₂ t) l r) ρ (ι₂ ._ ._ ._ t^SN l^SN) =
r [ t /0] , renβ TermD r (ε ∙ t) ρ , ι₂ t l r (th⁻¹^SN t ρ refl t^SN) (th⁻¹^SN l _ refl l^SN)
th⁻¹^↝SN (`rec ze su `0) ρ (ιz _ _ su^SN) = ze , refl , ιz ze su (th⁻¹^SN su _ refl su^SN)
th⁻¹^↝SN (`rec ze su (`1+ t)) ρ (ιs _ _ _ ze^SN t^SN) =
sub (base vl^Tm ∙ t ∙ `rec ze su t) su , renβ TermD su (ε ∙ t ∙ `rec ze su t) ρ
, ιs ze su t (th⁻¹^SN ze ρ refl ze^SN) (th⁻¹^SN t ρ refl t^SN)
th⁻¹^↝SN (f `∙ t) ρ ([∙]₂ r ._) =
let (g , eq , r′) = th⁻¹^↝SN f ρ r in g `∙ t , cong (_`∙ ren ρ t) eq , [∙]₂ r′ t
th⁻¹^↝SN (`case c bl br) ρ ([c]₁ r ._ ._) = let (d , eq , r′) = th⁻¹^↝SN c ρ r in
`case d bl br , cong (λ c → `case c (ren _ bl) (ren _ br)) eq , [c]₁ r′ bl br
th⁻¹^↝SN (`rec ze su t) ρ ([r]₃ ._ ._ r) = let (t′ , eq , r′) = th⁻¹^↝SN t ρ r in
`rec ze su t′ , cong (`rec (ren ρ ze) (ren _ su)) eq , [r]₃ ze su r′
_SNe∙_ : ∀ {Γ σ τ f t} → Γ ⊢SNe σ ⇒ τ ∋ f → Γ ⊢SN σ ∋ t → Γ ⊢SN τ ∋ f `∙ t
f^SNe SNe∙ t^SN = neu (app f^SNe t^SN)
SNe-ext : ∀ {Γ σ τ f} v → Γ ⊢SNe τ ∋ f `∙ `var v → Γ ⊢SNe σ ⇒ τ ∋ f
SNe-ext v (app f^SNe v^SN) = f^SNe
SN-ext : ∀ {Γ σ τ f} v → Γ ⊢SN τ ∋ f `∙ `var v → Γ ⊢SN σ ⇒ τ ∋ f
SN-ext v (neu fv^SNe) = neu (SNe-ext v fv^SNe)
SN-ext v (red ([∙]₂ r _) fv^SN) = red r (SN-ext v fv^SN)
SN-ext v (red (β t _ v^SN) fv^SN) = lam (th⁻¹^SN t (base vl^Var ∙ v) eq fv^SN) where
eq = sym $ Simulation.sim Sim.RenSub (base^VarTmᴿ ∙ᴿ refl) t
infix 4 _⊢_∋_↝sn_<_ _⊢_∋_↝sn_
_⊢_∋_↝sn_<_ = _⊢[ _⊢sn_∋_<_ ]_∋_↝_<_
_⊢_∋_↝sn_ = _⊢_∋_↝sn_< _
↝sn⁻¹^sn : ∀ {Γ σ τ t′ t i} c → Γ ⊢ σ ∋ t′ ↝sn t < i →
Γ ⊢sn τ ∋ cut t c → Γ ⊢sn τ ∋ cut t′ c
↝sn⁻¹^sn c (β b u u^sn) c[b[u]]^sn =
let (c^sn , b[u]^sn) = cut⁻¹^sn (b [ u /0]) c c[b[u]]^sn in
let b^sn = [/0]⁻¹^sn b u b[u]^sn in
c[fire⁻¹]^sn (β b u) (b^sn , u^sn) c^sn c[b[u]]^sn
↝sn⁻¹^sn c (ι₁ t l r t^sn r^sn) c[l[t]]^sn =
let (c^sn , l[t]^sn) = cut⁻¹^sn (l [ t /0]) c c[l[t]]^sn in
let l^sn = [/0]⁻¹^sn l t l[t]^sn in
c[fire⁻¹]^sn (ι₁ t l r) (t^sn , l^sn , r^sn) c^sn c[l[t]]^sn
↝sn⁻¹^sn c (ι₂ t l r t^sn l^sn) c[r[t]]^sn =
let (c^sn , r[t]^sn) = cut⁻¹^sn (r [ t /0]) c c[r[t]]^sn in
let r^sn = [/0]⁻¹^sn r t r[t]^sn in
c[fire⁻¹]^sn (ι₂ t l r) (t^sn , l^sn , r^sn) c^sn c[r[t]]^sn
↝sn⁻¹^sn c (ιz ze su su^sn) c[ze]^sn =
let (c^sn , ze^sn) = cut⁻¹^sn ze c c[ze]^sn in
c[fire⁻¹]^sn (ιz ze su) (ze^sn , su^sn) c^sn c[ze]^sn
↝sn⁻¹^sn c (ιs ze su t ze^sn t^sn) c[s[zst]]^sn =
let (c^sn , s[zst]^sn) = cut⁻¹^sn _ c c[s[zst]]^sn in
let su^sn = sub⁻¹^sn su (base vl^Tm ∙ t ∙ `rec ze su t) s[zst]^sn in
c[fire⁻¹]^sn (ιs ze su t) (ze^sn , su^sn , t^sn) c^sn c[s[zst]]^sn
↝sn⁻¹^sn c ([∙]₂ r^sn u) c[ft]^sn =
let eq t = cut-∘C t c (app <> u) in
let ft^sn′ = subst (_ ⊢sn _ ∋_) (eq _) c[ft]^sn in
let ih = ↝sn⁻¹^sn (c ∘C app <> u) r^sn ft^sn′ in
subst (_ ⊢sn _ ∋_) (sym (eq _)) ih
↝sn⁻¹^sn c ([c]₁ r^sn l r) c[slr]^sn =
let eq t = cut-∘C t c (cas <> l r) in
let slr^sn′ = subst (_ ⊢sn _ ∋_) (eq _) c[slr]^sn in
let ih = ↝sn⁻¹^sn (c ∘C cas <> l r) r^sn slr^sn′ in
subst (_ ⊢sn _ ∋_) (sym (eq _)) ih
↝sn⁻¹^sn c ([r]₃ ze su r^sn) c[zst]^sn =
let eq t = cut-∘C t c (rec ze su <>) in
let zst^sn′ = subst (_ ⊢sn _ ∋_) (eq _) c[zst]^sn in
let ih = ↝sn⁻¹^sn (c ∘C rec ze su <>) r^sn zst^sn′ in
subst (_ ⊢sn _ ∋_) (sym (eq _)) ih
mutual
sound^SN : ∀ {Γ σ t i} → Γ ⊢SN σ ∋ t < i → Γ ⊢sn σ ∋ t
sound^SN (neu t^SNe) = let (_ , v , eq , c^SN) = cut⁻¹^SNe t^SNe in
subst (_ ⊢sn _ ∋_) (sym eq) (cut^sn _ (sound^∣SN c^SN))
sound^SN (lam b^SN) = `λ^sn (sound^SN b^SN)
sound^SN (inl t^SN) = `i₁^sn (sound^SN t^SN)
sound^SN (inr t^SN) = `i₂^sn (sound^SN t^SN)
sound^SN zro = `0^sn
sound^SN (suc t^SN) = `1+^sn (sound^SN t^SN)
sound^SN (red r t^SN) = ↝sn⁻¹^sn <> (sound^↝SN r) (sound^SN t^SN)
sound^∣SN : ∀ {Γ α σ c i} → Γ ∣ α ⊢SN σ ∋ c < i → Γ ∣ α ⊢sn σ ∋ c
sound^∣SN <> = <>
sound^∣SN (app c^SN t^SN) = app (sound^∣SN c^SN) (sound^SN t^SN)
sound^∣SN (cas c^SN l^SN r^SN) = cas (sound^∣SN c^SN) (sound^SN l^SN) (sound^SN r^SN)
sound^∣SN (rec ze^SN su^SN t^SN) = rec (sound^SN ze^SN) (sound^SN su^SN) (sound^∣SN t^SN)
sound^↝SN : ∀ {Γ σ t u i} → Γ ⊢ σ ∋ t ↝SN u < i → Γ ⊢ σ ∋ t ↝sn u
sound^↝SN (β t u u^SN) = β t u (sound^SN u^SN)
sound^↝SN (ι₁ t l r t^SN r^SN) = ι₁ t l r (sound^SN t^SN) (sound^SN r^SN)
sound^↝SN (ι₂ t l r t^SN l^SN) = ι₂ t l r (sound^SN t^SN) (sound^SN l^SN)
sound^↝SN (ιz ze su su^SN) = ιz ze su (sound^SN su^SN)
sound^↝SN (ιs ze su t ze^SN t^SN) = ιs ze su t (sound^SN ze^SN) (sound^SN t^SN)
sound^↝SN ([∙]₂ r t) = [∙]₂ (sound^↝SN r) t
sound^↝SN ([c]₁ r _ _) = [c]₁ (sound^↝SN r) _ _
sound^↝SN ([r]₃ _ _ r) = [r]₃ _ _ (sound^↝SN r)
data Elim (Γ : List Type) (τ : Type) : Type → Set where
app : ∀ {σ} → Term σ Γ → Elim Γ τ (σ ⇒ τ)
cas : ∀ {σ₁ σ₂} → Term τ (σ₁ ∷ Γ) → Term τ (σ₂ ∷ Γ) → Elim Γ τ (σ₁ + σ₂)
rec : Term τ Γ → Term τ (τ ∷ ℕ ∷ Γ) → Elim Γ τ ℕ
elim : ∀ {Γ σ τ} → Elim Γ τ σ → Γ ∣ σ ⊢ τ
elim (app t) = app <> t
elim (cas l r) = cas <> l r
elim (rec ze su) = rec ze su <>
mutual
complete^SNe : ∀ {Γ σ α i c} v → Γ ∣ α ⊢SN σ ∋ c →
let t = cut (`var v) c in ∀ {t′} → t′ ≡ t → Γ ⊢sn σ ∋ t′ < i → Γ ⊢SNe σ ∋ t′
complete^SNe v <> refl c[v]^sn = var v
complete^SNe v (app c t^SN) refl c[v]∙t^sn =
app (complete^SNe v c refl (`∙t⁻¹^sn c[v]∙t^sn)) t^SN
complete^SNe v (cas c l^SN r^SN) refl c[v]lr^sn =
cas (complete^SNe v c refl (`case₁⁻¹^sn c[v]lr^sn)) l^SN r^SN
complete^SNe v (rec ze^SN su^SN c) refl czs[v]^sn =
rec ze^SN su^SN (complete^SNe v c refl (`rec₃⁻¹^sn czs[v]^sn))
complete^SN-βι : ∀ {Γ α σ i} (r : Γ ⊢↯ α) c →
let t = cut (unRed r) c in Γ ⊢ σ ∋ t ↝SN cut (βιRed r) c →
∀ {t′} → t′ ≡ t → Γ ⊢sn σ ∋ t′ < i → Γ ⊢SN σ ∋ t′
complete^SN-βι t c r refl (sn p) = red r (complete^SN _ (p (cut^↝ c (fire t))))
complete^SN : ∀ {Γ σ i} t → Γ ⊢sn σ ∋ t < i → Γ ⊢SN σ ∋ t
complete^SN (`var v) v^sn = neu (var v)
complete^SN (`i₁ t) it^sn = inl (complete^SN t (`i₁⁻¹^sn it^sn))
complete^SN (`i₂ t) it^sn = inr (complete^SN t (`i₂⁻¹^sn it^sn))
complete^SN `0 ze^sn = zro
complete^SN (`1+ t) st^sn = suc (complete^SN t (`1+⁻¹^sn st^sn))
complete^SN (`λ b) λb^sn = lam (complete^SN b (`λ⁻¹^sn λb^sn))
complete^SN (f `∙ t) ft^sn =
let (f^sn , t^sn) = `∙⁻¹^sn ft^sn in
let t^SN = complete^SN t t^sn in
elim^SN f (app t) f^sn (app <> t^SN) ft^sn
complete^SN (`case t l r) tlr^sn =
let (t^sn , l^sn , r^sn) = `case⁻¹^sn tlr^sn in
let (l^SN , r^SN) = (complete^SN l l^sn , complete^SN r r^sn) in
elim^SN t (cas l r) t^sn (cas <> l^SN r^SN) tlr^sn
complete^SN (`rec ze su t) zst^sn =
let (ze^sn , su^sn , t^sn) = `rec⁻¹^sn zst^sn in
let (ze^SN , su^SN) = (complete^SN ze ze^sn , complete^SN su su^sn) in
elim^SN t (rec ze su) t^sn (rec ze^SN su^SN <>) zst^sn
elim^SN : ∀ {Γ σ τ i} t e → Γ ⊢sn σ ∋ t < i → Γ ∣ σ ⊢SN τ ∋ elim e →
Γ ⊢sn τ ∋ cut t (elim e) < i → Γ ⊢SN τ ∋ cut t (elim e)
elim^SN t e t^sn e^SN e[t]^sn =
case spine^SN t e t^sn e^SN of λ where
(_ , c , inj₁ (v , eq , c^SN)) → neu (complete^SNe v c^SN eq e[t]^sn)
(_ , c , inj₂ (r , eq , r^SN)) → complete^SN-βι r c r^SN eq e[t]^sn
spine^SN : ∀ {Γ σ τ i} t e → Γ ⊢sn σ ∋ t < i → Γ ∣ σ ⊢SN τ ∋ elim e →
∃ λ α → ∃ λ (c : Γ ∣ α ⊢ τ) →
(∃ λ v → cut t (elim e) ≡ cut (`var v) c × Γ ∣ α ⊢SN τ ∋ c)
⊎ (∃ λ r → cut t (elim e) ≡ cut (unRed r) c
× Γ ⊢ τ ∋ cut (unRed r) c ↝SN cut (βιRed r) c)
spine^SN (`var v) e tm^sn e^SN = _ , elim e , inj₁ (v , refl , e^SN)
spine^SN (`λ b) (app t) tm^sn (app <> t^SN) = _ , <> , inj₂ (β b t , refl , β b t t^SN)
spine^SN (`i₁ t) (cas l r) tm^sn (cas <> l^SN r^SN) =
let t^SN = complete^SN t (`i₁⁻¹^sn tm^sn) in
_ , <> , inj₂ (ι₁ t l r , refl , ι₁ t l r t^SN r^SN)
spine^SN (`i₂ t) (cas l r) tm^sn (cas <> l^SN r^SN) =
let t^SN = complete^SN t (`i₂⁻¹^sn tm^sn) in
_ , <> , inj₂ (ι₂ t l r , refl , ι₂ t l r t^SN l^SN)
spine^SN `0 (rec ze su) tm^sn (rec ze^SN su^SN <>) =
_ , <> , inj₂ (ιz ze su , refl , ιz ze su su^SN)
spine^SN (`1+ t) (rec ze su) tm^sn (rec ze^SN su^SN <>) =
let t^SN = complete^SN t (`1+⁻¹^sn tm^sn) in
_ , <> , inj₂ (ιs ze su t , refl , ιs ze su t ze^SN t^SN)
spine^SN (f `∙ t) e tm^sn e^SN =
let (f^sn , t^sn) = `∙⁻¹^sn tm^sn in
let t^SN = complete^SN t t^sn in
case spine^SN f (app t) f^sn (app <> t^SN) of λ where
(_ , c , inj₁ (v , eq , c^SN)) →
_ , (elim e ∘C c) , inj₁ (v , spine-eq e c eq , ∘Cᴿ e^SN c^SN)
(_ , c , inj₂ (r , eq , r^SN)) →
_ , (elim e ∘C c) , inj₂ (r , spine-eq e c eq , spine-red e c r r^SN)
spine^SN (`case t l r) e tm^sn e^SN =
let (t^sn , l^sn , r^sn) = `case⁻¹^sn tm^sn in
let (l^SN , r^SN) = (complete^SN l l^sn , complete^SN r r^sn) in
case spine^SN t (cas l r) t^sn (cas <> l^SN r^SN) of λ where
(_ , c , inj₁ (v , eq , c^SN)) →
_ , (elim e ∘C c) , inj₁ (v , spine-eq e c eq , ∘Cᴿ e^SN c^SN)
(_ , c , inj₂ (r , eq , r^SN)) →
_ , (elim e ∘C c) , inj₂ (r , spine-eq e c eq , spine-red e c r r^SN)
spine^SN (`rec ze su t) e tm^sn e^SN =
let (ze^sn , su^sn , t^sn) = `rec⁻¹^sn tm^sn in
let (ze^SN , su^SN) = (complete^SN ze ze^sn , complete^SN su su^sn) in
case spine^SN t (rec ze su) t^sn (rec ze^SN su^SN <>) of λ where
(_ , c , inj₁ (v , eq , c^SN)) →
_ , (elim e ∘C c) , inj₁ (v , spine-eq e c eq , ∘Cᴿ e^SN c^SN)
(_ , c , inj₂ (r , eq , r^SN)) →
_ , (elim e ∘C c) , inj₂ (r , spine-eq e c eq , spine-red e c r r^SN)
spine-eq : ∀ {Γ α β σ t tc} (e : Elim Γ σ β) (c : Γ ∣ α ⊢ β) →
tc ≡ cut t c → cut tc (elim e) ≡ cut t (elim e ∘C c)
spine-eq e c refl = cut-∘C _ (elim e) c
spine-red : ∀ {Γ α β σ} e c → (r : Γ ⊢↯ α) →
Γ ⊢ β ∋ cut (unRed r) c ↝SN cut (βιRed r) c →
Γ ⊢ σ ∋ cut (unRed r) (elim e ∘C c) ↝SN cut (βιRed r) (elim e ∘C c)
spine-red (app t) c r r^SN = [∙]₂ r^SN t
spine-red (cas _ _) c r r^SN = [c]₁ r^SN _ _
spine-red (rec _ _) c r r^SN = [r]₃ _ _ r^SN
infix 2 <_>
data <_> {Γ σ} (𝓢 : Term σ Γ → Set) (t : Term σ Γ) : Set where
cnd : 𝓢 t → < 𝓢 > t
neu : Γ ⊢SNe σ ∋ t → < 𝓢 > t
red : ∀ {t′} → Γ ⊢ σ ∋ t ↝SN t′ → < 𝓢 > t′ → < 𝓢 > t
infix 3 _+𝓡_
data _+𝓡_ {Γ σ τ} (𝓢 : Term σ Γ → Set) (𝓣 : Term τ Γ → Set) : Term (σ + τ) Γ → Set where
inl : ∀ {t} → 𝓢 t → (𝓢 +𝓡 𝓣) (`i₁ t)
inr : ∀ {t} → 𝓣 t → (𝓢 +𝓡 𝓣) (`i₂ t)
data ℕ𝓡 {Γ} : Size → Term ℕ Γ → Set where
zro : ∀ {i} → ℕ𝓡 (↑ i) `0
suc : ∀ {i t} → < ℕ𝓡 i > t → ℕ𝓡 (↑ i) (`1+ t)
infix 3 _⊢𝓡_∋_
_⊢𝓡_∋_ : ∀ Γ σ → Term σ Γ → Set
Γ ⊢𝓡 α ∋ t = Γ ⊢SN α ∋ t
Γ ⊢𝓡 ℕ ∋ t = < ℕ𝓡 _ > t
Γ ⊢𝓡 σ + τ ∋ t = < (Γ ⊢𝓡 σ ∋_) +𝓡 (Γ ⊢𝓡 τ ∋_) > t
Γ ⊢𝓡 σ ⇒ τ ∋ t = ∀ {Δ} ρ {u} → Δ ⊢𝓡 σ ∋ u → Δ ⊢𝓡 τ ∋ ren ρ t `∙ u
𝓡ᴾ : Pred Term
pred 𝓡ᴾ = _ ⊢𝓡_∋_
Quote : List Type → Type → Set
Quote Γ σ = ∀ {t} → Γ ⊢𝓡 σ ∋ t → Γ ⊢SN σ ∋ t
quote^<> : ∀ {Γ σ 𝓢} → (∀ {t} → 𝓢 t → Γ ⊢SN σ ∋ t) →
∀ {t} → < 𝓢 > t → Γ ⊢SN σ ∋ t
quote^<> σ^𝓡 (cnd t^𝓡) = σ^𝓡 t^𝓡
quote^<> σ^𝓡 (neu t^SNe) = neu t^SNe
quote^<> σ^𝓡 (red r t^𝓡) = red r (quote^<> σ^𝓡 t^𝓡)
quote^+𝓡 : ∀ {Γ σ τ} → Quote Γ σ → Quote Γ τ →
∀ {t} → ((Γ ⊢𝓡 σ ∋_) +𝓡 (Γ ⊢𝓡 τ ∋_)) t → Γ ⊢SN σ + τ ∋ t
quote^+𝓡 σ^𝓡 τ^𝓡 (inl t^𝓡) = inl (σ^𝓡 t^𝓡)
quote^+𝓡 σ^𝓡 τ^𝓡 (inr t^𝓡) = inr (τ^𝓡 t^𝓡)
quote^ℕ𝓡 : ∀ {Γ t i} → ℕ𝓡 i t → Γ ⊢SN ℕ ∋ t
quote^ℕ𝓡 zro = zro
quote^ℕ𝓡 (suc t^𝓡) = suc (quote^<> quote^ℕ𝓡 t^𝓡)
mutual
quote^𝓡 : ∀ {Γ} σ → Quote Γ σ
quote^𝓡 α t^𝓡 = t^𝓡
quote^𝓡 ℕ t^𝓡 = quote^<> quote^ℕ𝓡 t^𝓡
quote^𝓡 (σ + τ) t^𝓡 = quote^<> (quote^+𝓡 (quote^𝓡 σ) (quote^𝓡 τ)) t^𝓡
quote^𝓡 (σ ⇒ τ) t^𝓡 = th⁻¹^SN _ embed refl (SN-ext Var.z tz^SN)
where z^𝓡 = unquote^𝓡 σ (var Var.z)
embed = pack Var.s
tz^SN = quote^𝓡 τ (t^𝓡 embed z^𝓡)
unquote^𝓡 : ∀ {Γ} σ {t} → Γ ⊢SNe σ ∋ t → Γ ⊢𝓡 σ ∋ t
unquote^𝓡 α t^SNe = neu t^SNe
unquote^𝓡 ℕ t^SNe = neu t^SNe
unquote^𝓡 (σ + τ) t^SNe = neu t^SNe
unquote^𝓡 (σ ⇒ τ) t^SNe ρ u^𝓡 = unquote^𝓡 τ (app (th^SNe ρ t^SNe) u^SN)
where u^SN = quote^𝓡 σ u^𝓡
↝SN⁻¹^𝓡 : ∀ {Γ} σ {t′ t} → Γ ⊢ σ ∋ t′ ↝SN t → Γ ⊢𝓡 σ ∋ t → Γ ⊢𝓡 σ ∋ t′
↝SN⁻¹^𝓡 α r t^𝓡 = red r t^𝓡
↝SN⁻¹^𝓡 ℕ r t^𝓡 = red r t^𝓡
↝SN⁻¹^𝓡 (σ + τ) r t^𝓡 = red r t^𝓡
↝SN⁻¹^𝓡 (σ ⇒ τ) r t^𝓡 = λ ρ u^𝓡 → ↝SN⁻¹^𝓡 τ ([∙]₂ (th^↝SN ρ r) _) (t^𝓡 ρ u^𝓡)
th^<> : ∀ {σ} {𝓢 : ∀ {Γ} → Term σ Γ → Set}
(th^𝓢 : ∀ {Γ Δ t} (ρ : Thinning Γ Δ) → 𝓢 t → 𝓢 (ren ρ t)) →
∀ {Γ Δ t} (ρ : Thinning Γ Δ) → < 𝓢 > t → < 𝓢 > (ren ρ t)
th^<> th^𝓢 ρ (cnd t^𝓢) = cnd (th^𝓢 ρ t^𝓢)
th^<> th^𝓢 ρ (neu t^SNe) = neu (th^SNe ρ t^SNe)
th^<> th^𝓢 ρ (red r t^𝓢) = red (th^↝SN ρ r) (th^<> th^𝓢 ρ t^𝓢)
th^ℕ𝓡 : ∀ {i Γ Δ t} (ρ : Thinning Γ Δ) → ℕ𝓡 i t → ℕ𝓡 i (ren ρ t)
th^ℕ𝓡 ρ zro = zro
th^ℕ𝓡 ρ (suc {i} t^𝓡) = suc (th^<> (th^ℕ𝓡 {i}) ρ t^𝓡)
th^+𝓡 : ∀ {σ τ} {𝓢 : ∀ {Γ} → Term σ Γ → Set} {𝓣 : ∀ {Γ} → Term τ Γ → Set}
(th^𝓢 : ∀ {Γ Δ} (ρ : Thinning Γ Δ) → ∀ t → 𝓢 t → 𝓢 (ren ρ t)) →
(th^𝓣 : ∀ {Γ Δ} (ρ : Thinning Γ Δ) → ∀ t → 𝓣 t → 𝓣 (ren ρ t)) →
∀ {Γ Δ t} (ρ : Thinning Γ Δ) → (𝓢 +𝓡 𝓣) t → (𝓢 +𝓡 𝓣) (ren ρ t)
th^+𝓡 th^𝓢 th^𝓣 ρ (inl t^𝓢) = inl (th^𝓢 ρ _ t^𝓢)
th^+𝓡 th^𝓢 th^𝓣 ρ (inr t^𝓣) = inr (th^𝓣 ρ _ t^𝓣)
th^𝓡 : (σ : Type) → ∀ {Γ Δ} ρ t → Γ ⊢𝓡 σ ∋ t → Δ ⊢𝓡 σ ∋ ren ρ t
th^𝓡 α ρ t t^𝓡 = th^SN ρ t^𝓡
th^𝓡 ℕ ρ t t^𝓡 = th^<> th^ℕ𝓡 ρ t^𝓡
th^𝓡 (σ + τ) ρ t t^𝓡 = th^<> (th^+𝓡 (th^𝓡 σ) (th^𝓡 τ)) ρ t^𝓡
th^𝓡 (σ ⇒ τ) ρ t t^𝓡 ρ′ u^𝓡 = cast (t^𝓡 (select ρ ρ′) u^𝓡)
where cast = subst (λ t → _ ⊢𝓡 _ ∋ t `∙ _) (sym $ ren² TermD t ρ ρ′)
app^𝓡 : ∀ {σ τ Γ} f t → Γ ⊢𝓡 σ ⇒ τ ∋ f → Γ ⊢𝓡 σ ∋ t → Γ ⊢𝓡 τ ∋ f `∙ t
app^𝓡 f t f^𝓡 t^𝓡 = cast (f^𝓡 (base vl^Var) t^𝓡)
where cast = subst (λ f → _ ⊢𝓡 _ ∋ f `∙ t) (ren-id f)
reify^𝓡 : ∀ Θ τ {Γ Δ i} (sc : Scope (Tm TermD i) Θ τ Γ) (ρ : (Γ ─Env) Term Δ) →
Kripkeᴾ 𝓡ᴾ 𝓡ᴾ Θ τ (Semantics.body Sub ρ Θ τ sc) →
(Θ ++ Δ) ⊢SN τ ∋ sub (lift vl^Tm Θ ρ) sc
reify^𝓡 [] τ sc ρ scᴾ = cast (quote^𝓡 _ scᴾ) where
cast = subst (_ ⊢SN _ ∋_) (Simulation.sim Sim.SubExt (lift[]^Tm ρ) sc)
reify^𝓡 Θ@(_ ∷ _) τ sc ρ scᴾ = quote^𝓡 τ (scᴾ nms (nmsᴿ)) where
nms = freshʳ vl^Var Θ
nmsᴿ : P.All 𝓡ᴾ _ (freshˡ vl^Tm _)
lookupᴾ nmsᴿ k = unquote^𝓡 _ (lookupᴾ freshˡ^SNe k)
sub^𝓡 : ∀ Θ τ {i Γ Δ} (sc : Scope (Tm TermD i) Θ τ Γ) (vs : (Θ ─Env) Term Δ) (ρ : (Γ ─Env) Term Δ) →
Kripkeᴾ 𝓡ᴾ 𝓡ᴾ Θ τ (Semantics.body Sub ρ Θ τ sc) →
P.All 𝓡ᴾ _ vs →
Δ ⊢𝓡 τ ∋ sub (vs >> base vl^Tm) (sub (lift vl^Tm Θ ρ) sc)
sub^𝓡 [] τ sc vs ρ scᴿ vsᴿ = cast scᴿ where
subᴿ : R.All Eqᴿ _ (sub (vs >> base vl^Tm) <$> lift vl^Tm [] ρ) ρ
lookupᴿ subᴿ k = begin
sub (vs >> base vl^Tm) (ren (th^Env th^Var (base vl^Var) (pack id)) (lookup ρ k))
≡⟨ rensub TermD (lookup ρ k) (th^Env th^Var (base vl^Var) (pack id)) (vs >> base vl^Tm) ⟩
sub (select (th^Env th^Var (base vl^Var) (pack id)) (base vl^Tm)) (lookup ρ k)
≡⟨ Simulation.sim Sim.SubExt (packᴿ (λ v → cong (lookup (base vl^Tm)) (lookup-base^Var v))) (lookup ρ k) ⟩
sub (base vl^Tm) (lookup ρ k)
≡⟨ sub-id (lookup ρ k) ⟩
lookup ρ k
∎
cast = subst (_ ⊢𝓡 τ ∋_) (sym (Fusion.fusion (Sub² TermD) subᴿ sc))
sub^𝓡 Θ@(_ ∷ _) τ sc vs ρ scᴿ vsᴿ = cast (scᴿ (base vl^Var) vsᴿ) where
subᴿ : R.All Eqᴿ _ (sub (vs >> base vl^Tm) <$> lift vl^Tm Θ ρ)
(vs >> th^Env th^Tm ρ (base vl^Var))
lookupᴿ subᴿ k with split Θ k
... | inj₁ k₁ = begin
sub (vs >> base vl^Tm) (ren (pack (injectˡ _)) (lookup ((th^Env th^Tm (base vl^Tm) (pack Var.s)) ∙ `var Var.z) k₁))
≡⟨ cong (λ v → sub (vs >> base vl^Tm) (ren (pack (injectˡ _)) v)) (lookupᴿ th^base^s∙z k₁) ⟩
sub (vs >> base vl^Tm) (ren (pack (injectˡ _)) (`var k₁))
≡⟨ injectˡ->> vs (base vl^Tm) k₁ ⟩
lookup vs k₁
∎
... | inj₂ k₂ = begin
sub (vs >> base vl^Tm) (ren (th^Env th^Var (base vl^Var) (pack (injectʳ Θ))) (lookup ρ k₂))
≡⟨ rensub TermD (lookup ρ k₂) (th^Env th^Var (base vl^Var) (pack (injectʳ Θ))) (vs >> base vl^Tm) ⟩
sub (select (th^Env th^Var (base vl^Var) (pack (injectʳ Θ))) (vs >> base vl^Tm)) (lookup ρ k₂)
≡⟨ Simulation.sim Sim.SubExt sub'ᴿ (lookup ρ k₂) ⟩
sub (`var <$> base vl^Var) (lookup ρ k₂)
≡⟨ sym (Sim.rensub (base vl^Var) (lookup ρ k₂)) ⟩
ren (base vl^Var) (lookup ρ k₂)
∎ where
sub'ᴿ : R.All Eqᴿ _ (select (th^Env th^Var (base vl^Var) (pack (injectʳ Θ))) (vs >> base vl^Tm))
(`var <$> base vl^Var)
lookupᴿ sub'ᴿ k = begin
lookup (vs >> base vl^Tm) (lookup {𝓥 = Var} (pack (injectʳ Θ)) (lookup (base vl^Var) k))
≡⟨ cong (λ v → lookup (vs >> base vl^Tm) (lookup {𝓥 = Var} (pack (injectʳ Θ)) v)) (lookup-base^Var k) ⟩
lookup (vs >> base vl^Tm) (injectʳ Θ k)
≡⟨ injectʳ->> vs (base vl^Tm) k ⟩
lookup (base vl^Tm) k
≡⟨ sym (lookupᴿ base^VarTmᴿ k) ⟩
lookup {𝓥 = Term} (`var <$> base vl^Var) k
∎
cast = subst (_ ⊢𝓡 τ ∋_) (sym (Fusion.fusion (Sub² TermD) subᴿ sc))
[/0]^𝓡 :
∀ σ τ {Γ Δ i} t (l : Tm TermD i τ (σ ∷ Γ)) (ρ : (Γ ─Env) Term Δ) →
Δ ⊢𝓡 σ ∋ t →
Kripkeᴾ 𝓡ᴾ 𝓡ᴾ (σ ∷ []) τ (Semantics.body Sub ρ (σ ∷ []) τ l) →
Δ ⊢𝓡 τ ∋ sub (lift vl^Tm (σ ∷ []) ρ) l [ t /0]
[/0]^𝓡 σ τ t l ρ tᴾ lᴾ = cast (sub^𝓡 (σ ∷ []) τ l (ε ∙ t) ρ lᴾ (εᴾ ∙ᴾ tᴾ)) where
subᴿ : R.All Eqᴿ _ ((ε ∙ t) >> base vl^Tm) (t /0])
lookupᴿ subᴿ Var.z = refl
lookupᴿ subᴿ (Var.s v) = refl
cast = subst (_ ⊢𝓡 τ ∋_) (Simulation.sim Sim.SubExt subᴿ (sub _ l))
case^𝓡 : ∀ {σ τ ν i Γ Δ} (t : Term (σ + τ) Δ)
(l : Tm TermD i ν (σ ∷ Γ)) (r : Tm TermD i ν (τ ∷ Γ))
(ρ : (Γ ─Env) Term Δ) → Δ ⊢𝓡 σ + τ ∋ t →
Kripkeᴾ 𝓡ᴾ 𝓡ᴾ (σ ∷ []) ν (Semantics.body Sub ρ (σ ∷ []) ν l) →
Kripkeᴾ 𝓡ᴾ 𝓡ᴾ (τ ∷ []) ν (Semantics.body Sub ρ (τ ∷ []) ν r) →
Δ ⊢𝓡 ν ∋ `case t (sub (lift vl^Tm (σ ∷ []) ρ) l) (sub (lift vl^Tm (τ ∷ []) ρ) r)
case^𝓡 {σ} {τ} {ν} t bl br ρ (neu t^SNe) blᴾ brᴾ =
unquote^𝓡 ν (cas t^SNe (reify^𝓡 (σ ∷ []) ν bl ρ blᴾ) (reify^𝓡 (τ ∷ []) ν br ρ brᴾ))
case^𝓡 t bl br ρ (red r tᴾ) blᴾ brᴾ =
↝SN⁻¹^𝓡 _ ([c]₁ r (sub _ bl) (sub _ br)) (case^𝓡 _ bl br ρ tᴾ blᴾ brᴾ)
case^𝓡 {σ} {τ} {ν} (`i₁ t) bl br ρ (cnd (inl tᴾ)) blᴾ brᴾ =
↝SN⁻¹^𝓡 _ (ι₁ t (sub _ bl) (sub _ br) (quote^𝓡 _ tᴾ) (reify^𝓡 (τ ∷ []) ν br ρ brᴾ))
([/0]^𝓡 _ _ t bl ρ tᴾ blᴾ)
case^𝓡 {σ} {τ} {ν} (`i₂ t) bl br ρ (cnd (inr tᴾ)) blᴾ brᴾ =
↝SN⁻¹^𝓡 _ (ι₂ t (sub _ bl) (sub _ br) (quote^𝓡 _ tᴾ) (reify^𝓡 (σ ∷ []) ν bl ρ blᴾ))
([/0]^𝓡 _ _ t br ρ tᴾ brᴾ)
rec^𝓡 : ∀ {σ i Γ Δ} (ze : Tm TermD i σ Γ) (su : Tm TermD i σ (σ ∷ ℕ ∷ Γ))
(t : Term ℕ Δ) (ρ : (Γ ─Env) Term Δ) →
Δ ⊢𝓡 σ ∋ sub ρ ze → Kripkeᴾ 𝓡ᴾ 𝓡ᴾ (σ ∷ ℕ ∷ []) σ (Semantics.body Sub ρ (σ ∷ ℕ ∷ []) σ su) →
Δ ⊢𝓡 ℕ ∋ t →
Δ ⊢𝓡 σ ∋ `rec (sub ρ ze) (sub (lift vl^Tm (σ ∷ ℕ ∷ []) ρ) su) t
rec^𝓡 {σ} ze su t ρ ze^𝓡 su^𝓡 (neu t^SNe) =
unquote^𝓡 σ (rec (quote^𝓡 _ ze^𝓡) (reify^𝓡 (σ ∷ ℕ ∷ []) σ su ρ su^𝓡) t^SNe)
rec^𝓡 {σ} ze su t ρ ze^𝓡 su^𝓡 (red r t^𝓡) =
↝SN⁻¹^𝓡 σ ([r]₃ (sub ρ ze) (sub _ su) r) (rec^𝓡 ze su _ ρ ze^𝓡 su^𝓡 t^𝓡)
rec^𝓡 ze su .`0 ρ ze^𝓡 su^𝓡 (cnd zro) =
↝SN⁻¹^𝓡 _ (ιz (sub ρ ze) (sub _ su) (reify^𝓡 (_ ∷ ℕ ∷ []) _ su ρ su^𝓡)) ze^𝓡
rec^𝓡 {σ} ze su .(`1+ _) ρ ze^𝓡 su^𝓡 (cnd (suc {t = t} t^𝓡)) =
↝SN⁻¹^𝓡 _ (ιs (sub ρ ze) (sub _ su) _ (quote^𝓡 σ ze^𝓡) (quote^𝓡 ℕ t^𝓡))
$ subst (_ ⊢𝓡 σ ∋_) (Simulation.sim Sim.SubExt subᴿ (sub (lift vl^Tm (σ ∷ ℕ ∷ []) ρ) su))
$ sub^𝓡 (σ ∷ ℕ ∷ []) σ su (ε ∙ t ∙ `rec (sub ρ ze) (sub _ su) t) ρ su^𝓡
(εᴾ ∙ᴾ t^𝓡 ∙ᴾ rec^𝓡 ze su t ρ ze^𝓡 su^𝓡 t^𝓡) where
subᴿ : R.All Eqᴿ _ ((ε ∙ t ∙ `rec (sub ρ ze) (sub _ su) t) >> base vl^Tm)
(base vl^Tm ∙ t ∙ `rec (sub ρ ze) (sub _ su) t)
lookupᴿ subᴿ Var.z = refl
lookupᴿ subᴿ (Var.s Var.z) = refl
lookupᴿ subᴿ (Var.s (Var.s v)) = refl
fundamental : Fundamental TermD Sub 𝓡ᴾ 𝓡ᴾ
Fundamental.thᴾ fundamental {i = σ} {v = v} = λ ρ v^𝓡 → th^𝓡 σ ρ v v^𝓡
Fundamental.varᴾ fundamental = λ x → x
Fundamental.algᴾ fundamental = algᴾ where
algᴾ : ∀ {ρ} (b : ⟦ TermD ⟧ (Scope (Tm TermD i)) σ Γ) →
let v = fmap TermD (Semantics.body Sub ρ) b in
P.All 𝓡ᴾ _ ρ → Fdm.All TermD (Kripkeᴾ 𝓡ᴾ 𝓡ᴾ) v → Δ ⊢𝓡 σ ∋ Semantics.alg Sub v
algᴾ (`i₁' t) ρᴾ (tᴾ , _) = cnd (inl tᴾ)
algᴾ (`i₂' t) ρᴾ (tᴾ , _) = cnd (inr tᴾ)
algᴾ `0' ρᴾ _ = cnd zro
algᴾ (`1+' t) ρᴾ (tᴾ , _) = cnd (suc tᴾ)
algᴾ {ρ = ρ} (`case' t l r) ρᴾ (tᴾ , lᴾ , rᴾ , _) = case^𝓡 (sub ρ t) l r ρ tᴾ lᴾ rᴾ
algᴾ (`rec' ze su t) ρᴾ (zᴾ , sᴾ , tᴾ , _) = rec^𝓡 ze su (sub _ t) _ zᴾ sᴾ tᴾ
algᴾ (f `∙' t) ρᴾ (fᴾ , tᴾ , _) = app^𝓡 (sub _ f) (sub _ t) fᴾ tᴾ
algᴾ {ρ = ρ₁} (`λ' b) ρᴾ (bᴾ , _) ρ {u} u^𝓡 =
↝SN⁻¹^𝓡 _ β-step $ cast (bᴾ ρ (εᴾ ∙ᴾ u^𝓡))
where
β-step = β (ren _ (sub _ b)) _ (quote^𝓡 _ u^𝓡)
ρ′ = lift vl^Var (_ ∷ []) ρ
ρ₁′ = lift vl^Tm (_ ∷ []) ρ₁
ρᴿ : R.All VarTmᴿ _ ρ (select (freshʳ vl^Var (_ ∷ [])) (select ρ′ (u /0])))
lookupᴿ ρᴿ k = sym $ begin
lookup (base vl^Tm) (lookup (base vl^Var) (lookup ρ (lookup (base vl^Var) k)))
≡⟨ lookup-base^Tm _ ⟩
`var (lookup (base vl^Var) (lookup ρ (lookup (base vl^Var) k)))
≡⟨ cong `var (lookup-base^Var _) ⟩
`var (lookup ρ (lookup (base vl^Var) k))
≡⟨ cong (`var ∘ lookup ρ) (lookup-base^Var k) ⟩
`var (lookup ρ k) ∎
ρᴿ′ : R.All Eqᴿ _ (sub (select ρ′ (u /0])) <$> ρ₁′) ((ε ∙ u) >> th^Env th^Tm ρ₁ ρ)
lookupᴿ ρᴿ′ Var.z = refl
lookupᴿ ρᴿ′ (Var.s k) = begin
sub (select ρ′ (u /0])) (ren _ (lookup ρ₁ k)) ≡⟨ rensub TermD (lookup ρ₁ k) _ _ ⟩
sub _ (lookup ρ₁ k) ≡⟨ sym $ Simulation.sim Sim.RenSub ρᴿ (lookup ρ₁ k) ⟩
ren ρ (lookup ρ₁ k) ∎
eq : sub ((ε ∙ u) >> th^Env th^Tm ρ₁ ρ) b ≡ ren ρ′ (sub ρ₁′ b) [ u /0]
eq = sym $ begin
ren ρ′ (sub ρ₁′ b) [ u /0] ≡⟨ rensub TermD (sub ρ₁′ b) ρ′ (u /0]) ⟩
sub (select ρ′ (u /0])) (sub ρ₁′ b) ≡⟨ Fusion.fusion (Sub² TermD) ρᴿ′ b ⟩
sub ((ε ∙ u) >> th^Env th^Tm ρ₁ ρ) b ∎
cast = subst (_ ⊢𝓡 _ ∋_) eq
eval : ∀ {Γ Δ σ ρ} → P.All 𝓡ᴾ _ ρ → (t : Term σ Γ) → Δ ⊢𝓡 σ ∋ sub ρ t
eval = Fundamental.fundamental fundamental
dummy : P.All 𝓡ᴾ Γ (base vl^Tm)
lookupᴾ dummy v rewrite lookup-base^Tm {d = TermD} v = unquote^𝓡 _ (var v)
_^SN : ∀ t → Γ ⊢SN σ ∋ t
t ^SN = cast (quote^𝓡 _ (eval dummy t))
where cast = subst (_ ⊢SN _ ∋_) (sub-id t)
_^sn : ∀ t → Γ ⊢sn σ ∋ t
t ^sn = sound^SN (t ^SN)