module A202401.STLC-Naturals-SWNF-CBV where
open import A202401.STLC-Naturals-RenSub public
open import A202401.STLC-Naturals-SWNF public
open import A202401.Kit3 public
infix 4 _⇒_
data _⇒_ {Γ} : ∀ {A} → Γ ⊢ A → Γ ⊢ A → Set where
cong$₁ : ∀ {A B} {t₁ t₁′ : Γ ⊢ A ⌜⊃⌝ B} {t₂ : Γ ⊢ A} (r₁ : t₁ ⇒ t₁′) →
t₁ ⌜$⌝ t₂ ⇒ t₁′ ⌜$⌝ t₂
cong$₂ : ∀ {A B} {t₁ : Γ ⊢ A ⌜⊃⌝ B} {t₂ t₂′ : Γ ⊢ A} (p₁ : NF t₁) (r₂ : t₂ ⇒ t₂′) →
t₁ ⌜$⌝ t₂ ⇒ t₁ ⌜$⌝ t₂′
congsuc : ∀ {t t′ : Γ ⊢ ⌜ℕ⌝} (r : t ⇒ t′) → ⌜suc⌝ t ⇒ ⌜suc⌝ t′
congrecₙ : ∀ {A} {tₙ tₙ′ : Γ ⊢ ⌜ℕ⌝} {t₀ : Γ ⊢ A} {tₛ : (Γ , ⌜ℕ⌝) , A ⊢ A} (rₙ : tₙ ⇒ tₙ′) →
⌜rec⌝ tₙ t₀ tₛ ⇒ ⌜rec⌝ tₙ′ t₀ tₛ
congrec₀ : ∀ {A} {tₙ : Γ ⊢ ⌜ℕ⌝} {t₀ t₀′ : Γ ⊢ A} {tₛ : (Γ , ⌜ℕ⌝) , A ⊢ A} (pₙ : NF tₙ)
(r₀ : t₀ ⇒ t₀′) →
⌜rec⌝ tₙ t₀ tₛ ⇒ ⌜rec⌝ tₙ t₀′ tₛ
congrecₛ : ∀ {A} {tₙ : Γ ⊢ ⌜ℕ⌝} {t₀ : Γ ⊢ A} {tₛ tₛ′ : (Γ , ⌜ℕ⌝) , A ⊢ A} (pₙ : NF tₙ)
(p₀ : NF t₀) (rₛ : tₛ ⇒ tₛ′) →
⌜rec⌝ tₙ t₀ tₛ ⇒ ⌜rec⌝ tₙ t₀ tₛ′
βred⊃ : ∀ {A B} {t₁ : Γ , A ⊢ B} {t₂ : Γ ⊢ A} {t′} (eq : t′ ≡ t₁ [ t₂ ]) (p₂ : NF t₂) →
⌜λ⌝ t₁ ⌜$⌝ t₂ ⇒ t′
βredℕ₀ : ∀ {A} {t₀ : Γ ⊢ A} {tₛ : (Γ , ⌜ℕ⌝) , A ⊢ A} (p₀ : NF t₀) (pₛ : NF tₛ) →
⌜rec⌝ ⌜zero⌝ t₀ tₛ ⇒ t₀
βredℕₛ : ∀ {A} {tₙ : Γ ⊢ ⌜ℕ⌝} {t₀ : Γ ⊢ A} {tₛ : (Γ , ⌜ℕ⌝) , A ⊢ A} {t′}
(eq : t′ ≡ tₛ [ wk (⌜rec⌝ tₙ t₀ tₛ) ] [ tₙ ]) → (pₙ : NF (⌜suc⌝ tₙ)) (p₀ : NF t₀)
(pₛ : NF tₛ) →
⌜rec⌝ (⌜suc⌝ tₙ) t₀ tₛ ⇒ t′
open RedKit1 (kit tmkit _⇒_) public
mutual
NF→¬R : ∀ {Γ A} {t : Γ ⊢ A} → NF t → ¬R t
NF→¬R (⌜suc⌝ p) (congsuc r) = r ↯ NF→¬R p
NF→¬R (nnf p) r = r ↯ NNF→¬R p
NNF→¬R : ∀ {Γ A} {t : Γ ⊢ A} → NNF t → ¬R t
NNF→¬R (p₁ ⌜$⌝ p₂) (cong$₁ r₁) = r₁ ↯ NNF→¬R p₁
NNF→¬R (p₁ ⌜$⌝ p₂) (cong$₂ p₁′ r₂) = r₂ ↯ NF→¬R p₂
NNF→¬R (() ⌜$⌝ p₂) (βred⊃ eq p₂′)
NNF→¬R (⌜rec⌝ pₙ p₀ pₛ) (congrecₙ rₙ) = rₙ ↯ NNF→¬R pₙ
NNF→¬R (⌜rec⌝ pₙ p₀ pₛ) (congrec₀ pₙ′ r₀) = r₀ ↯ NF→¬R p₀
NNF→¬R (⌜rec⌝ pₙ p₀ pₛ) (congrecₛ pₙ′ p₀′ rₛ) = rₛ ↯ NF→¬R pₛ
open RedKit2 (kit redkit1 uniNF NF→¬R) public
det⇒ : ∀ {Γ A} {t t′ t″ : Γ ⊢ A} → t ⇒ t′ → t ⇒ t″ → t′ ≡ t″
det⇒ (cong$₁ r₁) (cong$₁ r₁′) = (_⌜$⌝ _) & det⇒ r₁ r₁′
det⇒ (cong$₁ r₁) (cong$₂ p₁′ r₂′) = r₁ ↯ NF→¬R p₁′
det⇒ (cong$₂ p₁ r₂) (cong$₁ r₁′) = r₁′ ↯ NF→¬R p₁
det⇒ (cong$₂ p₁ r₂) (cong$₂ p₁′ r₂′) = (_ ⌜$⌝_) & det⇒ r₂ r₂′
det⇒ (cong$₂ p₁ r₂) (βred⊃ refl p₂′) = r₂ ↯ NF→¬R p₂′
det⇒ (congsuc r) (congsuc r′) = ⌜suc⌝ & det⇒ r r′
det⇒ (congrecₙ rₙ) (congrecₙ rₙ′) = _ & det⇒ rₙ rₙ′
det⇒ (congrecₙ rₙ) (congrec₀ pₙ′ r₀′) = rₙ ↯ NF→¬R pₙ′
det⇒ (congrecₙ rₙ) (congrecₛ pₙ′ p₀′ rₛ′) = rₙ ↯ NF→¬R pₙ′
det⇒ (congrecₙ rₙ) (βredℕₛ refl pₙ′ p₀′ pₛ′) = rₙ ↯ NF→¬R pₙ′
det⇒ (congrec₀ pₙ r₀) (congrecₙ rₙ′) = rₙ′ ↯ NF→¬R pₙ
det⇒ (congrec₀ pₙ r₀) (congrec₀ pₙ′ r₀′) = _ & uniNF pₙ pₙ′ ⊗ det⇒ r₀ r₀′
det⇒ (congrec₀ pₙ r₀) (congrecₛ pₙ′ p₀′ rₛ′) = r₀ ↯ NF→¬R p₀′
det⇒ (congrec₀ pₙ r₀) (βredℕ₀ p₀′ pₛ′) = r₀ ↯ NF→¬R p₀′
det⇒ (congrec₀ pₙ r₀) (βredℕₛ refl pₙ′ p₀′ pₛ′) = r₀ ↯ NF→¬R p₀′
det⇒ (congrecₛ pₙ p₀ rₛ) (congrecₙ rₙ′) = rₙ′ ↯ NF→¬R pₙ
det⇒ (congrecₛ pₙ p₀ rₛ) (congrec₀ pₙ′ r₀′) = r₀′ ↯ NF→¬R p₀
det⇒ (congrecₛ pₙ p₀ rₛ) (congrecₛ pₙ′ p₀′ rₛ′) = _ & uniNF pₙ pₙ′ ⊗ uniNF p₀ p₀
⊗ det⇒ rₛ rₛ′
det⇒ (congrecₛ pₙ p₀ rₛ) (βredℕ₀ p₀′ pₛ′) = rₛ ↯ NF→¬R pₛ′
det⇒ (congrecₛ pₙ p₀ rₛ) (βredℕₛ refl pₙ′ p₀′ pₛ′) = rₛ ↯ NF→¬R pₛ′
det⇒ (βred⊃ refl p₂) (cong$₂ p₁′ r₂′) = r₂′ ↯ NF→¬R p₂
det⇒ (βred⊃ refl p₂) (βred⊃ refl p₂′) = refl
det⇒ (βredℕ₀ p₀ pₛ) (congrec₀ pₙ′ r₀′) = r₀′ ↯ NF→¬R p₀
det⇒ (βredℕ₀ p₀ pₛ) (congrecₛ pₙ′ p₀′ rₛ′) = rₛ′ ↯ NF→¬R pₛ
det⇒ (βredℕ₀ p₀ pₛ) (βredℕ₀ p₀′ pₛ′) = refl
det⇒ (βredℕₛ refl pₙ p₀ pₛ) (congrecₙ rₙ′) = rₙ′ ↯ NF→¬R pₙ
det⇒ (βredℕₛ refl pₙ p₀ pₛ) (congrec₀ pₙ′ r₀′) = r₀′ ↯ NF→¬R p₀
det⇒ (βredℕₛ refl pₙ p₀ pₛ) (congrecₛ pₙ′ p₀′ rₛ′) = rₛ′ ↯ NF→¬R pₛ
det⇒ (βredℕₛ refl pₙ p₀ pₛ) (βredℕₛ refl pₙ′ p₀′ pₛ′) = refl
uni⇒ : ∀ {Γ A} {t t′ : Γ ⊢ A} (r r′ : t ⇒ t′) → r ≡ r′
uni⇒ (cong$₁ r₁) (cong$₁ r₁′) = cong$₁ & uni⇒ r₁ r₁′
uni⇒ (cong$₁ r₁) (cong$₂ p₁′ r₂′) = r₁ ↯ NF→¬R p₁′
uni⇒ (cong$₂ p₁ r₂) (cong$₁ r₁′) = r₁′ ↯ NF→¬R p₁
uni⇒ (cong$₂ p₁ r₂) (cong$₂ p₁′ r₂′) = cong$₂ & uniNF p₁ p₁′ ⊗ uni⇒ r₂ r₂′
uni⇒ (cong$₂ p₁ r₂) (βred⊃ eq′ p₂) = r₂ ↯ NF→¬R p₂
uni⇒ (congsuc r) (congsuc r′) = congsuc & uni⇒ r r′
uni⇒ (congrecₙ rₙ) (congrecₙ rₙ′) = congrecₙ & uni⇒ rₙ rₙ′
uni⇒ (congrecₙ rₙ) (congrec₀ pₙ′ r₀′) = rₙ ↯ NF→¬R pₙ′
uni⇒ (congrecₙ rₙ) (congrecₛ pₙ′ p₀′ rₛ′) = rₙ ↯ NF→¬R pₙ′
uni⇒ (congrecₙ rₙ) (βredℕₛ eq′ pₙ′ p₀′ pₛ′) = rₙ ↯ NF→¬R pₙ′
uni⇒ (congrec₀ pₙ r₀) (congrecₙ rₙ′) = rₙ′ ↯ NF→¬R pₙ
uni⇒ (congrec₀ pₙ r₀) (congrec₀ pₙ′ r₀′) = congrec₀ & uniNF pₙ pₙ′ ⊗ uni⇒ r₀ r₀′
uni⇒ (congrec₀ pₙ r₀) (congrecₛ pₙ′ p₀′ rₛ′) = r₀ ↯ NF→¬R p₀′
uni⇒ (congrec₀ pₙ r₀) (βredℕ₀ p₀′ pₛ′) = r₀ ↯ NF→¬R p₀′
uni⇒ (congrec₀ pₙ r₀) (βredℕₛ eq′ pₙ′ p₀′ pₛ′) = r₀ ↯ NF→¬R p₀′
uni⇒ (congrecₛ pₙ p₀ rₛ) (congrecₙ rₙ′) = rₙ′ ↯ NF→¬R pₙ
uni⇒ (congrecₛ pₙ p₀ rₛ) (congrec₀ pₙ′ r₀′) = r₀′ ↯ NF→¬R p₀
uni⇒ (congrecₛ pₙ p₀ rₛ) (congrecₛ pₙ′ p₀′ rₛ′) = _ & uniNF pₙ pₙ′ ⊗ uniNF p₀ p₀′
⊗ uni⇒ rₛ rₛ′
uni⇒ (congrecₛ pₙ p₀ rₛ) (βredℕₛ eq′ pₙ′ p₀′ pₛ′) = rₛ ↯ NF→¬R pₛ′
uni⇒ (βred⊃ eq p₂) (cong$₂ p₁′ r₂′) = r₂′ ↯ NF→¬R p₂
uni⇒ (βred⊃ refl p₂) (βred⊃ refl p₂′) = βred⊃ refl & uniNF p₂ p₂′
uni⇒ (βredℕ₀ p₀ pₛ) (congrec₀ pₙ′ r₀′) = r₀′ ↯ NF→¬R p₀
uni⇒ (βredℕ₀ p₀ pₛ) (βredℕ₀ p₀′ pₛ′) = βredℕ₀ & uniNF p₀ p₀′ ⊗ uniNF pₛ pₛ′
uni⇒ (βredℕₛ eq pₙ p₀ pₛ) (congrecₙ rₙ′) = rₙ′ ↯ NF→¬R pₙ
uni⇒ (βredℕₛ eq pₙ p₀ pₛ) (congrec₀ pₙ′ r₀′) = r₀′ ↯ NF→¬R p₀
uni⇒ (βredℕₛ eq pₙ p₀ pₛ) (congrecₛ pₙ′ p₀′ rₛ′) = rₛ′ ↯ NF→¬R pₛ
uni⇒ (βredℕₛ refl pₙ p₀ pₛ) (βredℕₛ refl pₙ′ p₀′ pₛ′) = βredℕₛ refl & uniNF pₙ pₙ′ ⊗ uniNF p₀ p₀′
⊗ uniNF pₛ pₛ′
open DetKit (kit redkit2 det⇒ uni⇒) public
prog⇒ : ∀ {Γ A} (t : Γ ⊢ A) → Prog t
prog⇒ (var i) = done (nnf var-)
prog⇒ (⌜λ⌝ t) = done ⌜λ⌝-
prog⇒ (t₁ ⌜$⌝ t₂) with prog⇒ t₁ | prog⇒ t₂
... | step r₁ | _ = step (cong$₁ r₁)
... | done p₁ | step r₂ = step (cong$₂ p₁ r₂)
... | done ⌜λ⌝- | done p₂ = step (βred⊃ refl p₂)
... | done (nnf p₁) | done p₂ = done (nnf (p₁ ⌜$⌝ p₂))
prog⇒ ⌜zero⌝ = done ⌜zero⌝
prog⇒ (⌜suc⌝ t) with prog⇒ t
... | step r = step (congsuc r)
... | done p = done (⌜suc⌝ p)
prog⇒ (⌜rec⌝ tₙ t₀ tₛ) with prog⇒ tₙ | prog⇒ t₀ | prog⇒ tₛ
... | step rₙ | _ | _ = step (congrecₙ rₙ)
... | done pₙ | step r₀ | _ = step (congrec₀ pₙ r₀)
... | done pₙ | done p₀ | step rₛ = step (congrecₛ pₙ p₀ rₛ)
... | done ⌜zero⌝ | done p₀ | done pₛ = step (βredℕ₀ p₀ pₛ)
... | done (⌜suc⌝ pₙ) | done p₀ | done pₛ = step (βredℕₛ refl (⌜suc⌝ pₙ) p₀ pₛ)
... | done (nnf pₙ) | done p₀ | done pₛ = done (nnf (⌜rec⌝ pₙ p₀ pₛ))
open ProgKit (kit redkit2 prog⇒) public
ren⇒ : ∀ {Γ Γ′ A} {t t′ : Γ ⊢ A} (ϱ : Γ ⊑ Γ′) → t ⇒ t′ → ren ϱ t ⇒ ren ϱ t′
ren⇒ ϱ (cong$₁ r₁) = cong$₁ (ren⇒ ϱ r₁)
ren⇒ ϱ (cong$₂ p₁ r₂) = cong$₂ (renNF ϱ p₁) (ren⇒ ϱ r₂)
ren⇒ ϱ (congsuc r) = congsuc (ren⇒ ϱ r)
ren⇒ ϱ (congrecₙ rₙ) = congrecₙ (ren⇒ ϱ rₙ)
ren⇒ ϱ (congrec₀ pₙ r₀) = congrec₀ (renNF ϱ pₙ) (ren⇒ ϱ r₀)
ren⇒ ϱ (congrecₛ pₙ p₀ rₛ) = congrecₛ (renNF ϱ pₙ) (renNF ϱ p₀)
(ren⇒ (lift⊑ (lift⊑ ϱ)) rₛ)
ren⇒ ϱ (βred⊃ {t₁ = t₁} refl p₂) = βred⊃ (rencut ϱ t₁ _ ⁻¹) (renNF ϱ p₂)
ren⇒ ϱ (βredℕ₀ p₀ pₛ) = βredℕ₀ (renNF ϱ p₀) (renNF (lift⊑ (lift⊑ ϱ)) pₛ)
ren⇒ ϱ (βredℕₛ {tₙ = tₙ} {t₀} {tₛ} refl pₙ p₀ pₛ) =
βredℕₛ eq (renNF ϱ pₙ) (renNF ϱ p₀) (renNF (lift⊑ (lift⊑ ϱ)) pₛ)
where
eq : ren ϱ (tₛ [ wk (⌜rec⌝ tₙ t₀ tₛ) ] [ tₙ ]) ≡
ren (lift⊑ (lift⊑ ϱ)) tₛ
[ wk (⌜rec⌝ (ren ϱ tₙ) (ren ϱ t₀) (ren (lift⊑ (lift⊑ ϱ)) tₛ)) ] [ ren ϱ tₙ ]
eq = rencut ϱ (tₛ [ wk (⌜rec⌝ tₙ t₀ tₛ) ]) tₙ ⁻¹
⋮ (_[ ren ϱ tₙ ]) &
( rencut (lift⊑ ϱ) tₛ (wk (⌜rec⌝ tₙ t₀ tₛ)) ⁻¹
⋮ (ren (lift⊑ (lift⊑ ϱ)) tₛ [_]) &
( compren (lift⊑ ϱ) (wk⊑ id⊑) (⌜rec⌝ tₙ t₀ tₛ) ⁻¹
⋮ (flip ren (⌜rec⌝ tₙ t₀ tₛ) ∘ wk⊑) & (rid⊑ ϱ ⋮ lid⊑ ϱ ⁻¹)
⋮ ⌜rec⌝ & compren (wk⊑ id⊑) ϱ tₙ
⊗ compren (wk⊑ id⊑) ϱ t₀
⊗ compren (lift⊑ (lift⊑ (wk⊑ id⊑))) (lift⊑ (lift⊑ ϱ)) tₛ
)
)
sub⇒ : ∀ {Γ Ξ A} {σ : Ξ ⊢§ Γ} {t t′ : Γ ⊢ A} → NNF§ σ → t ⇒ t′ → sub σ t ⇒ sub σ t′
sub⇒ ψ (cong$₁ r₁) = cong$₁ (sub⇒ ψ r₁)
sub⇒ ψ (cong$₂ p₁ r₂) = cong$₂ (subNF ψ p₁) (sub⇒ ψ r₂)
sub⇒ ψ (congsuc r) = congsuc (sub⇒ ψ r)
sub⇒ ψ (congrecₙ rₙ) = congrecₙ (sub⇒ ψ rₙ)
sub⇒ ψ (congrec₀ pₙ r₀) = congrec₀ (subNF ψ pₙ) (sub⇒ ψ r₀)
sub⇒ ψ (congrecₛ pₙ p₀ rₛ) = congrecₛ (subNF ψ pₙ) (subNF ψ p₀)
(sub⇒ (liftNNF§ (liftNNF§ ψ)) rₛ)
sub⇒ ψ (βred⊃ {t₁ = t₁} refl p₂) = βred⊃ (subcut _ t₁ _ ⁻¹) (subNF ψ p₂)
sub⇒ ψ (βredℕ₀ p₀ pₛ) = βredℕ₀ (subNF ψ p₀) (subNF (liftNNF§ (liftNNF§ ψ)) pₛ)
sub⇒ {σ = σ} ψ (βredℕₛ {tₙ = tₙ} {t₀} {tₛ} refl pₙ p₀ pₛ) =
βredℕₛ eq (subNF ψ pₙ) (subNF ψ p₀) (subNF (liftNNF§ (liftNNF§ ψ)) pₛ)
where
eq : sub σ (tₛ [ wk (⌜rec⌝ tₙ t₀ tₛ) ] [ tₙ ]) ≡
sub (lift§ (lift§ σ)) tₛ
[ wk (⌜rec⌝ (sub σ tₙ) (sub σ t₀) (sub (lift§ (lift§ σ)) tₛ)) ] [ sub σ tₙ ]
eq = subcut σ (tₛ [ wk (⌜rec⌝ tₙ t₀ tₛ) ]) tₙ ⁻¹
⋮ (_[ sub σ tₙ ]) &
( subcut (lift§ σ) tₛ (wk (⌜rec⌝ tₙ t₀ tₛ)) ⁻¹
⋮ (sub (lift§ (lift§ σ)) tₛ [_]) &
( eqsubren (lift§ σ) (wk⊑ id⊑) (⌜rec⌝ tₙ t₀ tₛ) ⁻¹
⋮ flip sub (⌜rec⌝ tₙ t₀ tₛ) & lidget§ (wk§ σ)
⋮ ⌜rec⌝ & eqrensub (wk⊑ id⊑) σ tₙ
⊗ eqrensub (wk⊑ id⊑) σ t₀
⊗ ( ((flip sub tₛ ∘ (_, var zero)) ∘ (_, var (wk∋ zero))) &
( wk§ & eqwkren§ (wk⊑ id⊑) σ ⁻¹
⋮ eqwkren§ (lift⊑ (wk⊑ id⊑)) (wk§ σ) ⁻¹
)
⋮ eqrensub (lift⊑ (lift⊑ (wk⊑ id⊑))) (lift§ (lift§ σ)) tₛ
)
)
)