module A201903.5-5-Equivalence-HAO where
open import A201903.1-2-Syntax-Predicates
import A201903.2-1-Semantics-BigStep as BS
import A201903.2-2-Semantics-SmallStep as SS
import A201903.3-3-Properties-BigStep-CBV as BS-CBV
import A201903.3-5-Properties-BigStep-HAO as BS-HAO
import A201903.4-3-Properties-SmallStep-CBV as SS-CBV
import A201903.4-5-Properties-SmallStep-HAO as SS-HAO
import A201903.5-3-Equivalence-CBV as CBV
module Lem-5-5-1 where
open SS-HAO
open BS-HAO
rev-lam* : ∀ {n i s} {e : Tm (suc n)} {e′} → lam s e ⇒*⟨ i ⟩ lam s e′ → e ⇒*⟨ i ⟩ e′
rev-lam* ε = ε
rev-lam* (lam r ◅ rs) = r ◅ rev-lam* rs
¬lam⇒*var : ∀ {n s} {e : Tm (suc n)} {s′ x} → ¬ (lam s e ⇒* var s′ x)
¬lam⇒*var = λ { (lam r ◅ rs) → rs ↯ ¬lam⇒*var }
¬lam-s⇒*lam-s′ : ∀ {n s} {e : Tm (suc n)} {s′ e′} → s ≢ s′ → ¬ (lam s e ⇒* lam s′ e′)
¬lam-s⇒*lam-s′ s≢s′ = λ { ε → refl ↯ s≢s′
; (lam r ◅ rs) → rs ↯ ¬lam-s⇒*lam-s′ s≢s′ }
¬lam⇒*app : ∀ {n s} {e : Tm (suc n)} {e₁ e₂} → ¬ (lam s e ⇒* app e₁ e₂)
¬lam⇒*app = λ { (lam r ◅ rs) → rs ↯ ¬lam⇒*app }
rev-app₂* : ∀ {n i} {e₁ e₂ : Tm n} {e′} →
NANF e₁ → app e₁ e₂ ⇒*⟨ i ⟩ e′ → NF e′ →
(∃ λ e₂′ →
e₂ ⇒*⟨ i ⟩ e₂′ × NF e₂′ × app e₁ e₂′ ≡ e′)
rev-app₂* p₁ ε (nf (app p₁′ p₂)) = _ , ε , p₂ , refl
rev-app₂* () (applam p₂ ◅ rs) p′
rev-app₂* p₁ (cbv-app₁ r₁ ◅ rs) p′ = r₁ ↯ SS-CBV.nrf←nawnf (nawnf←nanf p₁)
rev-app₂* p₁ (app₁ p₁′ r₁ ◅ rs) p′ = r₁ ↯ nrf←nanf p₁
rev-app₂* () (app₂ₐ r₂ ◅ rs) p′
rev-app₂* p₁ (app₂ p₁′ r₂ ◅ rs) p′ with rev-app₂* p₁′ rs p′
... | _ , rs₂ , p₂′ , refl = _ , r₂ ◅ rs₂ , p₂′ , refl
rev-app₁* : ∀ {n i} {e₁ e₂ : Tm n} {e′} →
NAWNF e₁ → app e₁ e₂ ⇒*⟨ i ⟩ e′ → NF e′ →
(∃² λ e₁′ e₂′ →
e₁ ⇒*⟨ i ⟩ e₁′ × NANF e₁′ × e₂ ⇒*⟨ i ⟩ e₂′ × NF e₂′ × app e₁′ e₂′ ≡ e′)
rev-app₁* p₁ ε (nf (app p₁′ p₂′)) = _ , ε , p₁′ , ε , p₂′ , refl
rev-app₁* () (applam p₂ ◅ rs) p′
rev-app₁* p₁ (cbv-app₁ r₁ ◅ rs) p′ = r₁ ↯ SS-CBV.nrf←nawnf p₁
rev-app₁* p₁ (app₁ p₁′ r₁ ◅ rs) p′ with rev-app₁* (nawnf-⇒ p₁′ r₁) rs p′
... | _ , rs₁ , p₁″ , rs₂ , p₂′ , refl = _ , r₁ ◅ rs₁ , p₁″ , rs₂ , p₂′ , refl
rev-app₁* () (app₂ₐ r₂ ◅ rs) p′
rev-app₁* p₁ (app₂ p₁′ r₂ ◅ rs) p′ with rev-app₂* p₁′ rs p′
... | _ , rs₂ , p₂′ , refl = _ , ε , p₁′ , r₂ ◅ rs₂ , p₂′ , refl
rev-app* : ∀ {n i} {e₁ e₂ : Tm n} {e′} →
app e₁ e₂ ⇒*⟨ i ⟩ e′ → NF e′ →
(∃³ λ s e₁′ e₂′ →
e₁ SS.CBV.⇒*⟨ i ⟩ lam s e₁′ × e₂ ⇒*⟨ i ⟩ e₂′ × NF e₂′ × e₁′ [ e₂′ ] ⇒*⟨ i ⟩ e′) ⊎
(∃³ λ e₁′ e₁″ e₂′ →
e₁ SS.CBV.⇒*⟨ i ⟩ e₁′ × NAWNF e₁′ × e₁′ ⇒*⟨ i ⟩ e₁″ × NANF e₁″ ×
e₂ ⇒*⟨ i ⟩ e₂′ × NF e₂′ × app e₁″ e₂′ ≡ e′)
rev-app* ε (nf (app p₁ p₂)) = inj₂ (_ , ε , nawnf←nanf p₁ , ε , p₁ , ε , p₂ , refl)
rev-app* (applam p₂ ◅ rs) p′ = inj₁ (_ , ε , ε , p₂ , rs)
rev-app* (cbv-app₁ r₁ ◅ rs) p′ with rev-app* rs p′
... | inj₁ (_ , rs₁ , rs₂ , p₂′ , rs′)
= inj₁ (_ , r₁ ◅ rs₁ , rs₂ , p₂′ , rs′)
... | inj₂ (_ , rs₁ , p₁′ , rs₁′ , p₁″ , rs₂ , p₂′ , refl)
= inj₂ (_ , r₁ ◅ rs₁ , p₁′ , rs₁′ , p₁″ , rs₂ , p₂′ , refl)
rev-app* (app₁ p₁ r₁ ◅ rs) p′ with rev-app₁* (nawnf-⇒ p₁ r₁) rs p′
... | _ , rs₁ , p₁″ , rs₂ , p₂′ , refl
= inj₂ (_ , ε , p₁ , r₁ ◅ rs₁ , p₁″ , rs₂ , p₂′ , refl)
rev-app* (app₂ₐ r₂ ◅ rs) p′ with rev-app* rs p′
... | inj₁ (_ , rs₁ , rs₂ , p₂′ , rs′)
= inj₁ (_ , rs₁ , r₂ ◅ rs₂ , p₂′ , rs′)
... | inj₂ (_ , rs₁ , p₁′ , rs₁′ , p₁″ , rs₂ , p₂′ , refl)
= inj₂ (_ , rs₁ , p₁′ , rs₁′ , p₁″ , r₂ ◅ rs₂ , p₂′ , refl)
rev-app* (app₂ p₁ r₂ ◅ rs) p′ with rev-app₂* p₁ rs p′
... | _ , rs₂ , p₂′ , refl
= inj₂ (_ , ε , nawnf←nanf p₁ , ε , p₁ , r₂ ◅ rs₂ , p₂′ , refl)
mutual
bs←ss : ∀ {n i} {e : Tm n} {e′} → e ⇒*⟨ i ⟩ e′ → NF e′ → e ⟱ e′
bs←ss ε p′ = refl-⟱ p′
bs←ss (r ◅ rs) p′ = bs←ss′ r rs p′
bs←ss′ : ∀ {n i} {e : Tm n} {e′ e″} → e ⇒ e′ → e′ ⇒*⟨ i ⟩ e″ → NF e″ → e ⟱ e″
bs←ss′ (applam p₂) rs p″ = applam (BS-CBV.refl-⟱ lam)
(refl-⟱ p₂)
(bs←ss rs p″)
bs←ss′ (lam {s = s} r) rs (lam {s = s′} p″) with s ≟ s′
... | no s≢s′ = rs ↯ ¬lam-s⇒*lam-s′ s≢s′
... | yes refl = lam (bs←ss′ r (rev-lam* rs) p″)
bs←ss′ (lam r) rs (nf var) = rs ↯ ¬lam⇒*var
bs←ss′ (lam r) rs (nf (app _ _)) = rs ↯ ¬lam⇒*app
bs←ss′ (cbv-app₁ r₁) rs p″ with rev-app* rs p″
... | inj₁ (_ , rs₁ , rs₂ , p₂′ , rs′) = applam (CBV.Lem-5-3-1.bs←ss′ r₁ rs₁ lam)
(bs←ss rs₂ p₂′)
(bs←ss rs′ p″)
... | inj₂ (_ , rs₁ , p₁′ , rs₁′ , p₁″ , rs₂ , p₂′ , refl) = app (CBV.Lem-5-3-1.bs←ss′ r₁ rs₁ (wnf p₁′))
(na←nawnf p₁′)
(bs←ss rs₁′ (nf p₁″))
(bs←ss rs₂ p₂′)
bs←ss′ (app₁ p₁ r₁) rs p″ with rev-app₁* (nawnf-⇒ p₁ r₁) rs p″
... | _ , rs₁ , p₁′ , rs₂ , p₂′ , refl = app (BS-CBV.refl-⟱′ p₁)
(na←nawnf p₁)
(bs←ss′ r₁ rs₁ (nf p₁′))
(bs←ss rs₂ p₂′)
bs←ss′ (app₂ₐ r₂) rs p″ with rev-app* rs p″
... | inj₁ (_ , rs₁ , rs₂ , p₂′ , rs′) = applam (CBV.Lem-5-3-1.bs←ss rs₁ lam)
(bs←ss′ r₂ rs₂ p₂′)
(bs←ss rs′ p″)
... | inj₂ (_ , rs₁ , p₁′ , rs₁′ , p₁″ , rs₂ , p₂′ , refl) = app (CBV.Lem-5-3-1.bs←ss rs₁ (wnf p₁′))
(na←nawnf p₁′)
(bs←ss rs₁′ (nf p₁″))
(bs←ss′ r₂ rs₂ p₂′)
bs←ss′ (app₂ p₁ r₂) rs p″ with rev-app₂* p₁ rs p″
... | _ , rs₂ , p₂′ , refl = app (BS-CBV.refl-⟱′ (nawnf←nanf p₁))
(na←nanf p₁)
(refl-⟱′ p₁)
(bs←ss′ r₂ rs₂ p₂′)
module Lem-5-5-2 where
open SS-HAO
open BS-HAO
applam* : ∀ {n s} {e₁ : Tm (suc n)} {e₂ : Tm n} → NF e₂ → app (lam s e₁) e₂ ⇒* e₁ [ e₂ ]
applam* p₂ = applam p₂ ◅ ε
lam* : ∀ {n s} {e : Tm (suc n)} {e′} → e ⇒* e′ → lam s e ⇒* lam s e′
lam* = map* lam
cbv-app₁* : ∀ {n} {e₁ e₂ : Tm n} {e₁′} → e₁ SS.CBV.⇒* e₁′ → app e₁ e₂ ⇒* app e₁′ e₂
cbv-app₁* = map* cbv-app₁
app₁* : ∀ {n} {e₁ e₂ : Tm n} {e₁′} → NAWNF e₁ → e₁ ⇒* e₁′ → app e₁ e₂ ⇒* app e₁′ e₂
app₁* p₁ ε = ε
app₁* p₁ (r₁ ◅ rs₁) = app₁ p₁ r₁ ◅ app₁* (nawnf-⇒ p₁ r₁) rs₁
app₂ₐ* : ∀ {n s} {e₁ : Tm (suc n)} {e₂ : Tm n} {e₂′} →
e₂ ⇒* e₂′ →
app (lam s e₁) e₂ ⇒* app (lam s e₁) e₂′
app₂ₐ* = map* app₂ₐ
app₂* : ∀ {n} {e₁ e₂ : Tm n} {e₂′} → NANF e₁ → e₂ ⇒* e₂′ → app e₁ e₂ ⇒* app e₁ e₂′
app₂* p₁ = map* (app₂ p₁)
bs-applam : ∀ {n s} {e₁ e₂ : Tm n} {e₁′ e₂′ e′} →
e₁ SS.CBV.⇒* lam s e₁′ → e₂ ⇒* e₂′ → NF e₂′ → e₁′ [ e₂′ ] ⇒* e′ →
app e₁ e₂ ⇒* e′
bs-applam rs₁ rs₂ p₂′ rs = cbv-app₁* rs₁ ◅◅ app₂ₐ* rs₂ ◅◅ applam* p₂′ ◅◅ rs
bs-lam : ∀ {n s} {e : Tm (suc n)} {e′} → e ⇒* e′ → lam s e ⇒* lam s e′
bs-lam = lam*
bs-app : ∀ {n} {e₁ e₂ : Tm n} {e₁′ e₁″ e₂′} →
e₁ SS.CBV.⇒* e₁′ → NAWNF e₁′ → e₁′ ⇒* e₁″ → NANF e₁″ → e₂ ⇒* e₂′ →
app e₁ e₂ ⇒* app e₁″ e₂′
bs-app rs₁ p₁′ rs₁′ p₁″ rs₂ = cbv-app₁* rs₁ ◅◅ app₁* p₁′ rs₁′ ◅◅ app₂* p₁″ rs₂
ss←bs : ∀ {n} {e : Tm n} {e′} → e ⟱ e′ → e ⇒* e′
ss←bs (applam r₁ r₂ r) = bs-applam (CBV.Lem-5-3-2.ss←bs r₁) (ss←bs r₂) (nf-⟱ r₂) (ss←bs r)
ss←bs var = ε
ss←bs (lam r) = bs-lam (ss←bs r)
ss←bs (app r₁ p₁′ r₁′ r₂) = bs-app (CBV.Lem-5-3-2.ss←bs r₁) p₁″ (ss←bs r₁′) p₁‴ (ss←bs r₂)
where
p₁″ = nawnf←wnf (BS-CBV.wnf-⟱ r₁) p₁′
p₁‴ = nanf←nf (nf-⟱ r₁′) (na←wnf-⟱ (BS-CBV.wnf-⟱ r₁) p₁′ r₁′)
module Thm-5-5-3 where
ss↔bs : ∀ {n} {e : Tm n} {e′} → (e SS.HAO.⇒* e′ × NF e′) ↔ e BS.HAO.⟱ e′
ss↔bs = uncurry Lem-5-5-1.bs←ss , λ r → Lem-5-5-2.ss←bs r , BS-HAO.nf-⟱ r