{-# OPTIONS --rewriting #-}
module Reflect3 where

import DS
import CPS
open import DS-CPS

open import Data.Unit
open import Data.Empty
open import Data.Product
open import Function
open import Relation.Binary.PropositionalEquality

-- substitution lemma
mutual
  lemma-substV : {var : CPS.Ty → Set} → {τ₁ τ₂ : DS.Ty} →
                 {v₁ : (var ∘ cpsT) τ₁ → DS.value[ var ∘ cpsT ] τ₂} →
                 {v  : DS.value[ var ∘ cpsT ] τ₁} →
                 {v₂ : DS.value[ var ∘ cpsT ] τ₂} →
                 (sub : DS.SubstV v₁ v v₂) →
                 CPS.SubstV {var} (λ x → cpsV (v₁ x)) (cpsV v) (cpsV v₂)
  lemma-substV DS.sVar= = CPS.sVar=
  lemma-substV DS.sVar≠ = CPS.sVar≠
  lemma-substV DS.sNum = CPS.sNum
  lemma-substV DS.sBol = CPS.sBol
  lemma-substV (DS.sFun sub) =
    CPS.sFun (λ x → lemma-subst _ (sub x) CPS.sKVar≠ CPS.sGVar≠)
  lemma-substV (DS.sShift id) = CPS.sShift (cps-id-cont-type id)
  lemma-substV DS.sShift0 = CPS.sShift0

  lemma-subst : {var : CPS.Ty → Set} → {τ₁ τ₂ α β : DS.Ty} {σ σα σβ : DS.Mc} →
                {Δ : CPS.Delta} → {Θ : CPS.Theta} →
                {e : (var ∘ cpsT) τ₁ →
                     DS.term[ var ∘ cpsT , τ₂ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β} →
                {k : (var ∘ cpsT) τ₁ →
                     CPS.cont[ var , Δ ] (cpsT τ₂ CPS.⇒ cpsM σα ⇒ cpsT α)} →
                {m : (var ∘ cpsT) τ₁ → CPS.mcont[ var , Θ , cpsM σ ] cpsM σβ} →
                {v : DS.value[ var ∘ cpsT ] τ₁} →
                (ΔΘ : CPS.Delta-Theta Δ Θ) →
                {e' : DS.term[ var ∘ cpsT , τ₂ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β} →
                {k' : CPS.cont[ var , Δ ] (cpsT τ₂ CPS.⇒ cpsM σα ⇒ cpsT α)} →
                {m' : CPS.mcont[ var , Θ , cpsM σ ] cpsM σβ} →
                (sub : DS.Subst e v e') →
                (sub-k : CPS.SubstC k (cpsV v) k') →
                (sub-m : CPS.SubstM m (cpsV v) m') →
                CPS.Subst (λ x → cpsE ΔΘ (e x) (k x) (m x)) (cpsV v)
                          (cpsE ΔΘ e' k' m')
  lemma-subst ΔΘ (DS.sVal sub-v) sub-k sub-m =
    CPS.sVal ΔΘ sub-k (lemma-substV sub-v) sub-m 
  lemma-subst ΔΘ (DS.sNonVal (DS.sApp (DS.sVal sub-v₁)
                                      (DS.sVal sub-v₂))) sub-k sub-m =
    CPS.sApp ΔΘ (lemma-substV sub-v₁) (lemma-substV sub-v₂) sub-k sub-m
  lemma-subst ΔΘ (DS.sNonVal (DS.sApp (DS.sVal sub-v)
                                      (DS.sNonVal sub-q))) sub-k sub-m =
    lemma-subst _ (DS.sNonVal sub-q) (CPS.sKLet (λ x →
      CPS.sApp _ (lemma-substV sub-v) CPS.sVar≠ sub-k CPS.sGVar≠)) sub-m
  lemma-subst ΔΘ (DS.sNonVal (DS.sApp (DS.sNonVal sub-p)
                                      (DS.sVal sub-w))) sub-k sub-m =
     lemma-subst _ (DS.sNonVal sub-p) (CPS.sKLet (λ x →
      CPS.sApp _ CPS.sVar≠ (lemma-substV sub-w) sub-k CPS.sGVar≠)) sub-m
  lemma-subst ΔΘ (DS.sNonVal (DS.sApp (DS.sNonVal sub-p)
                                      (DS.sNonVal sub-q))) sub-k sub-m =
    lemma-subst _ (DS.sNonVal sub-p) (CPS.sKLet (λ x →
      lemma-subst _ (DS.sNonVal sub-q) (CPS.sKLet (λ y →
        CPS.sApp _ CPS.sVar≠ CPS.sVar≠ sub-k CPS.sGVar≠)) CPS.sGVar≠)) sub-m
  lemma-subst ΔΘ (DS.sNonVal (DS.sReset {id = id} sub)) sub-k sub-m =
    lemma-subst _ sub (CPS.sKId (cps-id-cont-type id))
                      (CPS.sGCons ΔΘ sub-k sub-m)
  lemma-subst ΔΘ (DS.sNonVal (DS.sLet sub₁ sub₂)) sub-k sub-m =
    lemma-subst _ sub₂ (CPS.sKLet (λ x →
      lemma-subst _ (sub₁ x) sub-k CPS.sGVar≠)) sub-m


lemma-csubst-type : {var : CPS.Ty → Set} → {τ α β : DS.Ty} →
                    {κ : CPS.CTy} → {σ σα σβ : DS.Mc} →
                    {Δ Δ₁ Δ₂ : CPS.Delta} → {Θ₁ Θ₂ : CPS.Theta} →
                    {sΔΘ : CPS.Delta-Theta-K Δ₁ Θ₁ Δ Δ₂ Θ₂} →
                    (e : DS.term[ var ∘ cpsT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
                    {k : CPS.cont[ var , Δ₁ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)} →
                    {m : CPS.mcont[ var , Θ₁ , cpsM σ ] cpsM σβ} →
                    {c : CPS.cont[ var , Δ ] κ} →
                    {k' : CPS.cont[ var , Δ₂ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)} →
                    {m' : CPS.mcont[ var , Θ₂ , cpsM σ ] cpsM σβ} →
                    (csub-km : CPS.CSubstCM sΔΘ k m c k' m') →
                    Set
lemma-csubst-type e {k} {m} {c} {k'} {m'} (CPS.sKG csub-k) =
  CPS.CSubst (cpsE tt e k m) c (cpsE tt e k' m')
lemma-csubst-type {Δ₁ = Δ₁} {Θ₁ = Θ₁} e {k} {m} {c} {k'} {m'} (CPS.s•DK csub-m) =
  CPS.CSubst (cpsE tt e k m) c (cpsE tt e k' m')

lemma-csubst : {var : CPS.Ty → Set} → {τ α β : DS.Ty} →
               {κ : CPS.CTy} → {σ σα σβ : DS.Mc} →
               {Δ Δ₁ Δ₂ : CPS.Delta} → {Θ₁ Θ₂ : CPS.Theta} →
               {ΔΘ : CPS.Delta-Theta-K Δ₁ Θ₁ Δ Δ₂ Θ₂} →
               (e : DS.term[ var ∘ cpsT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
               {k : CPS.cont[ var , Δ₁ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)} →
               {m : CPS.mcont[ var , Θ₁ , cpsM σ ] cpsM σβ} →
               {c : CPS.cont[ var , Δ ] κ} →
               {k' : CPS.cont[ var , Δ₂ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)} →
               {m' : CPS.mcont[ var , Θ₂ , cpsM σ ] cpsM σβ} →
               (csub-km : CPS.CSubstCM ΔΘ k m c k' m') →
               lemma-csubst-type e csub-km
lemma-csubst (DS.Val v) (CPS.sKG csub-k) = CPS.sVal₁ csub-k
lemma-csubst (DS.Val v) (CPS.s•DK csub-m) = CPS.sVal₂ csub-m
lemma-csubst (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) (CPS.sKG csub-k) =
  CPS.sApp₁ csub-k
lemma-csubst (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) (CPS.s•DK csub-m) =
  CPS.sApp₂ csub-m
lemma-csubst (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) (CPS.sKG csub-k) =
  lemma-csubst (DS.NonVal q) (CPS.sKG (CPS.sKLet₂ (λ y → CPS.sApp₁ csub-k)))
lemma-csubst (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) (CPS.s•DK csub-m) =
  lemma-csubst (DS.NonVal q) (CPS.s•DK csub-m)
lemma-csubst (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) (CPS.sKG csub-k) =
  lemma-csubst (DS.NonVal p) (CPS.sKG (CPS.sKLet₂ (λ x → CPS.sApp₁ csub-k)))
lemma-csubst (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) (CPS.s•DK csub-m) =
  lemma-csubst (DS.NonVal p) (CPS.s•DK csub-m)
lemma-csubst (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) (CPS.sKG csub-k) =
  lemma-csubst (DS.NonVal p) (CPS.sKG (CPS.sKLet₂ (λ x →
    lemma-csubst (DS.NonVal q) (CPS.sKG (CPS.sKLet₂ (λ y →
      CPS.sApp₁ csub-k))))))
lemma-csubst (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) (CPS.s•DK csub-m) =
  lemma-csubst (DS.NonVal p) (CPS.s•DK csub-m)
lemma-csubst (DS.NonVal (DS.Reset id₁ e)) (CPS.sKG csub-k) =
  lemma-csubst e (CPS.s•DK (CPS.sGCons₁ csub-k))
lemma-csubst (DS.NonVal (DS.Reset id₁ e)) (CPS.s•DK csub-m) =
  lemma-csubst e (CPS.s•DK (CPS.sGCons₂ csub-m))
lemma-csubst (DS.NonVal (DS.Let e₁ e₂)) (CPS.sKG csub-k) =
  lemma-csubst e₁ (CPS.sKG (CPS.sKLet₂ (λ x →
    lemma-csubst (e₂ x) ((CPS.sKG csub-k)))))
lemma-csubst (DS.NonVal (DS.Let e₁ e₂)) (CPS.s•DK csub-m) =
  lemma-csubst e₁ (CPS.s•DK csub-m)

lemma-msubst : {var : CPS.Ty → Set} → {τ α β : DS.Ty} → {σ σ' σα σβ : DS.Mc} →
               {Δ : CPS.Delta} → {Θ Θ' : CPS.Theta} → 
               {ΔΘ : CPS.Delta-Theta Δ Θ} →
               {ΔΘ' : CPS.Delta-Theta Δ (Θ CPS.+++ Θ')} →
               (e : DS.term[ var ∘ cpsT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
               {k : CPS.cont[ var , Δ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)} →
               {m : CPS.mcont[ var , Θ , cpsM σ' ] cpsM σβ} →
               {g  : CPS.mcont[ var , Θ' , cpsM σ ] cpsM σ'} →
               {m' : CPS.mcont[ var ,  Θ CPS.+++ Θ' , cpsM σ ] cpsM σβ} →
               (msub-m : CPS.MSubstM m g refl m') →
               CPS.MSubst (cpsE ΔΘ e k m) g
                          (CPS.++-assoc Δ Θ Θ')
                          (cpsE ΔΘ' e k m')
lemma-msubst (DS.Val v) msub-m = CPS.sVal _ _ msub-m
lemma-msubst (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) {k} {m} msub-m =
  CPS.sApp _ _ (cpsV v) (cpsV w) k m msub-m
lemma-msubst (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) msub-m =
  lemma-msubst (DS.NonVal q) msub-m
lemma-msubst (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) msub-m =
  lemma-msubst (DS.NonVal p) msub-m
lemma-msubst (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) msub-m =
  lemma-msubst (DS.NonVal p) msub-m
lemma-msubst (DS.NonVal (DS.Reset id e)) {k} {m} {g} msub-m =
  lemma-msubst e (CPS.mGCons _ _ msub-m)
lemma-msubst (DS.NonVal (DS.Let e₁ e₂)) msub-m = lemma-msubst e₁ msub-m

-- lemma
correctCM : {var : CPS.Ty → Set} → {τ α β : DS.Ty} {σ σα σβ : DS.Mc} →
           {Δ : CPS.Delta} → {Θ : CPS.Theta} →
           (ΔΘ : CPS.Delta-Theta Δ Θ) →
           (M : DS.term[ var ∘ cpsT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
           {K K' : CPS.cont[ var , Δ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)} →
           {G G' : CPS.mcont[ var , Θ , cpsM σ ] cpsM σβ} →
           CPS.ReduceCM {var} K G K' G' →
           CPS.Reduce {var} (cpsE ΔΘ M K G) (cpsE ΔΘ M K' G')
correctCM ΔΘ (DS.Val v) (CPS.RedC red-k) = CPS.RVal₁ _ red-k
correctCM ΔΘ (DS.Val v) (CPS.RedM red-m) = CPS.RVal₃ _ red-m
correctCM ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) (CPS.RedC red-k) =
  CPS.RApp₃ ΔΘ red-k
correctCM ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) (CPS.RedM red-m) =
  CPS.RApp₄ ΔΘ red-m
correctCM ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) (CPS.RedC red-k) =
  correctCM _ (DS.NonVal q) (CPS.RedC(CPS.RKLet λ y → CPS.RApp₃ _ red-k))
correctCM ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) (CPS.RedM red-m) =
  correctCM _ (DS.NonVal q) (CPS.RedM red-m) 
correctCM ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) (CPS.RedC red-k) =
  correctCM _ (DS.NonVal p) (CPS.RedC(CPS.RKLet λ x → CPS.RApp₃ _ red-k))
correctCM ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) (CPS.RedM red-m) =
 correctCM _ (DS.NonVal p) (CPS.RedM red-m) 
correctCM ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) (CPS.RedC red-k) =
  correctCM _ (DS.NonVal p) (CPS.RedC(CPS.RKLet λ x →
    correctCM _ (DS.NonVal q) (CPS.RedC(CPS.RKLet λ y → CPS.RApp₃ _ red-k)) ))
correctCM ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) (CPS.RedM red-m) =
  correctCM _ (DS.NonVal p) (CPS.RedM red-m) 
correctCM ΔΘ (DS.NonVal (DS.Reset id₁ e)) (CPS.RedC red-k) =
  correctCM _ e (CPS.RedM (CPS.RGCons₁ _ red-k))
correctCM ΔΘ (DS.NonVal (DS.Reset id₁ e)) (CPS.RedM red-m) =
  correctCM _ e (CPS.RedM (CPS.RGCons₂ _ red-m))
correctCM ΔΘ (DS.NonVal (DS.Let e₁ e₂)) (CPS.RedC red-k) =
  correctCM _ e₁ (CPS.RedC
                  (CPS.RKLet (λ x → correctCM _ (e₂ x) (CPS.RedC red-k))))
correctCM ΔΘ (DS.NonVal (DS.Let e₁ e₂)) (CPS.RedM red-m) =
  correctCM _ e₁ (CPS.RedM red-m)


contExist : {var : CPS.Ty → Set} {Δ : CPS.Delta}
            {τ τ₄ τ₅ α : DS.Ty} →
            {σ₅ σα : DS.Mc} →
            (j : DS.pcontext[ var ∘ cpsT , τ₄ DS.▷⟨ σ₅ ⟩ τ₅ , τ ]⟨ σα ⟩ α) →
            (k : CPS.cont[ var , Δ ] (cpsT τ₄ CPS.⇒ cpsM σ₅ ⇒ cpsT τ₅)) →
            Σ[ j' ∈ CPS.cont[ var  , Δ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α) ]
            ({β : DS.Ty}{σ σβ : DS.Mc}{Θ : CPS.Theta}
             (p : DS.nonvalue[ var ∘ cpsT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β ) →
             (ΔΘ : CPS.Delta-Theta Δ Θ) →
             (m : CPS.mcont[ var , Θ , cpsM σ ] cpsM σβ) →
             cpsE ΔΘ (DS.plug j (DS.NonVal p)) k m ≡ cpsE ΔΘ (DS.NonVal p) j' m)
            ×
            ({σ' : DS.Mc}{Θ' : CPS.Theta}
             (v : DS.value[ var ∘ cpsT ] τ) →
             (ΔΘ' : CPS.Delta-Theta Δ Θ') →
             (m' : CPS.mcont[ var , Θ' , cpsM σ' ] cpsM σα) →
             CPS.Reduce
               (CPS.Val ΔΘ' j' (cpsV v) m')
               (cpsE ΔΘ' (DS.plug j (DS.Val v)) k m'))
contExist DS.Hole k = k , (λ p ΔΘ m → refl) , λ v ΔΘ' m' → CPS.RId
contExist (DS.App₁ j (DS.Val v)) k with contExist j k
... | j' , eq , red = _ , (λ p ΔΘ m → eq (DS.App (DS.NonVal p) (DS.Val v)) ΔΘ m) ,
  λ v' ΔΘ' m' → begin
  CPS.Val ΔΘ'
    (CPS.KLet (λ x → CPS.App tt (CPS.Var x) (cpsV v) j' CPS.GVar))
    (cpsV v') m'
  ⟶⟨ CPS.RBetaLet ΔΘ'
       (CPS.sApp tt CPS.sVar= (CPS.SubstV≠ (cpsV v)) (CPS.SubstC≠ j') CPS.sGVar≠)
       (CPS.sApp ΔΘ' tt (cpsV v') (cpsV v) j' CPS.GVar CPS.mGVar=) ⟩
  cpsE ΔΘ' (DS.NonVal (DS.App (DS.Val v') (DS.Val v))) j' m'
  ≡⟨ sym (eq (DS.App (DS.Val v') (DS.Val v)) ΔΘ' m') ⟩
  cpsE ΔΘ' (DS.plug j (DS.NonVal (DS.App (DS.Val v') (DS.Val v)))) k m'
  ∎
  where open CPS.Reasoning
contExist (DS.App₁ j (DS.NonVal p)) k with contExist j k
... | j' , eq , red = _ ,
  (λ p' ΔΘ m → eq (DS.App (DS.NonVal p') (DS.NonVal p)) ΔΘ m) ,
  λ v ΔΘ' m' → begin
  CPS.Val ΔΘ'
    (CPS.KLet
      (λ x →
         cpsE tt (DS.NonVal p)
         (CPS.KLet (λ y → CPS.App tt (CPS.Var x) (CPS.Var y) j' CPS.GVar))
         CPS.GVar))
    (cpsV v) m'
  ⟶⟨ CPS.RBetaLet ΔΘ'
       (lemma-subst tt (DS.Subst≠ (DS.NonVal p))
         (CPS.sKLet λ x →
           CPS.sApp tt CPS.sVar= CPS.sVar≠
                       (CPS.SubstC≠ j') (CPS.SubstM≠ CPS.GVar))
         (CPS.sGVar≠))
       (lemma-msubst (DS.NonVal p) CPS.mGVar=) ⟩
  cpsE ΔΘ' (DS.NonVal (DS.App (DS.Val v) (DS.NonVal p))) j' m'
  ≡⟨ sym (eq (DS.App (DS.Val v) (DS.NonVal p)) ΔΘ' m') ⟩
  cpsE ΔΘ' (DS.plug j (DS.NonVal (DS.App (DS.Val v) (DS.NonVal p)))) k m'
  ∎
  where open CPS.Reasoning
contExist (DS.App₂ v j) k with contExist j k
... | j' , eq , red = _ ,
  (λ p ΔΘ m → eq (DS.App (DS.Val v) (DS.NonVal p)) ΔΘ m) ,
  λ v' ΔΘ' m' → begin
  CPS.Val ΔΘ'
    (CPS.KLet (λ y → CPS.App tt (cpsV v) (CPS.Var y) j' CPS.GVar))
    (cpsV v') m'
  ⟶⟨ CPS.RBetaLet ΔΘ'
       (CPS.sApp tt (CPS.SubstV≠ (cpsV v)) CPS.sVar=
                    (CPS.SubstC≠ j') (CPS.SubstM≠ CPS.GVar))
       (CPS.sApp ΔΘ' tt (cpsV v) (cpsV v') j' CPS.GVar CPS.mGVar=) ⟩
  cpsE ΔΘ' (DS.NonVal (DS.App (DS.Val v) (DS.Val v'))) j' m'
  ≡⟨ sym (eq (DS.App (DS.Val v) (DS.Val v')) ΔΘ' m') ⟩
  cpsE ΔΘ' (DS.plug j (DS.NonVal (DS.App (DS.Val v) (DS.Val v')))) k m'
  ∎
  where open CPS.Reasoning
contExist (DS.Let j f) k with contExist j k
... | j' , eq , red = _ ,
  (λ p ΔΘ m → eq (DS.Let (DS.NonVal p) f) ΔΘ m) ,
  λ v ΔΘ' m' → begin
  CPS.Val ΔΘ' (CPS.KLet (λ x → cpsE tt (f x) j' CPS.GVar)) (cpsV v) m'
  ≡⟨ sym (eq (DS.Let (DS.Val v) f) ΔΘ' m') ⟩
  cpsE ΔΘ' (DS.plug j (DS.NonVal (DS.Let (DS.Val v) f))) k m'
  ∎
  where open CPS.Reasoning

redShift : {var : CPS.Ty → Set}
           {τ τ₁ τ₂ τ₃ τ₄ τ₅ α α₁ β γ γ' : DS.Ty}
           {σ σ₁ σ₂ σ₅ σα σβ σid : DS.Mc} →
           {Δ : CPS.Delta} → {Θ : CPS.Theta} →
           (ΔΘ : CPS.Delta-Theta Δ Θ) →
           (id₁ : DS.id-cont-type γ σid γ') →
           (id₂ : DS.id-cont-type τ₄ σ₅ τ₅) →
           (w   : DS.value[ var ∘ cpsT ]
                    ((τ₁ DS.⇒ τ₂ ⟨ σ₁ ⟩ τ₃ ⟨ σ₂ ⟩ α₁) DS.⇒ γ ⟨ σid ⟩ γ' ⟨
                      τ DS.⇨⟨ σα ⟩ α ∷ σβ ⟩ β)) →
           (j   : DS.pcontext[ var ∘ cpsT , τ₄ DS.▷⟨ σ₅ ⟩ τ₅ , τ₁ ]⟨
                    τ₂ DS.⇨⟨ σ₁ ⟩ τ₃ ∷ σ₂ ⟩ α₁) →
           {K   : CPS.cont[ var , Δ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)} →
           {G   : CPS.mcont[ var , Θ , cpsM σ ] cpsM σβ } →
           CPS.Reduce
             (cpsE tt
               (DS.plug j
                 (DS.NonVal (DS.App (DS.Val (DS.Shift id₁)) (DS.Val w))))
               (CPS.KId (cps-id-cont-type id₂)) (CPS.GCons ΔΘ K G))
             (CPS.App tt (cpsV w)
               (CPS.Fun
                 (λ x → cpsE tt (DS.plug j (DS.Val (DS.Var x)))
                                (CPS.KId (cps-id-cont-type id₂))
                                (CPS.GCons tt CPS.KVar CPS.GVar)))
               (CPS.KId (cps-id-cont-type id₁)) (CPS.GCons ΔΘ K G))
redShift {var} ΔΘ id₁ id₂ w j {K} {G} with contExist {var} j
                                           (CPS.KId (cps-id-cont-type id₂))
... | j' , eq , red = begin
  cpsE tt
    (DS.plug j
      (DS.NonVal (DS.App (DS.Val (DS.Shift id₁)) (DS.Val w))))
    (CPS.KId (cps-id-cont-type id₂)) (CPS.GCons ΔΘ K G)
  ≡⟨ eq (DS.App (DS.Val (DS.Shift id₁)) (DS.Val w)) _ (CPS.GCons ΔΘ K G) ⟩
  cpsE tt
    (DS.NonVal (DS.App (DS.Val (DS.Shift id₁)) (DS.Val w)))
    j' (CPS.GCons ΔΘ K G)
  ⟶⟨ CPS.RShift (cps-id-cont-type id₁) (cps-id-cont-type id₂) ⟩ 
  CPS.App tt (cpsV w)
    (CPS.Fun (λ y → CPS.Val tt j' (CPS.Var y)
                  (CPS.GCons tt CPS.KVar CPS.GVar)))
    (CPS.KId (cps-id-cont-type id₁)) (CPS.GCons ΔΘ K G)
  ⟶⟨ CPS.RApp₂ tt
       (CPS.RFun (λ x → red (DS.Var x) _ (CPS.GCons tt CPS.KVar CPS.GVar))) ⟩
  CPS.App tt (cpsV w)
    (CPS.Fun
      (λ x → cpsE tt (DS.plug j (DS.Val (DS.Var x)))
                     (CPS.KId (cps-id-cont-type id₂))
                     (CPS.GCons tt CPS.KVar CPS.GVar)))
    (CPS.KId (cps-id-cont-type id₁)) (CPS.GCons ΔΘ K G)
  ∎
  where open CPS.Reasoning

redShift0 : {var : CPS.Ty → Set } → {Δ : CPS.Delta} {Θ : CPS.Theta} →
            {τ τ₁ τ₂ τ₃ τ₄ τ₅ α α₁ β : DS.Ty} →
            {σ₁ σ₂ σ₅ σ σα σβ : DS.Mc} →
            (ΔΘ : CPS.Delta-Theta Δ Θ) →
            (id  : DS.id-cont-type τ₄ σ₅ τ₅) →
            (v   : DS.value[ var ∘ cpsT ]
                     ((τ₁ DS.⇒ τ₂ ⟨ σ₁ ⟩ τ₃ ⟨ σ₂ ⟩ α₁) DS.⇒
                          τ ⟨ σα ⟩ α ⟨ σβ ⟩ β)) →
            (j   : DS.pcontext[ var ∘ cpsT , τ₄ DS.▷⟨ σ₅ ⟩ τ₅ , τ₁ ]⟨
                     τ₂ DS.⇨⟨ σ₁ ⟩ τ₃ ∷ σ₂ ⟩ α₁) →
            {K   : CPS.cont[ var , Δ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)} →
            {G   : CPS.mcont[ var , Θ , cpsM σ ] cpsM σβ } →
            CPS.Reduce
              (cpsE tt
                (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v))))
                  (CPS.KId (cps-id-cont-type id)) (CPS.GCons ΔΘ K G))
              (CPS.App ΔΘ (cpsV v)
                (CPS.Fun
                  (λ x →
                     cpsE tt (DS.plug j (DS.Val (DS.Var x)))
                     (CPS.KId (cps-id-cont-type id))
                     (CPS.GCons tt CPS.KVar CPS.GVar)))
                K G)
redShift0 {var} {Θ = Θ} ΔΘ id v j {K} {G} with contExist {var} j
                                           (CPS.KId (cps-id-cont-type id))
... | j' , eq , red = begin
  cpsE tt
    (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v))))
    (CPS.KId (cps-id-cont-type id)) (CPS.GCons ΔΘ K G)
  ≡⟨ eq (DS.App (DS.Val DS.Shift0) (DS.Val v)) tt (CPS.GCons ΔΘ K G) ⟩
  cpsE tt
    (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v)))
    j' (CPS.GCons ΔΘ K G)
  ⟶⟨ CPS.RShift0 ΔΘ (cps-id-cont-type id) ⟩
  CPS.App ΔΘ (cpsV v)
    (CPS.Fun
      (λ y →
        CPS.Val tt j' (CPS.Var y) (CPS.GCons tt CPS.KVar CPS.GVar)))
    K G
  ⟶⟨ CPS.RApp₂ ΔΘ
       (CPS.RFun (λ x → red (DS.Var x) tt (CPS.GCons tt CPS.KVar CPS.GVar))) ⟩
  CPS.App ΔΘ (cpsV v)
    (CPS.Fun
      (λ x →
         cpsE tt (DS.plug j (DS.Val (DS.Var x)))
         (CPS.KId (cps-id-cont-type id)) (CPS.GCons tt CPS.KVar CPS.GVar)))
    K G
  ∎
  where open CPS.Reasoning


-- main theorem: DS の項 M, N に対して、M → N ならば、M* → N*
mutual
  -- DS の値 V, W に対して、V → W ならば、V† → W†
  correctV : {var : CPS.Ty → Set} → {τ β : DS.Ty} {σβ : DS.Mc} →
             {V W : DS.value[ var ∘ cpsT ] τ} →
             DS.Reduce {β = β} {σβ = σβ} (DS.Val V) (DS.Val W) →
             CPS.ReduceV {var} (cpsV V) (cpsV W)
  correctV (DS.REtaV _) = CPS.REtaV 
  correctV (DS.RFun red) = CPS.RFun (λ x → correctE _ (red x))
  correctV DS.RId = CPS.RId
  correctV (DS.RTrans {e₂ = DS.Val v} red₁ red₂) =
    CPS.RTrans (correctV red₁) (correctV red₂)
  correctV (DS.RTrans {e₂ = DS.NonVal p} red₁ red₂) with DS.reduceVal red₁
  ... | ()

  -- DS の項 M, N 任意のCPS項の継続 K, メタ継続G に対して、M→N ならば M:K:G → N:K:G
  correctE : {var : CPS.Ty → Set} → {τ α β : DS.Ty} {σ σα σβ : DS.Mc} →
             {Δ : CPS.Delta} → {Θ : CPS.Theta} →
             {M N : DS.term[ var ∘ cpsT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β} →
             (ΔΘ : CPS.Delta-Theta Δ Θ) →
             {K : CPS.cont[ var , Δ ] (cpsT τ CPS.⇒ cpsM σα ⇒ cpsT α)} →
             {G : CPS.mcont[ var , Θ , cpsM σ ] cpsM σβ} →
             DS.Reduce {β = β} {σβ = σβ} M N →
             CPS.Reduce {var} (cpsE ΔΘ M K G) (cpsE ΔΘ N K G)
  correctE ΔΘ (DS.RBetaV e₁ v₂ e₁' sub) =
    CPS.RBetaV ΔΘ (lemma-subst _ sub CPS.sKVar≠ CPS.sGVar≠)
                  (lemma-csubst e₁' (CPS.sKG (CPS.sKVar=)))
                  (lemma-msubst e₁' CPS.mGVar=)
  correctE ΔΘ (DS.REtaV v) = CPS.RVal₂ ΔΘ CPS.REtaV
  correctE ΔΘ (DS.RBetaLet v₁ e₂ e₂' sub) =
    CPS.RBetaLet ΔΘ (lemma-subst _ sub (CPS.SubstC≠ _) CPS.sGVar≠)
                    (lemma-msubst e₂' CPS.mGVar=)
  correctE ΔΘ (DS.REtaLet e) = correctCM _ e (CPS.RedC CPS.REtaLet)
  correctE ΔΘ (DS.RAssoc e₁ e₂ e₃) = CPS.RId
  correctE ΔΘ (DS.RLet1 e₁ (DS.Val v)) = CPS.RId
  correctE ΔΘ (DS.RLet1 e₁ (DS.NonVal p)) = CPS.RId
  correctE ΔΘ (DS.RLet2 e₂) = CPS.RId
  correctE ΔΘ (DS.RShift id₁ id₂ v j) = redShift ΔΘ id₁ id₂ v j
  correctE ΔΘ (DS.RShift0 id v j) = redShift0 ΔΘ id v j
  correctE ΔΘ (DS.RReset v) = CPS.RReset ΔΘ
  correctE ΔΘ (DS.RFun red) =
    CPS.RVal₂ ΔΘ (CPS.RFun (λ x → correctE _ (red x)))
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.Val v} {DS.Val v'} {DS.Val w} red) =
    CPS.RApp₁ _ (correctV red)
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.Val v} {DS.Val v'} {DS.NonVal q} red) = 
    correctCM _ (DS.NonVal q) (CPS.RedC (CPS.RKLet (λ x → CPS.RApp₁ _ (correctV red))))
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.Val v}
                         {DS.NonVal p} {DS.Val w} red) with DS.reduceVal red
  ... | ()
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.Val v}
                         {DS.NonVal p} {DS.NonVal q} red) with DS.reduceVal red
  ... | ()
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.NonVal p} {DS.Val v} {DS.Val w} red) =
    CPS.RTrans (correctE _ red)
               (CPS.RBetaLet _ (CPS.sApp tt CPS.sVar= (CPS.SubstV≠ (cpsV w))
                                            (CPS.SubstC≠ _) (CPS.SubstM≠ _))
                               (CPS.sApp _ tt (cpsV v) (cpsV w) _ _ CPS.mGVar=))
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.NonVal p} {DS.Val v} {DS.NonVal q} red) =
    CPS.RTrans (correctE _ red)
               (CPS.RBetaLet _ (lemma-subst _ (DS.Subst≠ (DS.NonVal q))
                                 (CPS.sKLet (λ x →
                                   CPS.sApp tt CPS.sVar= CPS.sVar≠
                                            (CPS.SubstC≠ _) (CPS.SubstM≠ _)))
                                 (CPS.SubstM≠ _))
                               (lemma-msubst (DS.NonVal q) CPS.mGVar=))
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.NonVal p} {DS.NonVal p'} {DS.Val w} red) =
    correctE _ red
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.NonVal p} {DS.NonVal p'} {DS.NonVal q} red) =
    correctE _ red
  correctE ΔΘ (DS.RApp₂ {e₂ = DS.Val w} {DS.Val w'} red) = CPS.RApp₂ _ (correctV red)
  correctE ΔΘ (DS.RApp₂ {e₂ = DS.Val w} {DS.NonVal q} red) with DS.reduceVal red
  ... | ()
  correctE ΔΘ (DS.RApp₂ {v₁ = v₁} {e₂ = DS.NonVal q} {DS.Val w} red) =
    CPS.RTrans (correctE _ red)
               (CPS.RBetaLet _ (CPS.sApp tt (lemma-substV (DS.SubstV≠ _))
                                CPS.sVar= (CPS.SubstC≠ _) (CPS.SubstM≠ _))
                             (CPS.sApp _ tt (cpsV v₁) (cpsV w) _ _ CPS.mGVar=))
  correctE ΔΘ (DS.RApp₂ {e₂ = DS.NonVal q} {DS.NonVal q'} red) = correctE _ red
  correctE ΔΘ (DS.RLet₁ red) = correctE _ red
  correctE ΔΘ (DS.RLet₂ {e₁ = e₁} red) =
    correctCM _ e₁ (CPS.RedC (CPS.RKLet (λ x → correctE _ (red x))))
  correctE ΔΘ (DS.RReset₁ id red) = correctE _ red
  correctE ΔΘ DS.RId = CPS.RId
  correctE ΔΘ (DS.RTrans red₁ red₂) =
    CPS.RTrans (correctE _ red₁) (correctE _ red₂)