open import Definition.Typed.EqualityRelation
open import Definition.Typed.Restrictions
open import Graded.Modality
module Definition.LogicalRelation.Substitution.Introductions.Nat
{a} {M : Set a}
{π : Modality M}
(R : Type-restrictions π)
β¦ eqrel : EqRelSet R β¦
where
open EqRelSet eqrel
open Type-restrictions R
open import Definition.LogicalRelation R
open import Definition.LogicalRelation.Hidden R
open import Definition.LogicalRelation.Irrelevance R
open import Definition.LogicalRelation.Properties R
open import Definition.LogicalRelation.ShapeView R
open import Definition.LogicalRelation.Substitution R
open import
Definition.LogicalRelation.Substitution.Introductions.Universe R
open import Definition.LogicalRelation.Substitution.Introductions.Var R
open import Definition.Typed R
open import Definition.Typed.Properties R
open import Definition.Typed.Reasoning.Reduction.Primitive R
open import Definition.Untyped M
open import Definition.Untyped.Neutral M type-variant
open import Definition.Untyped.Properties M
open import Tools.Empty
open import Tools.Fin
open import Tools.Function
open import Tools.Product as Ξ£
import Tools.PropositionalEquality as PE
import Tools.Reasoning.PropositionalEquality
private variable
Ξ Ξ : Con Term _
A Aβ Aβ B t tβ tβ u uβ uβ v vβ vβ : Term _
Οβ Οβ : Subst _ _
l lβ² lβ³ lβ΄ : TypeLevel
p q r : M
opaque
β©ββ : Ξ β©β¨ l β© β β β’ Ξ
β©ββ =
lemma ββ β-elim
, (Ξ» β’Ξ β βα΅£ ([_,_,_] (ββ±Ό β’Ξ) (ββ±Ό β’Ξ) (id (ββ±Ό β’Ξ))))
where
lemma : Ξ β©β¨ l β©β β β β’ Ξ
lemma (emb 0<1 β©β) = lemma β©β
lemma (noemb [ β’β , _ , _ ]) = wf β’β
opaque
β©ββ·Uβ : Ξ β©β¨ ΒΉ β© β β· U β β’ Ξ
β©ββ·Uβ =
(Ξ» β©β β
case β©β·Uβ .projβ β©β of Ξ»
(_ , _ , ββ* , _) β
wfTerm (β’t-redβ ββ*))
, (Ξ» β’Ξ β
β©β·Uβ .projβ
( (_ , 0<1 , β©ββ .projβ β’Ξ)
, (_ , idRedTerm:*: (ββ±Ό β’Ξ) , ββ , β
β-βrefl β’Ξ)
))
opaque
unfolding _β©β¨_β©_β·_
β©β·ββ : Ξ β©β¨ l β© t β· β β Ξ β©β t β·β
β©β·ββ =
(Ξ» (β©β , β©t) β
lemma (β-elim β©β)
((irrelevanceTerm β©β) (β-intr (β-elim β©β)) β©t))
, (Ξ» β©t β
βα΅£ (idRed:*: (ββ±Ό (wfTerm (β’t-redβ (_β©β_β·β.d β©t))))) , β©t)
where
lemma :
(β©A : Ξ β©β¨ l β©β A) β
Ξ β©β¨ l β© t β· A / β-intr β©A β
Ξ β©β t β·β
lemma (noemb _) β©t = β©t
lemma (emb 0<1 β©A) β©t = lemma β©A β©t
opaque
β©zeroβ·ββ : Ξ β©β¨ l β© zero β· β β β’ Ξ
β©zeroβ·ββ =
wfTerm ββ escape-β©β·
, (Ξ» β’Ξ β
β©β·ββ .projβ $
ββ _ (idRedTerm:*: (zeroβ±Ό β’Ξ)) (β
β-zerorefl β’Ξ) zeroα΅£)
opaque
β©sucβ·ββ :
Ξ β©β¨ l β© suc t β· β β
Ξ β©β¨ l β© t β· β
β©sucβ·ββ {Ξ} {l} {t} =
Ξ β©β¨ l β© suc t β· β ββ¨ β©β·ββ β©
Ξ β©β suc t β·β ββ¨ (Ξ» (ββ _ suc-tβ*u _ u-ok) β
case whnfRed*Term (redβ suc-tβ*u) sucβ of Ξ» {
PE.refl β
lemma u-ok })
, (Ξ» β©t@(ββ _ [ β’t , _ , tβ*u ] uβ
u u-ok) β
let tβu = tβ*u , naturalWhnf (natural u-ok) in
ββ _ (idRedTerm:*: (sucβ±Ό β’t))
(β
-suc-cong $
β
β-red (id (ββ±Ό (wfTerm β’t)) , ββ) tβu tβu uβ
u)
(sucα΅£ β©t))
β©
Ξ β©β t β·β βΛβ¨ β©β·ββ β©
Ξ β©β¨ l β© t β· β β‘β
where
lemma : Natural-prop Ξ (suc t) β Ξ β©β t β·β
lemma (sucα΅£ β©t) = β©t
opaque
unfolding _β©β¨_β©_β‘_
β©ββ‘β : Ξ β©β¨ l β© β β‘ A β Ξ β©β β β‘ A
β©ββ‘β =
(Ξ» (β©β , _ , ββ‘A) β
lemma (β-elim β©β)
((irrelevanceEq β©β) (β-intr (β-elim β©β)) ββ‘A))
, (Ξ» ββ‘A β
case idRed:*: (ββ±Ό (wfEq (subset* ββ‘A))) of Ξ»
ββ*β β
let β©β = βα΅£ ββ*β in
β©β
, (redSubst* ββ‘A β©β) .projβ
, ββ‘A)
where
lemma :
(β©A : Ξ β©β¨ l β©β A) β
Ξ β©β¨ l β© A β‘ B / β-intr β©A β
Ξ β©β A β‘ B
lemma (noemb _) Aβ‘B = Aβ‘B
lemma (emb 0<1 β©A) Aβ‘B = lemma β©A Aβ‘B
opaque
β©ββ‘ββ·Uβ : Ξ β©β¨ ΒΉ β© β β‘ β β· U β β’ Ξ
β©ββ‘ββ·Uβ =
(Ξ» ββ‘β β
case β©β‘β·Uβ .projβ ββ‘β of Ξ»
(_ , _ , _ , ββ* , _) β
wfTerm (β’t-redβ ββ*))
, (Ξ» β’Ξ β
case idRedTerm:*: (ββ±Ό β’Ξ) of Ξ»
ββ*β β
β©β‘β·Uβ .projβ
( (_ , 0<1 , β©ββ‘β .projβ (id (ββ±Ό β’Ξ)))
, (_ , _ , ββ*β , ββ*β , ββ , ββ , β
β-βrefl β’Ξ)
))
opaque
unfolding _β©β¨_β©_β‘_β·_
β©β‘β·ββ :
Ξ β©β¨ l β© t β‘ u β· β β
(Ξ β©β t β·β Γ Ξ β©β u β·β Γ Ξ β©β t β‘ u β·β)
β©β‘β·ββ =
(Ξ» (β©β , β©t , β©u , tβ‘u) β
lemma (β-elim β©β)
((irrelevanceTerm β©β) (β-intr (β-elim β©β)) β©t)
((irrelevanceTerm β©β) (β-intr (β-elim β©β)) β©u)
((irrelevanceEqTerm β©β) (β-intr (β-elim β©β)) tβ‘u))
, (Ξ» (β©t , β©u , tβ‘u) β
βα΅£ (idRed:*: (ββ±Ό (wfTerm (β’t-redβ (_β©β_β‘_β·β.d tβ‘u)))))
, β©t , β©u , tβ‘u)
where
lemma :
(β©A : Ξ β©β¨ l β©β A) β
Ξ β©β¨ l β© t β· A / β-intr β©A β
Ξ β©β¨ l β© u β· A / β-intr β©A β
Ξ β©β¨ l β© t β‘ u β· A / β-intr β©A β
Ξ β©β t β·β Γ Ξ β©β u β·β Γ Ξ β©β t β‘ u β·β
lemma (noemb _) β©t β©u tβ‘u = β©t , β©u , tβ‘u
lemma (emb 0<1 β©A) β©t β©u tβ‘u = lemma β©A β©t β©u tβ‘u
opaque
β©zeroβ‘zeroβ·ββ : Ξ β©β¨ l β© zero β‘ zero β· β β β’ Ξ
β©zeroβ‘zeroβ·ββ {Ξ} {l} =
Ξ β©β¨ l β© zero β‘ zero β· β ββ¨ projβ ββ wf-β©β‘β· , refl-β©β‘β· β©
Ξ β©β¨ l β© zero β· β ββ¨ β©zeroβ·ββ β©
β’ Ξ β‘β
opaque
β©sucβ‘sucβ·ββ :
Ξ β©β¨ l β© suc t β‘ suc u β· β β
Ξ β©β¨ l β© t β‘ u β· β
β©sucβ‘sucβ·ββ {Ξ} {l} {t} {u} =
Ξ β©β¨ l β© suc t β‘ suc u β· β ββ¨ β©β‘β·ββ β©
Ξ β©β suc t β·β Γ Ξ β©β suc u β·β Γ Ξ β©β suc t β‘ suc u β·β ββ¨ β©β·ββ {l = l} ββ β©sucβ·ββ ββ symβ β©β·ββ
Γ-cong-β
β©β·ββ {l = l} ββ β©sucβ·ββ ββ symβ β©β·ββ
Γ-cong-β
(lemmaβ , lemmaβ) β©
Ξ β©β t β·β Γ Ξ β©β u β·β Γ Ξ β©β t β‘ u β·β βΛβ¨ β©β‘β·ββ β©
Ξ β©β¨ l β© t β‘ u β· β β‘β
where
lemmaβ : [Natural]-prop Ξ (suc t) (suc u) β Ξ β©β t β‘ u β·β
lemmaβ (sucα΅£ tβ‘u) = tβ‘u
lemmaβ : Ξ β©β suc t β‘ suc u β·β β Ξ β©β t β‘ u β·β
lemmaβ (βββ _ _ suc-tβ*tβ² suc-uβ*uβ² _ tβ²β‘uβ²) =
case whnfRed*Term (redβ suc-tβ*tβ²) sucβ of Ξ» {
PE.refl β
case whnfRed*Term (redβ suc-uβ*uβ²) sucβ of Ξ» {
PE.refl β
lemmaβ tβ²β‘uβ²}}
lemmaβ : Ξ β©β t β‘ u β·β β Ξ β©β suc t β‘ suc u β·β
lemmaβ
tβ‘u@(βββ _ _ [ β’t , _ , tβ*tβ² ] [ β’u , _ , uβ*uβ² ] tβ²β
uβ² tβ²β‘uβ²) =
let tβ²-ok , uβ²-ok = split tβ²β‘uβ² in
βββ _ _ (idRedTerm:*: (sucβ±Ό β’t)) (idRedTerm:*: (sucβ±Ό β’u))
(β
-suc-cong $
β
β-red (id (ββ±Ό (wfTerm β’t)) , ββ) (tβ*tβ² , naturalWhnf tβ²-ok)
(uβ*uβ² , naturalWhnf uβ²-ok) tβ²β
uβ²)
(sucα΅£ tβ‘u)
opaque
β©zeroβ‘sucβ·ββ : Ξ β©β¨ l β© zero β‘ suc t β· β β β₯
β©zeroβ‘sucβ·ββ =
(Ξ» zeroβ‘suc β
case β©β‘β·ββ .projβ zeroβ‘suc of Ξ»
(_ , _ , βββ _ _ zeroβ* sucβ* _ rest) β
case whnfRed*Term (redβ zeroβ*) zeroβ of Ξ» {
PE.refl β
case whnfRed*Term (redβ sucβ*) sucβ of Ξ» {
PE.refl β
case rest of Ξ» where
(ne (neNfββ () _ _)) }})
, β₯-elim
opaque
βα΅ : β©α΅ Ξ β Ξ β©α΅β¨ l β© β
βα΅ {Ξ} {l} β©Ξ =
β©α΅β .projβ
( β©Ξ
, Ξ» {_} {Ξ = Ξ} {Οβ = Οβ} {Οβ = Οβ} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ ββ¨ projβ ββ escape-β©Λ’β‘β· β©
β’ Ξ ββ¨ ββ±Ό β©
(Ξ β’ β) ββ¨ id β©
Ξ β’ β β* β βΛβ¨ β©ββ‘β β©β
Ξ β©β¨ l β© β β‘ β β‘
)
opaque
βα΅α΅ : β©α΅ Ξ β Ξ β©α΅β¨ ΒΉ β© β β· U
βα΅α΅ {Ξ} β©Ξ =
β©α΅β·β .projβ
( β©α΅U β©Ξ
, Ξ» {_} {Ξ = Ξ} {Οβ = Οβ} {Οβ = Οβ} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ ββ¨ projβ ββ escape-β©Λ’β‘β· β©
β’ Ξ βΛβ¨ β©ββ‘ββ·Uβ β©β
Ξ β©β¨ ΒΉ β© β β‘ β β· U β‘
)
opaque
β©zero :
β’ Ξ β
Ξ β©β¨ l β© zero β· β
β©zero = β©zeroβ·ββ .projβ
opaque
zeroα΅ :
β©α΅ Ξ β
Ξ β©α΅β¨ l β© zero β· β
zeroα΅ {Ξ} {l} β©Ξ =
β©α΅β·β .projβ
( βα΅ β©Ξ
, Ξ» {_} {Ξ = Ξ} {Οβ = Οβ} {Οβ = Οβ} β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ ββ¨ projβ ββ escape-β©Λ’β‘β· β©
β’ Ξ βΛβ¨ β©zeroβ‘zeroβ·ββ β©β
Ξ β©β¨ l β© zero β‘ zero β· β β‘
)
opaque
β©suc :
Ξ β©β¨ l β© t β· β β
Ξ β©β¨ l β© suc t β· β
β©suc = β©sucβ·ββ .projβ
opaque
β©sucβ‘suc :
Ξ β©β¨ l β© t β‘ u β· β β
Ξ β©β¨ l β© suc t β‘ suc u β· β
β©sucβ‘suc = β©sucβ‘sucβ·ββ .projβ
opaque
suc-congα΅ :
Ξ β©α΅β¨ l β© t β‘ u β· β β
Ξ β©α΅β¨ l β© suc t β‘ suc u β· β
suc-congα΅ tβ‘u =
β©α΅β‘β·β .projβ
( βα΅ (wf-β©α΅ $ wf-β©α΅β· $ wf-β©α΅β‘β· tβ‘u .projβ)
, β©sucβ‘suc ββ β©α΅β‘β·β .projβ tβ‘u .projβ
)
opaque
sucα΅ :
Ξ β©α΅β¨ l β© t β· β β
Ξ β©α΅β¨ l β© suc t β· β
sucα΅ β©t =
β©α΅β·ββ©α΅β‘β· .projβ $
suc-congα΅ (refl-β©α΅β‘β· β©t)
private opaque
natrec-subst*β² :
Ξ β β β’ A β
(β {vβ vβ} β
Ξ β©β¨ lβ² β© vβ β‘ vβ β· β β
Ξ β©β¨ l β© A [ vβ ]β β‘ A [ vβ ]β) β
Ξ β’ t β· A [ zero ]β β
Ξ β β β A β’ u β· A [ suc (var x1) ]βΒ² β
Ξ β’ vβ β* vβ β· β β
Ξ β©β¨ lβ² β© vβ β· β β
Ξ β’ natrec p q r A t u vβ β* natrec p q r A t u vβ β· A [ vβ ]β
natrec-subst*β²
{A} {t} {u} {vβ} {vβ} {p} {q} {r} β’A Aβ‘A β’t β’u vββ*vβ β©vβ =
case vββ*vβ of Ξ» where
(id β’vβ) β
id (natrecβ±Ό β’A β’t β’u β’vβ)
(_β¨_ {tβ² = vβ} vββvβ vββ*vβ) β
case
vβ ββ¨ vββvβ β©β©β·
vβ ββ¨ wf-β©β‘β· (β©β·-β* vββ*vβ β©vβ) .projβ β©β©β·
of Ξ»
vββ‘vβ β
natrec p q r A t u vβ β· A [ vβ ]β ββ¨ natrec-subst β’A β’t β’u vββvβ β©β·
β¨ β
-eq $ escape-β©β‘ $ Aβ‘A vββ‘vβ β©β
natrec p q r A t u vβ β· A [ vβ ]β β*β¨ natrec-subst*β² β’A Aβ‘A β’t β’u vββ*vβ β©vβ β©ββ·
natrec p q r A t u vβ β
opaque
natrec-subst* :
Ξ β β β©α΅β¨ l β© A β
Ξ β’ t β· A [ zero ]β β
Ξ β β β A β’ u β· A [ suc (var x1) ]βΒ² β
Ξ β’ vβ β* vβ β· β β
Ξ β©β¨ lβ² β© vβ β· β β
Ξ β’ natrec p q r A t u vβ β* natrec p q r A t u vβ β· A [ vβ ]β
natrec-subst* β©A =
natrec-subst*β² (escape-β©α΅ β©A) (β©α΅β‘ββ©β‘β·ββ©[]ββ‘[]β (refl-β©α΅β‘ β©A))
private opaque
β©natrecβ‘natrecβ² :
Ξ β β β’ Aβ β
Ξ β β β’ Aβ β
Ξ β β β’ Aβ β
Aβ β
(β {vβ vβ} β
Ξ β©β¨ l β© vβ β‘ vβ β· β β
Ξ β©β¨ l β© Aβ [ vβ ]β β‘ Aβ [ vβ ]β) β
(β {vβ vβ} β
Ξ β©β¨ l β© vβ β‘ vβ β· β β
Ξ β©β¨ l β© Aβ [ vβ ]β β‘ Aβ [ vβ ]β) β
(β {vβ vβ} β
Ξ β©β¨ l β© vβ β‘ vβ β· β β
Ξ β©β¨ l β© Aβ [ vβ ]β β‘ Aβ [ vβ ]β) β
Ξ β’ tβ β· Aβ [ zero ]β β
Ξ β’ tβ β· Aβ [ zero ]β β
Ξ β©β¨ l β© tβ β‘ tβ β· Aβ [ zero ]β β
Ξ β β β Aβ β’ uβ β· Aβ [ suc (var x1) ]βΒ² β
Ξ β β β Aβ β’ uβ β· Aβ [ suc (var x1) ]βΒ² β
Ξ β β β Aβ β’ uβ β
uβ β· Aβ [ suc (var x1) ]βΒ² β
(β {vβ vβ wβ wβ} β
Ξ β©β¨ l β© vβ β‘ vβ β· β β
Ξ β©β¨ l β© wβ β‘ wβ β· Aβ [ vβ ]β β
Ξ β©β¨ l β© uβ [ vβ , wβ ]ββ β‘ uβ [ vβ , wβ ]ββ β· Aβ [ suc vβ ]β) β
Ξ β©β vβ β·β β
Ξ β©β vβ β·β β
Ξ β©β vβ β‘ vβ β·β β
Ξ β©β¨ l β© natrec p q r Aβ tβ uβ vβ β‘
natrec p q r Aβ tβ uβ vβ β· Aβ [ vβ ]β
β©natrecβ‘natrecβ²
{Aβ} {Aβ} {l} {tβ} {tβ} {uβ} {uβ} {vβ} {vβ} {p} {q} {r}
β’Aβ β’Aβ Aββ
Aβ Aββ‘Aβ Aββ‘Aβ Aββ‘Aβ β’tβ β’tβ tββ‘tβ β’uβ β’uβ uββ
uβ uββ‘uβ
β©β-vβ@(ββ vββ²β² vββ*vββ²β² _ vββ²β²-prop)
β©β-vβ@(ββ vββ²β² vββ*vββ²β² _ vββ²β²-prop)
β©β-vββ‘vβ@(βββ vββ² vββ² vββ*vββ² vββ*vββ² vββ²β
vββ² vββ²βΌvββ²) =
case Ξ£.map naturalWhnf naturalWhnf $ split vββ²βΌvββ² of Ξ»
(vββ²-whnf , vββ²-whnf) β
case whrDet*Term (redβ vββ*vββ² , vββ²-whnf)
(redβ vββ*vββ²β² , naturalWhnf (natural vββ²β²-prop)) of Ξ» {
PE.refl β
case whrDet*Term (redβ vββ*vββ² , vββ²-whnf)
(redβ vββ*vββ²β² , naturalWhnf (natural vββ²β²-prop)) of Ξ» {
PE.refl β
case β©β‘β·ββ {l = l} .projβ (β©β-vβ , β©β-vβ , β©β-vββ‘vβ) of Ξ»
vββ‘vβ β
case wf-β©β‘β· vββ‘vβ of Ξ»
(β©vβ , β©vβ) β
case β©β·-β* vββ*vββ² β©vβ of Ξ»
vββ‘vββ² β
case β©β·-β* vββ*vββ² β©vβ of Ξ»
vββ‘vββ² β
case wf-β©β‘β· vββ‘vββ² .projβ of Ξ»
β©vββ² β
case wf-β©β‘β· vββ‘vββ² .projβ of Ξ»
β©vββ² β
case
vββ² β‘Λβ¨ vββ‘vββ² β©β©β·
vβ β‘β¨ vββ‘vβ β©β©β·
vβ β‘β¨ vββ‘vββ² β©β©β·β
vββ² β
of Ξ»
vββ²β‘vββ² β
case Aββ‘Aβ vββ²β‘vββ² of Ξ»
Aβ[vββ²]β‘Aβ[vββ²] β
case β
-eq $ escape-β©β‘ Aβ[vββ²]β‘Aβ[vββ²] of Ξ»
β’Aβ[vββ²]β‘Aβ[vββ²] β
case
(Ξ» (hyp : _ β©β¨ l β© _ β‘ _ β· _) β
natrec p q r Aβ tβ uβ vβ β· Aβ [ vβ ]β β*β¨ natrec-subst*β² β’Aβ Aββ‘Aβ β’tβ β’uβ (redβ vββ*vββ²) β©vββ² β©β©β·β·
β¨ Aββ‘Aβ vββ‘vββ² β©β©β·
natrec p q r Aβ tβ uβ vββ² β· Aβ [ vββ² ]β β‘β¨ hyp β©β©β·β·β*
β¨ β’Aβ[vββ²]β‘Aβ[vββ²] β©β
β· Aβ [ vββ² ]β Λβ¨ β
-eq $ escape-β©β‘ $ Aββ‘Aβ vββ‘vββ² β©β
natrec p q r Aβ tβ uβ vββ² β· Aβ [ vβ ]β β*β¨ natrec-subst*β² β’Aβ Aββ‘Aβ β’tβ β’uβ (redβ vββ*vββ²) β©vββ² β©ββ·
natrec p q r Aβ tβ uβ vβ β)
of Ξ»
lemma β
lemma
(case vββ²βΌvββ² of Ξ» where
(ne (neNfββ vββ²-ne vββ²-ne vββ²~vββ²)) β
neutral-β©β‘β· (wf-β©β‘ Aβ[vββ²]β‘Aβ[vββ²] .projβ)
(natrecβ vββ²-ne) (natrecβ vββ²-ne)
(natrecβ±Ό β’Aβ β’tβ β’uβ (escape-β©β· β©vββ²))
(conv (natrecβ±Ό β’Aβ β’tβ β’uβ (escape-β©β· β©vββ²))
(sym β’Aβ[vββ²]β‘Aβ[vββ²])) $
~-natrec β’Aβ Aββ
Aβ (escape-β©β‘β· tββ‘tβ) uββ
uβ vββ²~vββ²
zeroα΅£ β
natrec p q r Aβ tβ uβ zero ββ¨ natrec-zero β’Aβ β’tβ β’uβ β©β©β·
tβ β· Aβ [ zero ]β β‘β¨ tββ‘tβ β©β©β·β·β*
β¨ β’Aβ[vββ²]β‘Aβ[vββ²] β©β
tβ β· Aβ [ zero ]β ββ¨ natrec-zero β’Aβ β’tβ β’uβ , β’tβ β©ββ·
natrec p q r Aβ tβ uβ zero β
(sucα΅£ {n = vββ³} {nβ² = vββ³} β©β-vββ³β‘vββ³) β
case vββ²β²-prop of Ξ» {
(ne suc-ne) β case _β©neNf_β·_.neK suc-ne of Ξ» ();
(sucα΅£ β©β-vββ³) β
case vββ²β²-prop of Ξ» {
(ne suc-ne) β case _β©neNf_β·_.neK suc-ne of Ξ» ();
(sucα΅£ β©β-vββ³) β
case β©β‘β·ββ .projβ (β©β-vββ³ , β©β-vββ³ , β©β-vββ³β‘vββ³) of Ξ»
vββ³β‘vββ³ β
case wf-β©β‘β· vββ³β‘vββ³ of Ξ»
(β©vββ³ , β©vββ³) β
case uββ‘uβ vββ³β‘vββ³ $
β©natrecβ‘natrecβ² β’Aβ β’Aβ Aββ
Aβ Aββ‘Aβ Aββ‘Aβ Aββ‘Aβ
β’tβ β’tβ tββ‘tβ β’uβ β’uβ uββ
uβ uββ‘uβ
β©β-vββ³ β©β-vββ³ β©β-vββ³β‘vββ³ of Ξ»
uβ[vββ³,nr]β‘uβ[vββ³,nr] β
natrec p q r Aβ tβ uβ (suc vββ³) ββ¨ natrec-suc β’Aβ β’tβ β’uβ (escape-β©β· β©vββ³) β©β©β·
uβ [ vββ³ , natrec p q r Aβ tβ uβ vββ³ ]ββ β· Aβ [ suc vββ³ ]β β‘β¨ uβ[vββ³,nr]β‘uβ[vββ³,nr] β©β©β·β·β*
β¨ β’Aβ[vββ²]β‘Aβ[vββ²] β©β
uβ [ vββ³ , natrec p q r Aβ tβ uβ vββ³ ]ββ β· Aβ [ suc vββ³ ]β ββ¨ natrec-suc β’Aβ β’tβ β’uβ (escape-β©β· β©vββ³)
, escape-β©β· $
conv-β©β· Aβ[vββ²]β‘Aβ[vββ²] $
wf-β©β‘β· uβ[vββ³,nr]β‘uβ[vββ³,nr] .projβ
β©ββ·
natrec p q r Aβ tβ uβ (suc vββ³) β }}) }}
opaque
β©natrecβ‘natrec :
Ξ β β β©α΅β¨ l β© Aβ β‘ Aβ β
Ξ β©α΅β¨ lβ² β© tβ β‘ tβ β· Aβ [ zero ]β β
Ξ β β β Aβ β©α΅β¨ lβ³ β© uβ β‘ uβ β· Aβ [ suc (var x1) ]βΒ² β
Ξ β©α΅β¨ lβ΄ β© vβ β‘ vβ β· β β
Ξ β©Λ’ Οβ β‘ Οβ β· Ξ β
Ξ β©β¨ l β© natrec p q r Aβ tβ uβ vβ [ Οβ ] β‘
natrec p q r Aβ tβ uβ vβ [ Οβ ] β· Aβ [ vβ ]β [ Οβ ]
β©natrecβ‘natrec {l} {Aβ} {Aβ} {Οβ} Aββ‘Aβ tββ‘tβ uββ‘uβ vββ‘vβ Οββ‘Οβ =
case wf-β©α΅β‘ Aββ‘Aβ of Ξ»
(β©Aβ , β©Aβ) β
case wf-β©α΅β‘β· tββ‘tβ of Ξ»
(_ , β©tβ) β
case conv-β©α΅β·
(β©α΅β‘ββ©α΅β‘β·ββ©α΅[]ββ‘[]β Aββ‘Aβ $
refl-β©α΅β‘β· $ zeroα΅ {l = l} $ wf-β©α΅ (wf-β©α΅β· β©tβ))
β©tβ of Ξ»
β©tβ β
case wf-β©α΅β‘β· uββ‘uβ of Ξ»
(β©uβ , β©uβ) β
case conv-β-β©α΅β· Aββ‘Aβ $
conv-β©α΅β·
(β©α΅β‘ββ©α΅β·ββ©α΅[]βΒ²β‘[]βΒ² Aββ‘Aβ $
sucα΅ (varα΅ (there here) (wf-β©α΅ (wf-β©α΅β· β©uβ)) .projβ))
β©uβ of Ξ»
β©uβ β
case wf-β©Λ’β‘β· Οββ‘Οβ of Ξ»
(β©Οβ , β©Οβ) β
case β©α΅β‘ββ©Λ’β‘β·ββ©[β]β‘[β] Aββ‘Aβ Οββ‘Οβ of Ξ»
Aβ[Οββ]β‘Aβ[Οββ] β
case PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (singleSubstLift Aβ _) $
β©α΅β‘β·β .projβ tββ‘tβ .projβ Οββ‘Οβ of Ξ»
tβ[Οβ]β‘tβ[Οβ] β
case PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (natrecSucCase _ Aβ) $
β©α΅β‘β·ββ©Λ’β‘β·ββ©[ββ]β‘[ββ]β· uββ‘uβ Οββ‘Οβ of Ξ»
uβ[Οβββ]β‘uβ[Οβββ] β
case β©β‘β·ββ .projβ $
β©α΅β‘β·β .projβ vββ‘vβ .projβ Οββ‘Οβ of Ξ»
(β©β-vβ , β©β-vβ , β©β-vββ‘vβ) β
PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _) (PE.sym $ singleSubstLift Aβ _) $
β©natrecβ‘natrecβ²
(escape $ wf-β©β‘ Aβ[Οββ]β‘Aβ[Οββ] .projβ)
(escape $ β©α΅ββ©Λ’β·ββ©[β] β©Aβ β©Οβ)
(escape-β©β‘ Aβ[Οββ]β‘Aβ[Οββ])
(β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]β (refl-β©α΅β‘ β©Aβ) (refl-β©Λ’β‘β· β©Οβ))
(β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]β (refl-β©α΅β‘ β©Aβ) (refl-β©Λ’β‘β· β©Οβ))
(β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]β Aββ‘Aβ Οββ‘Οβ)
(escape-β©β· $ wf-β©β‘β· tβ[Οβ]β‘tβ[Οβ] .projβ)
(PE.subst (_β’_β·_ _ _) (singleSubstLift Aβ _) $
escape-β©β· $ β©α΅β·ββ©Λ’β·ββ©[]β· β©tβ β©Οβ)
(level-β©β‘β·
(wf-β©β‘
(β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]β Aββ‘Aβ Οββ‘Οβ $
refl-β©β‘β· $ β©zero {l = l} $ escape-β©Λ’β· β©Οβ .projβ)
.projβ)
tβ[Οβ]β‘tβ[Οβ])
(escape-β©β· $ wf-β©β‘β· uβ[Οβββ]β‘uβ[Οβββ] .projβ)
(PE.subst (_β’_β·_ _ _) (natrecSucCase _ Aβ) $
escape-β©β· $ β©α΅β·ββ©Λ’β·ββ©[ββ]β· β©uβ β©Οβ)
(escape-β©β‘β· uβ[Οβββ]β‘uβ[Οβββ])
(Ξ» {vβ = vβ} {vβ = _} {wβ = wβ} vββ‘vβ wββ‘wβ β
level-β©β‘β·
(wf-β©β‘
(β©α΅β‘ββ©Λ’β‘β·ββ©β‘β·ββ©[β][]ββ‘[β][]β Aββ‘Aβ Οββ‘Οβ $
β©sucβ‘suc vββ‘vβ)
.projβ) $
PE.subst (_β©β¨_β©_β‘_β·_ _ _ _ _)
(Aβ [ suc (var x1) ]βΒ² [ Οβ β β ] [ vβ , wβ ]ββ β‘β¨ PE.cong _[ _ , _ ]ββ $ natrecSucCase _ Aβ β©
Aβ [ Οβ β ] [ suc (var x1) ]βΒ² [ vβ , wβ ]ββ β‘Λβ¨ substCompβΒ² (Aβ [ _ ]) _ β©
Aβ [ Οβ β ] [ suc vβ ]β β) $
β©α΅β‘β·ββ©Λ’β‘β·ββ©β‘β·ββ©β‘β·ββ©[ββ][]βββ‘[ββ][]βββ· uββ‘uβ Οββ‘Οβ vββ‘vβ wββ‘wβ)
β©β-vβ β©β-vβ β©β-vββ‘vβ
where
open Tools.Reasoning.PropositionalEquality
opaque
natrec-congα΅ :
Ξ β β β©α΅β¨ l β© Aβ β‘ Aβ β
Ξ β©α΅β¨ lβ² β© tβ β‘ tβ β· Aβ [ zero ]β β
Ξ β β β Aβ β©α΅β¨ lβ³ β© uβ β‘ uβ β· Aβ [ suc (var x1) ]βΒ² β
Ξ β©α΅β¨ lβ΄ β© vβ β‘ vβ β· β β
Ξ β©α΅β¨ l β© natrec p q r Aβ tβ uβ vβ β‘ natrec p q r Aβ tβ uβ vβ β·
Aβ [ vβ ]β
natrec-congα΅ Aββ‘Aβ tββ‘tβ uββ‘uβ vββ‘vβ =
β©α΅β‘β·β .projβ
( β©α΅ββ©α΅β·ββ©α΅[]β (wf-β©α΅β‘ Aββ‘Aβ .projβ) (wf-β©α΅β‘β· vββ‘vβ .projβ)
, β©natrecβ‘natrec Aββ‘Aβ tββ‘tβ uββ‘uβ vββ‘vβ
)
opaque
natrecα΅ :
Ξ β β β©α΅β¨ l β© A β
Ξ β©α΅β¨ lβ² β© t β· A [ zero ]β β
Ξ β β β A β©α΅β¨ lβ³ β© u β· A [ suc (var x1) ]βΒ² β
Ξ β©α΅β¨ lβ΄ β© v β· β β
Ξ β©α΅β¨ l β© natrec p q r A t u v β· A [ v ]β
natrecα΅ β©A β©t β©u β©v =
β©α΅β·ββ©α΅β‘β· .projβ $
natrec-congα΅ (refl-β©α΅β‘ β©A) (refl-β©α΅β‘β· β©t) (refl-β©α΅β‘β· β©u)
(refl-β©α΅β‘β· β©v)
opaque
natrec-zeroα΅ :
Ξ β β β©α΅β¨ lβ² β© A β
Ξ β©α΅β¨ l β© t β· A [ zero ]β β
Ξ β β β A β©α΅β¨ lβ³ β© u β· A [ suc (var x1) ]βΒ² β
Ξ β©α΅β¨ l β© natrec p q r A t u zero β‘ t β· A [ zero ]β
natrec-zeroα΅ {A} β©A β©t β©u =
β©α΅β·-β
(Ξ» β©Ο β
PE.subst (_β’_β_β·_ _ _ _) (PE.sym $ singleSubstLift A _) $
natrec-zero
(escape $ β©α΅ββ©Λ’β·ββ©[β] β©A β©Ο)
(PE.subst (_β’_β·_ _ _) (singleSubstLift A _) $
escape-β©β· $ β©α΅β·ββ©Λ’β·ββ©[]β· β©t β©Ο)
(PE.subst (_β’_β·_ _ _) (natrecSucCase _ A) $
escape-β©β· $ β©α΅β·ββ©Λ’β·ββ©[ββ]β· β©u β©Ο))
β©t
opaque
natrec-sucα΅ :
Ξ β β β©α΅β¨ lβ² β© A β
Ξ β©α΅β¨ lβ³ β© t β· A [ zero ]β β
Ξ β β β A β©α΅β¨ l β© u β· A [ suc (var x1) ]βΒ² β
Ξ β©α΅β¨ lβ΄ β© v β· β β
Ξ β©α΅β¨ l β© natrec p q r A t u (suc v) β‘
u [ v , natrec p q r A t u v ]ββ β· A [ suc v ]β
natrec-sucα΅ {A} {u} β©A β©t β©u β©v =
β©α΅β·-β
(Ξ» β©Ο β
PE.substβ (_β’_β_β·_ _ _) (PE.sym $ [,]-[]-commute u)
(PE.sym $ singleSubstLift A _) $
natrec-suc
(escape $ β©α΅ββ©Λ’β·ββ©[β] β©A β©Ο)
(PE.subst (_β’_β·_ _ _) (singleSubstLift A _) $
escape-β©β· $ β©α΅β·ββ©Λ’β·ββ©[]β· β©t β©Ο)
(PE.subst (_β’_β·_ _ _) (natrecSucCase _ A) $
escape-β©β· $ β©α΅β·ββ©Λ’β·ββ©[ββ]β· β©u β©Ο)
(escape-β©β· $ β©α΅β·ββ©Λ’β·ββ©[]β· β©v β©Ο))
(PE.subst (_β©α΅β¨_β©_β·_ _ _ _) (PE.sym $ substCompβΒ² A _) $
β©α΅β·ββ©α΅β·ββ©α΅β·ββ©α΅[]βββ· β©u β©v (natrecα΅ β©A β©t β©u β©v))