GentzenNormalForm3.agda

module BasicIPC.Syntax.GentzenNormalForm3 where

open import BasicIPC.Syntax.GentzenNormalForm public


data Re {Γ} : ∀ {A} → Γ ⊢ A → Γ ⊢ A → Set where
  conglamʳᵉ  : ∀ {A B} {t t′ : Γ , A ⊢ B} →
               Re t t′ → Re (lam t) (lam t′)

  congappʳᵉ  : ∀ {A B} {t t′ : Γ ⊢ A ▻ B} {u u′ : Γ ⊢ A} →
               Re t t′ → Re u u′ → Re (app t u) (app t′ u′)

  congpairʳᵉ : ∀ {A B} {t t′ : Γ ⊢ A} {u u′ : Γ ⊢ B} →
               Re t t′ → Re u u′ → Re (pair t u) (pair t′ u′)

  congfstʳᵉ  : ∀ {A B} {t t′ : Γ ⊢ A ∧ B} →
               Re t t′ → Re (fst t) (fst t′)

  congsndʳᵉ  : ∀ {A B} {t t′ : Γ ⊢ A ∧ B} →
               Re t t′ → Re (snd t) (snd t′)

  beta▻ʳᵉ    : ∀ {A B} {t : Γ , A ⊢ B} {u : Γ ⊢ A} →
               Re (app (lam t) u) ([ top ≔ u ] t)

  beta∧₁ʳᵉ   : ∀ {A B} {t : Γ ⊢ A} {u : Γ ⊢ B} →
               Re (fst (pair t u)) t

  beta∧₂ʳᵉ   : ∀ {A B} {t : Γ ⊢ A} {u : Γ ⊢ B} →
               Re (snd (pair t u)) u


data Nf {Γ} : ∀ {A} → Γ ⊢ A → Set where
  lamⁿᶠ  : ∀ {A B} {t : Γ , A ⊢ B} →
           Nf t → Nf (lam t)

  pairⁿᶠ : ∀ {A B} {t : Γ ⊢ A} {u : Γ ⊢ B} →
           Nf t → Nf u → Nf (pair t u)

  unitⁿᶠ : Nf unit


data Ch {Γ A} (t : Γ ⊢ A) : Γ ⊢ A → Set where
  done : Nf t → Ch t t

  step : ∀ {t′ t″ : Γ ⊢ A} {{_ : t ≢ t″}} →
         Ch t t′ → Re t′ t″ → Ch t t″


lamᶜʰ : ∀ {Γ A B} {t : Γ , A ⊢ B} → Nf t → Ch (lam t) (lam t)
lamᶜʰ ν = done (lamⁿᶠ ν)

unlamᶜʰ : ∀ {Γ A B} {t : Γ , A ⊢ B} → Ch (lam t) (lam t) → Nf t
unlamᶜʰ (done (lamⁿᶠ ν))    = ν
unlamᶜʰ (step {{s≢s′}} χ ρ) = refl ↯ s≢s′


pairᶜʰ : ∀ {Γ A B} {t : Γ ⊢ A} {u : Γ ⊢ B} → Nf t → Nf u → Ch (pair t u) (pair t u)
pairᶜʰ νₜ νᵤ = done (pairⁿᶠ νₜ νᵤ)

unpairᶜʰ₁ : ∀ {Γ A B} {t : Γ ⊢ A} {u : Γ ⊢ B} → Ch (pair t u) (pair t u) → Nf t
unpairᶜʰ₁ (done (pairⁿᶠ νₜ νᵤ)) = νₜ
unpairᶜʰ₁ (step {{s≢s′}} χ ρ)   = refl ↯ s≢s′

unpairᶜʰ₂ : ∀ {Γ A B} {t : Γ ⊢ A} {u : Γ ⊢ B} → Ch (pair t u) (pair t u) → Nf u
unpairᶜʰ₂ (done (pairⁿᶠ νₜ νᵤ)) = νᵤ
unpairᶜʰ₂ (step {{s≢s′}} χ ρ)   = refl ↯ s≢s′


record Sh {Γ A} (t : Γ ⊢ A) : Set where
  constructor sh
  field
    {t′} : Γ ⊢ A
    ch   : Ch t t′

open Sh public


lamˢʰ : ∀ {Γ A B} {t : Γ , A ⊢ B} → Sh t → Sh (lam t)
lamˢʰ (sh (done ν))            = sh (done (lamⁿᶠ ν))
lamˢʰ (sh (step {{t≢t′}} χ ρ)) = sh {!!}

unlamˢʰ : ∀ {Γ A B} {t : Γ , A ⊢ B} → Sh (lam t) → Sh t
unlamˢʰ σ = {!!}


sh? : ∀ {Γ A} → (t : Γ ⊢ A) → Dec (Sh t)
sh? (var i) = {!!}
sh? (lam t) = mapDec {!!} {!!} (sh? t)
sh? (app t u) = {!!}
sh? (pair t u) = {!!}
sh? (fst t) = {!!}
sh? (snd t) = {!!}
sh? unit = yes (sh (done unitⁿᶠ))