{-# OPTIONS --rewriting #-}

module Reflect3Direct 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 : Set} →
                 {v₁ : var → DS.value[ var ]} →
                 {v  : DS.value[ var ]} →
                 {v₂ : DS.value[ var ]} →
                 (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 = CPS.sShift
  lemma-substV DS.sShift0 = CPS.sShift0

  lemma-subst : {var : Set} →
                {Δ : CPS.Delta} → {Θ : CPS.Theta} →
                {e : var → DS.term[ var ]} →
                {k : var → CPS.cont[ var , Δ ]} →
                {m : var → CPS.mcont[ var , Θ ]} →
                {v : DS.value[ var ]} →
                (ΔΘ : CPS.Delta-Theta Δ Θ) →
                {e' : DS.term[ var ]} →
                {k' : CPS.cont[ var , Δ ]} →
                {m' : CPS.mcont[ var , Θ ]} →
                (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 sub)) sub-k sub-m =
    lemma-subst _ sub CPS.sKId
                      (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 : Set} →
                    {Δ Δ₁ Δ₂ : CPS.Delta} → {Θ₁ Θ₂ : CPS.Theta} →
                    {sΔΘ : CPS.Delta-Theta-K Δ₁ Θ₁ Δ Δ₂ Θ₂} →
                    (e : DS.term[ var ]) →
                    {k : CPS.cont[ var , Δ₁ ]} →
                    {m : CPS.mcont[ var , Θ₁ ]} →
                    {c : CPS.cont[ var , Δ ]} →
                    {k' : CPS.cont[ var , Δ₂ ]} →
                    {m' : CPS.mcont[ var , Θ₂ ]} →
                    (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 : Set} →
               {Δ Δ₁ Δ₂ : CPS.Delta} → {Θ₁ Θ₂ : CPS.Theta} →
               {ΔΘ : CPS.Delta-Theta-K Δ₁ Θ₁ Δ Δ₂ Θ₂} →
               (e : DS.term[ var ]) →
               {k : CPS.cont[ var , Δ₁ ]} →
               {m : CPS.mcont[ var , Θ₁ ]} →
               {c : CPS.cont[ var , Δ ]} →
               {k' : CPS.cont[ var , Δ₂ ]} →
               {m' : CPS.mcont[ var , Θ₂ ]} →
               (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 e)) (CPS.sKG csub-k) =
  lemma-csubst e (CPS.s•DK (CPS.sGCons₁ csub-k))
lemma-csubst (DS.NonVal (DS.Reset 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 : Set} → {Δ : CPS.Delta} → {Θ Θ' : CPS.Theta} → 
               {ΔΘ : CPS.Delta-Theta Δ Θ} →
               {ΔΘ' : CPS.Delta-Theta Δ (Θ CPS.+++ Θ')} →
               (e : DS.term[ var ]) →
               {k : CPS.cont[ var , Δ ]} →
               {m : CPS.mcont[ var , Θ ]} →
               {g  : CPS.mcont[ var , Θ' ]} →
               {m' : CPS.mcont[ var ,  Θ CPS.+++ Θ' ]} →
               (msub-m : CPS.MSubstM m g refl m') →
               CPS.MSubst (cpsE ΔΘ e k m) g
                          refl --(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 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 : Set} → {Δ : CPS.Delta} → {Θ : CPS.Theta} →
           (ΔΘ : CPS.Delta-Theta Δ Θ) →
           (M : DS.term[ var ]) →
           {K K' : CPS.cont[ var , Δ ]} →
           {G G' : CPS.mcont[ var , Θ ]} →
           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 e)) (CPS.RedC red-k) =
  correctCM _ e (CPS.RedM (CPS.RGCons₁ _ red-k))
correctCM ΔΘ (DS.NonVal (DS.Reset 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 : Set} {Δ : CPS.Delta}
            (j : DS.pcontext[ var ]) →
            (k : CPS.cont[ var , Δ ]) →
            Σ[ j' ∈ CPS.cont[ var  , Δ ] ]
            ({Θ : CPS.Theta}
             (p : DS.nonvalue[ var ]) →
             (ΔΘ : CPS.Delta-Theta Δ Θ) →
             (m : CPS.mcont[ var , Θ ]) →
             cpsE ΔΘ (DS.plug j (DS.NonVal p)) k m ≡ cpsE ΔΘ (DS.NonVal p) j' m)
            ×
            ({Θ' : CPS.Theta}
             (v : DS.value[ var ]) →
             (ΔΘ' : CPS.Delta-Theta Δ Θ') →
             (m' : CPS.mcont[ var , Θ' ]) →
             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 : Set} → {Δ : CPS.Delta} → {Θ : CPS.Theta} →
           (ΔΘ : CPS.Delta-Theta Δ Θ) →
           (w   : DS.value[ var ]) →
           (j   : DS.pcontext[ var ]) →
           {K   : CPS.cont[ var , Δ ]} →
           {G   : CPS.mcont[ var , Θ ]} →
           CPS.Reduce
             (cpsE tt
               (DS.plug j
                 (DS.NonVal (DS.App (DS.Val DS.Shift) (DS.Val w))))
               CPS.KId (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.GCons tt CPS.KVar CPS.GVar)))
               CPS.KId (CPS.GCons ΔΘ K G))
redShift {var} ΔΘ w j {K} {G} with contExist {var} j CPS.KId
... | j' , eq , red = begin
  cpsE tt
    (DS.plug j
      (DS.NonVal (DS.App (DS.Val DS.Shift) (DS.Val w))))
    CPS.KId (CPS.GCons ΔΘ K G)
  ≡⟨ eq (DS.App (DS.Val DS.Shift) (DS.Val w)) _ (CPS.GCons ΔΘ K G) ⟩
  cpsE tt
    (DS.NonVal (DS.App (DS.Val DS.Shift) (DS.Val w)))
    j' (CPS.GCons ΔΘ K G)
  ⟶⟨ CPS.RShift ⟩ 
  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.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.GCons tt CPS.KVar CPS.GVar)))
    CPS.KId (CPS.GCons ΔΘ K G)
  ∎
  where open CPS.Reasoning

redShift0 : {var : Set } → {Δ : CPS.Delta} {Θ : CPS.Theta} →
            (ΔΘ : CPS.Delta-Theta Δ Θ) →
            (v   : DS.value[ var ]) →
            (j   : DS.pcontext[ var ]) →
            {K   : CPS.cont[ var , Δ ]} →
            {G   : CPS.mcont[ var , Θ ]} →
            CPS.Reduce
              (cpsE tt
                (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v))))
                  CPS.KId (CPS.GCons ΔΘ K G))
              (CPS.App ΔΘ (cpsV v)
                (CPS.Fun
                  (λ x →
                     cpsE tt (DS.plug j (DS.Val (DS.Var x)))
                     CPS.KId
                     (CPS.GCons tt CPS.KVar CPS.GVar)))
                K G)
redShift0 {var} {Θ = Θ} ΔΘ v j {K} {G} with contExist {var} j CPS.KId
... | j' , eq , red = begin
  cpsE tt
    (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v))))
    CPS.KId (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.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.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 : Set} →
             {V W : DS.value[ var ]} →
             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 : Set} → {Δ : CPS.Delta} → {Θ : CPS.Theta} →
             {M N : DS.term[ var ]} →
             (ΔΘ : CPS.Delta-Theta Δ Θ) →
             {K : CPS.cont[ var , Δ ]} →
             {G : CPS.mcont[ var , Θ ]} →
             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 v j) = redShift ΔΘ v j
  correctE ΔΘ (DS.RShift0 v j) = redShift0 ΔΘ 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₁ red) = correctE _ red
  correctE ΔΘ DS.RId = CPS.RId
  correctE ΔΘ (DS.RTrans red₁ red₂) =
    CPS.RTrans (correctE _ red₁) (correctE _ red₂)