{-# OPTIONS --rewriting #-}

module Reflect3a where

import DS
import DSK
open import DS-DSK

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

-- substitution lemma
mutual
  -- v₁[x:=v] ≡ v₂ 
  lemma-SubstV : {var : Set} →
                 {v₁ : var → DS.value[ var ]} →
                 {v  : DS.value[ var ]} →
                 {v₂ : DS.value[ var ]} →
                 DS.SubstV v₁ v v₂ →
                 DSK.SubstV {var} (λ x → knV (v₁ x)) (knV v) (knV v₂)
  lemma-SubstV DS.sVar= = DSK.sVar=
  lemma-SubstV DS.sVar≠ = DSK.sVar≠
  lemma-SubstV DS.sNum = DSK.sNum
  lemma-SubstV DS.sBol = DSK.sBol
  lemma-SubstV (DS.sFun sub) =
    DSK.sFun (λ x → lemma-Subst _ (sub x) DSK.sKVar≠ DSK.sGVar≠)
  lemma-SubstV DS.sShift = DSK.sShift
  lemma-SubstV DS.sShift0 = DSK.sShift0
  
  -- e₁[x:=v] ≡ e₂ => (e₁[x:=v] : c₁[x:=v] : m₁[x:=v]) ≡ (e₂ : c₂ : m₂)
  lemma-Subst : {var : Set} {Δ : DSK.Delta} {Θ : DSK.Theta} →
                (ΔΘ : DSK.Delta-Theta Δ Θ) →
                {e₁ : var →
                        DS.term[ var ]} →
                {c₁ : var →
                        DSK.cont[ var , Δ ]} →
                {m₁ : var →
                        DSK.mcont[ var , Θ ]} →
                {v  : DS.value[ var ]} →
                {e₂ : DS.term[ var ]} →
                {c₂ : DSK.cont[ var , Δ ]} →
                {m₂ : DSK.mcont[ var , Θ ]} →
                DS.Subst e₁ v e₂ →
                DSK.SubstC c₁ (knV v) c₂ →
                DSK.SubstM m₁ (knV v) m₂ →
                DSK.Subst {var} (λ x → knE ΔΘ (e₁ x) (c₁ x) (m₁ x) )
                                (knV v)
                                (knE ΔΘ e₂ c₂ m₂)
  lemma-Subst ΔΘ (DS.sVal sub-v) sub-c sub-m =
    DSK.sVal ΔΘ sub-c (lemma-SubstV sub-v) sub-m
  lemma-Subst ΔΘ (DS.sNonVal (DS.sApp (DS.sVal sub-v₁) (DS.sVal sub-v₂))) sub-c sub-m =
    DSK.sApp ΔΘ (lemma-SubstV sub-v₁) (lemma-SubstV sub-v₂) sub-c sub-m
  lemma-Subst ΔΘ (DS.sNonVal (DS.sApp (DS.sVal sub-v) (DS.sNonVal sub))) sub-c sub-m =
    lemma-Subst ΔΘ (DS.sNonVal sub)
                    (DSK.sKLet (λ y →
                      DSK.sApp _ (lemma-SubstV sub-v) DSK.sVar≠ sub-c DSK.sGVar≠))
                    sub-m
  lemma-Subst ΔΘ (DS.sNonVal (DS.sApp (DS.sNonVal sub) (DS.sVal sub-v))) sub-c sub-m =
    lemma-Subst ΔΘ (DS.sNonVal sub)
                    (DSK.sKLet (λ x →
                      DSK.sApp _ DSK.sVar≠ (lemma-SubstV sub-v) sub-c DSK.sGVar≠))
                    sub-m
  lemma-Subst ΔΘ (DS.sNonVal (DS.sApp (DS.sNonVal sub₁) (DS.sNonVal sub₂))) sub-c sub-m =
    lemma-Subst ΔΘ (DS.sNonVal sub₁)
                    (DSK.sKLet (λ x →
                      lemma-Subst _ (DS.sNonVal sub₂)
                                    (DSK.sKLet (λ y →
                                      DSK.sApp _ DSK.sVar≠ DSK.sVar≠ sub-c DSK.sGVar≠))
                                    DSK.sGVar≠))
                    sub-m
  lemma-Subst ΔΘ (DS.sNonVal (DS.sReset sub)) sub-c sub-m =
    lemma-Subst _ sub (DSK.SubstC≠ _) (DSK.sGCons ΔΘ sub-c sub-m)
  lemma-Subst ΔΘ (DS.sNonVal (DS.sLet sub₁ sub₂)) sub-c sub-m =
    lemma-Subst ΔΘ sub₂
                (DSK.sKLet (λ x → lemma-Subst _ (sub₁ x) sub-c DSK.sGVar≠)) sub-m


-- m₁[k:=c'] ≡ m₂ => (e : c : m₁)[k:=c'] ≡ (e : c : m₂)
lemma-CSubstM : {var : Set} {Δ : DSK.Delta}
                (e  : DS.term[ var ]) →
                {c  : DSK.cont[ var , DSK.• ]} →
                {m₁ : DSK.mcont[ var , DSK.D DSK.K ]} →
                {c'  : DSK.cont[ var , Δ ]} →
                {m₂ : DSK.mcont[ var , DSK.D Δ ]} →
                DSK.CSubstM m₁ c' m₂ →
                DSK.CSubst (knE tt e c m₁) c' (knE tt e c m₂)
lemma-CSubstM (DS.Val v) csub-m = DSK.sVal₂ csub-m
lemma-CSubstM (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) csub-m =
  DSK.sApp₂ csub-m
lemma-CSubstM (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) csub-m =
  lemma-CSubstM (DS.NonVal q) csub-m
lemma-CSubstM (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) csub-m =
  lemma-CSubstM (DS.NonVal p) csub-m
lemma-CSubstM (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) csub-m =
  lemma-CSubstM (DS.NonVal p) csub-m
lemma-CSubstM (DS.NonVal (DS.Reset e)) csub-m =
  lemma-CSubstM e (DSK.sGCons₂ csub-m)
lemma-CSubstM (DS.NonVal (DS.Let e₁ e₂)) csub-m =
  lemma-CSubstM e₁ csub-m 


-- c₁[k:=c] ≡ c₂ => (e : c₁ : g)[k:=c] ≡ (e : c₂ : g)
lemma-CSubstC : {var : Set} {Δ : DSK.Delta}
                (e  : DS.term[ var ]) →
                {c₁ : DSK.cont[ var , DSK.K ]} →
                {c  : DSK.cont[ var , Δ ]} →
                {c₂ : DSK.cont[ var , Δ ]} →
                DSK.CSubstC c₁ c c₂ →
                DSK.CSubst (knE tt e c₁ DSK.GVar) c (knE tt e c₂ DSK.GVar)
lemma-CSubstC (DS.Val v) csub-c = DSK.sVal₁ csub-c 
lemma-CSubstC (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) csub-c =
  DSK.sApp₁ csub-c
lemma-CSubstC (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) csub-c =
  lemma-CSubstC (DS.NonVal q) (DSK.sKLet₂ (λ x → DSK.sApp₁ csub-c))
lemma-CSubstC (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) csub-c =
  lemma-CSubstC (DS.NonVal p) (DSK.sKLet₂ (λ x → DSK.sApp₁ csub-c))
lemma-CSubstC (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) csub-c =
  lemma-CSubstC (DS.NonVal p) (DSK.sKLet₂ (λ x →
    lemma-CSubstC (DS.NonVal q) (DSK.sKLet₂ (λ y → DSK.sApp₁ csub-c))))
lemma-CSubstC (DS.NonVal (DS.Reset e)) csub-c =
  lemma-CSubstM e (DSK.sGCons₁ csub-c)
lemma-CSubstC (DS.NonVal (DS.Let e₁ e₂)) csub-c =
  lemma-CSubstC e₁ (DSK.sKLet₂ (λ x → lemma-CSubstC (e₂ x) csub-c))
  
  
  
-- m₁[g:=m] ≡ m => (e : c : m₁)[g:=m] ≡ (e : c : m₂)
lemma-MSubst : {var : Set} {Δ : DSK.Delta} {Θ Θ' : DSK.Theta} →
               {ΔΘ₁ : DSK.Delta-Theta Δ Θ} →
               {ΔΘ₂ : DSK.Delta-Theta Δ (Θ DSK.+++ Θ')} →
               (e  : DS.term[ var ]) →
               {c  : DSK.cont[ var , Δ ]} →
               {m₁ : DSK.mcont[ var , Θ ]} →
               {m  : DSK.mcont[ var , Θ' ]} →
               {m₂ : DSK.mcont[ var , Θ DSK.+++ Θ' ]} →
               DSK.MSubstM m₁ m refl m₂ →
               DSK.MSubst (knE ΔΘ₁ e c m₁) m refl (knE ΔΘ₂ e c m₂)
lemma-MSubst (DS.Val v) msub-m = DSK.sVal _ _ msub-m
lemma-MSubst (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) msub-m =
  DSK.sApp _ _ _ _ _ _ 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)) msub-m =
  lemma-MSubst e (DSK.mGCons _ _ msub-m)
lemma-MSubst (DS.NonVal (DS.Let e₁ e₂)) msub-m = lemma-MSubst e₁ msub-m


-- RShift, RShift0
contExist : {var : Set} {Δ : DSK.Delta}
            (j : DS.pcontext[ var ]) →
            (c : DSK.cont[ var , Δ ]) →
            Σ[ j' ∈ DSK.cont[ var  , Δ ] ]
            ({Θ : DSK.Theta} (ΔΘ : DSK.Delta-Theta Δ Θ) →
             (p : DS.nonvalue[ var ]) →
             (m : DSK.mcont[ var , Θ ]) →
             knE ΔΘ (DS.plug j (DS.NonVal p)) c m ≡ knE ΔΘ (DS.NonVal p) j' m)
            ×
            ({Θ' : DSK.Theta} (ΔΘ' : DSK.Delta-Theta Δ Θ') →
             (v : DS.value[ var ]) →
             (m' : DSK.mcont[ var , Θ' ]) →
            DSK.Reduce (DSK.Val ΔΘ' j' (knV v) m')
                       (knE ΔΘ' (DS.plug j (DS.Val v)) c m'))
contExist DS.Hole c = c , (λ ΔΘ p m → refl) , λ ΔΘ' v m' → DSK.RId
contExist (DS.App₁ j (DS.Val w)) c with contExist j c
... | j' , eq , red = _ ,
  (λ ΔΘ p m → eq ΔΘ (DS.App (DS.NonVal p) (DS.Val w)) m) ,
  λ ΔΘ' v m' → begin
  DSK.Val ΔΘ' (DSK.KLet (λ x → DSK.App tt (DSK.Var x) (knV w) j' DSK.GVar))
              (knV v) m'
  ⟶⟨ DSK.RBetaLet _
        (DSK.sApp tt DSK.sVar= (DSK.SubstV≠ _) (DSK.SubstC≠ _) DSK.sGVar≠)
        (DSK.sApp _ _ _ _ _ _ DSK.mGVar=) ⟩
  knE ΔΘ' (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) j' m'
  ≡⟨ sym (eq ΔΘ' (DS.App (DS.Val v) (DS.Val w)) m') ⟩
  knE ΔΘ' (DS.plug j (DS.NonVal (DS.App (DS.Val v) (DS.Val w)))) c m'
  ∎
  where open DSK.Reasoning
contExist (DS.App₁ j (DS.NonVal q)) c with contExist j c
... | j' , eq , red = _ ,
  (λ ΔΘ p m → eq ΔΘ (DS.App (DS.NonVal p) (DS.NonVal q)) m) ,
  λ ΔΘ' v m' → begin
  DSK.Val ΔΘ'
    (DSK.KLet (λ x →
      knE tt (DS.NonVal q)
             (DSK.KLet (λ y → DSK.App tt (DSK.Var x) (DSK.Var y) j' DSK.GVar))
             DSK.GVar))
    (knV v) m'
  ⟶⟨ DSK.RBetaLet _
        (lemma-Subst tt (DS.Subst≠ (DS.NonVal q))
                        (DSK.sKLet λ x →
                          DSK.sApp tt DSK.sVar= DSK.sVar≠
                                      (DSK.SubstC≠ j') (DSK.SubstM≠ DSK.GVar))
                        DSK.sGVar≠)
        (lemma-MSubst (DS.NonVal q) DSK.mGVar=) ⟩
  knE ΔΘ' (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) j' m'
  ≡⟨ sym (eq ΔΘ' (DS.App (DS.Val v) (DS.NonVal q)) m') ⟩
  knE ΔΘ' (DS.plug j (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q)))) c m'
  ∎
  where open DSK.Reasoning
contExist (DS.App₂ v j) c with contExist j c
... | j' , eq , red = _ ,
  (λ ΔΘ p m → eq ΔΘ (DS.App (DS.Val v) (DS.NonVal p)) m) ,
  λ ΔΘ' v' m' → begin
  DSK.Val ΔΘ'
    (DSK.KLet (λ y → DSK.App tt (knV v) (DSK.Var y) j' DSK.GVar))
    (knV v') m'
  ⟶⟨ DSK.RBetaLet _
       (DSK.sApp tt (DSK.SubstV≠ _) DSK.sVar= (DSK.SubstC≠ _) (DSK.SubstM≠ _))
       (DSK.sApp _ _ _ _ _ _ DSK.mGVar=) ⟩ 
  knE ΔΘ' (DS.NonVal (DS.App (DS.Val v) (DS.Val v'))) j' m'
  ≡⟨ sym (eq ΔΘ' (DS.App (DS.Val v) (DS.Val v')) m') ⟩
  knE ΔΘ' (DS.plug j (DS.NonVal (DS.App (DS.Val v) (DS.Val v')))) c m'
  ∎
  where open DSK.Reasoning
contExist (DS.Let j f) c with contExist j c
... | j' , eq , red = _ ,
  (λ ΔΘ p m → eq ΔΘ (DS.Let (DS.NonVal p) f) m) ,
  λ ΔΘ' v m' → begin
  DSK.Val ΔΘ' (DSK.KLet (λ x → knE tt (f x) j' DSK.GVar)) (knV v) m'
  ≡⟨ sym (eq ΔΘ' (DS.Let (DS.Val v) f) m') ⟩
  knE ΔΘ' (DS.plug j (DS.NonVal (DS.Let (DS.Val v) f))) c m'
  ∎
  where open DSK.Reasoning

redShift : {var : Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
           (ΔΘ : DSK.Delta-Theta Δ Θ) →
           (v : DS.value[ var ]) →
           (j : DS.pcontext[ var ]) →
           {c : DSK.cont[ var , Δ ]} →
           {m : DSK.mcont[ var , Θ ]} →
           DSK.Reduce
             (knE tt
               (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift) (DS.Val v))))
               DSK.KId (DSK.GCons ΔΘ c m))
             (DSK.App tt (knV v)
               (DSK.Fun (λ x →
                 knE tt (DS.plug j (DS.Val (DS.Var x)))
                        DSK.KId
                        (DSK.GCons tt DSK.KVar DSK.GVar)))
               DSK.KId (DSK.GCons ΔΘ c m))
redShift {var} {Δ} {Θ} ΔΘ v j {c} {m}
  with contExist {var} j DSK.KId
... | j' , eq , red = begin
  knE tt (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift) (DS.Val v))))
         DSK.KId (DSK.GCons ΔΘ c m)
  ≡⟨ eq tt (DS.App (DS.Val DS.Shift) (DS.Val v)) (DSK.GCons ΔΘ c m) ⟩
  knE tt  (DS.NonVal (DS.App (DS.Val DS.Shift) (DS.Val v)))
          j' (DSK.GCons ΔΘ c m)
  ⟶⟨ DSK.RShift ⟩
  DSK.App tt (knV v)
    (DSK.Fun (λ x → DSK.Val tt j' (DSK.Var x) (DSK.GCons tt DSK.KVar DSK.GVar)))
    DSK.KId (DSK.GCons ΔΘ c m)
  ⟶⟨ DSK.RApp₂ _
       (DSK.RFun (λ x → red tt (DS.Var x) (DSK.GCons tt DSK.KVar DSK.GVar))) ⟩
  DSK.App tt (knV v)
    (DSK.Fun (λ x →
      knE tt (DS.plug j (DS.Val (DS.Var x)))
             DSK.KId (DSK.GCons tt DSK.KVar DSK.GVar)))
    DSK.KId (DSK.GCons ΔΘ c m)
  ∎
  where open DSK.Reasoning

redShift0 : {var : Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
            (ΔΘ : DSK.Delta-Theta Δ Θ) →
            (v : DS.value[ var ]) →
            (j : DS.pcontext[ var ]) →
            {c : DSK.cont[ var , Δ ]} →
            {m : DSK.mcont[ var , Θ ]} →
            DSK.Reduce
              (knE tt
                (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v))))
                DSK.KId (DSK.GCons ΔΘ c m))
              (DSK.App ΔΘ (knV v)
                (DSK.Fun
                  (λ x →
                    knE tt (DS.plug j (DS.Val (DS.Var x)))
                    DSK.KId (DSK.GCons tt DSK.KVar DSK.GVar)))
                c m)
redShift0 {var} {Δ} {Θ} ΔΘ v j {c} {m}
  with contExist {var} j DSK.KId
... | j' , eq , red = begin
  knE tt (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v))))
         DSK.KId (DSK.GCons ΔΘ c m)
  ≡⟨ eq tt (DS.App (DS.Val DS.Shift0) (DS.Val v)) (DSK.GCons ΔΘ c m) ⟩
  knE tt (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v)))
         j' (DSK.GCons ΔΘ c m)
  ⟶⟨ DSK.RShift0 ΔΘ ⟩
  DSK.App ΔΘ (knV v)
    (DSK.Fun (λ x →
        knE tt (DS.Val (DS.Var x)) j' (DSK.GCons tt DSK.KVar DSK.GVar)))
    c m
  ⟶⟨ DSK.RApp₂ _
       (DSK.RFun (λ x → (red tt (DS.Var x) (DSK.GCons tt DSK.KVar DSK.GVar)))) ⟩
  DSK.App ΔΘ (knV v)
    (DSK.Fun (λ x →
        knE tt (DS.plug j (DS.Val (DS.Var x)))
               DSK.KId (DSK.GCons tt DSK.KVar DSK.GVar)))
    c m
  ∎
  where open DSK.Reasoning

-- Reduction Presevation by : in the 3rd argument
correctM : {var : Set} {Δ : DSK.Delta} → {Θ : DSK.Theta} →
            (ΔΘ : DSK.Delta-Theta Δ Θ) →
            (e : DS.term[ var ]) →
            {c : DSK.cont[ var , Δ ]} →
            {m m' : DSK.mcont[ var , Θ ]} →
            DSK.ReduceM m m' →
            DSK.Reduce {var} (knE ΔΘ e c m) (knE ΔΘ e c m')
correctM ΔΘ (DS.Val v) red-m = DSK.RVal₃ _ red-m
correctM ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) red-m =
  DSK.RApp₄ _ red-m
correctM ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) red-m = 
  correctM _ (DS.NonVal q) red-m
correctM ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) red-m =
  correctM _ (DS.NonVal p) red-m
correctM ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) red-m = 
  correctM _ (DS.NonVal p) red-m
correctM ΔΘ (DS.NonVal (DS.Reset e)) red-m =
  correctM _ e (DSK.RGCons₂ _ red-m)
correctM ΔΘ (DS.NonVal (DS.Let e₁ e₂)) red-m =
  correctM _ e₁ red-m

-- Reduction preservation by : in the 2nd argument
correctC : {var : Set} {Δ : DSK.Delta} → {Θ : DSK.Theta} →
            (ΔΘ : DSK.Delta-Theta Δ Θ) →
            (e : DS.term[ var ]) →
            {c c' : DSK.cont[ var , Δ ]} →
            {m : DSK.mcont[ var , Θ ]} →
            DSK.ReduceC c c' →
            DSK.Reduce {var} (knE ΔΘ e c m) (knE ΔΘ e c' m)
correctC ΔΘ (DS.Val v) red-c = DSK.RVal₁ _ red-c
correctC ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.Val w))) red-c =
  DSK.RApp₃ _ red-c
correctC ΔΘ (DS.NonVal (DS.App (DS.Val v) (DS.NonVal q))) red-c =
  correctC _ (DS.NonVal q) (DSK.RKLet (λ x → DSK.RApp₃ _ red-c))
correctC ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.Val w))) red-c =
  correctC _ (DS.NonVal p) (DSK.RKLet (λ x → DSK.RApp₃ _ red-c))
correctC ΔΘ (DS.NonVal (DS.App (DS.NonVal p) (DS.NonVal q))) red-c = 
  correctC _ (DS.NonVal p) (DSK.RKLet (λ x →
    correctC _ (DS.NonVal q) (DSK.RKLet (λ y → DSK.RApp₃ _ red-c))))
correctC ΔΘ (DS.NonVal (DS.Reset e)) red-c =
  correctM _ e (DSK.RGCons₁ _ red-c)
correctC ΔΘ (DS.NonVal (DS.Let e₁ e₂)) red-c =
  correctC _ e₁ (DSK.RKLet (λ x → correctC _ (e₂ x) red-c))


-- main theorem
mutual
  -- value
  correctV : {var : Set} →
             {v w : DS.value[ var ]} →
             DS.Reduce (DS.Val v) (DS.Val w) →
             DSK.ReduceV {var} (knV v) (knV w)
  correctV (DS.REtaV _) = DSK.REtaV 
  correctV (DS.RFun red) = DSK.RFun (λ x → correctE _ (red x))
  correctV DS.RId = DSK.RId
  correctV (DS.RTrans {e₂ = DS.Val v} red₁ red₂) =
    DSK.RTrans (correctV red₁) (correctV red₂)
  correctV (DS.RTrans {e₂ = DS.NonVal p} red₁ red₂) with DS.reduceVal red₁
  ... | ()

  -- term
  correctE : {var : Set} → {Δ : DSK.Delta} → {Θ : DSK.Theta} →
             (ΔΘ : DSK.Delta-Theta Δ Θ) →
             {e e' : DS.term[ var ]} →
             {c : DSK.cont[ var , Δ ]} →
             {m : DSK.mcont[ var , Θ ]} →
             DS.Reduce e e' →
             DSK.Reduce {var} (knE ΔΘ e c m) (knE ΔΘ e' c m)
  correctE ΔΘ (DS.RBetaV e₁ v₂ e₁' sub) =
    DSK.RBetaV ΔΘ (lemma-Subst tt sub DSK.sKVar≠ DSK.sGVar≠)
                  (lemma-CSubstC e₁' DSK.sKVar=)
                  (lemma-MSubst e₁' DSK.mGVar=)
  correctE ΔΘ (DS.REtaV v) = DSK.RVal₂ ΔΘ DSK.REtaV
  correctE ΔΘ (DS.RBetaLet v₁ e₂ e₂' sub) =
    DSK.RBetaLet ΔΘ (lemma-Subst tt sub (DSK.SubstC≠ _) DSK.sGVar≠)
                    (lemma-MSubst e₂' DSK.mGVar=)
  correctE ΔΘ (DS.REtaLet e₁) = correctC _ e₁ DSK.REtaLet
  correctE ΔΘ (DS.RAssoc e₁ e₂ e₃) = DSK.RId
  correctE ΔΘ (DS.RLet1 e₁ (DS.Val v)) = DSK.RId
  correctE ΔΘ (DS.RLet1 e₁ (DS.NonVal p)) = DSK.RId
  correctE ΔΘ (DS.RLet2 e₂) = DSK.RId
  correctE ΔΘ (DS.RShift v j) = redShift _ v j
  correctE ΔΘ (DS.RShift0 v j) = redShift0 _ v j
  correctE ΔΘ (DS.RReset v₁) = DSK.RReset ΔΘ
  correctE ΔΘ (DS.RFun red) = DSK.RVal₂ ΔΘ (DSK.RFun λ x → correctE _ (red x))
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.Val v} {DS.Val v'} {DS.Val w} red) =
    DSK.RApp₁ _ (correctV red)
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.Val v} {DS.Val v'} {DS.NonVal q} red) =
    correctC _ (DS.NonVal q) (DSK.RKLet (λ x → DSK.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) =
    DSK.RTrans (correctE _ red)
               (DSK.RBetaLet _ (DSK.sApp tt DSK.sVar= (DSK.SubstV≠ _)
                                            (DSK.SubstC≠ _) (DSK.SubstM≠ _))
                               (DSK.sApp _ _ _ _ _ _ DSK.mGVar=))
  correctE ΔΘ (DS.RApp₁ {e₁ = DS.NonVal p} {DS.Val v} {DS.NonVal q} red) =
    DSK.RTrans (correctE _ red)
               (DSK.RBetaLet _
                 (lemma-Subst _ (DS.Subst≠ (DS.NonVal q))
                                (DSK.sKLet (λ x →
                                  (DSK.sApp tt DSK.sVar= DSK.sVar≠
                                               (DSK.SubstC≠ _) (DSK.SubstM≠ _))))
                                  (DSK.SubstM≠ _))
                 (lemma-MSubst (DS.NonVal q) DSK.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 v} {DS.Val v'} red) =
    DSK.RApp₂ _ (correctV red)
  correctE ΔΘ (DS.RApp₂ {e₂ = DS.Val v} {DS.NonVal p} red) with DS.reduceVal red
  ... | ()
  correctE ΔΘ (DS.RApp₂ {e₂ = DS.NonVal p} {DS.Val v} red) =
    DSK.RTrans (correctE _ red)
               (DSK.RBetaLet _ (DSK.sApp tt (lemma-SubstV (DS.SubstV≠ _)) DSK.sVar=
                                            (DSK.SubstC≠ _) (DSK.SubstM≠ _))
                               (DSK.sApp _ _ _ _ _ _ DSK.mGVar=))
  correctE ΔΘ (DS.RApp₂ {e₂ = DS.NonVal p} {DS.NonVal p'} red) =
    correctE _ red
  correctE ΔΘ (DS.RLet₁ red) = correctE _ red
  correctE ΔΘ (DS.RLet₂ {e₁ = e₁} red) =
    correctC _ e₁ (DSK.RKLet (λ x → correctE tt (red x)))
  correctE ΔΘ (DS.RReset₁ red) = correctE _ red
  correctE ΔΘ DS.RId = DSK.RId
  correctE ΔΘ (DS.RTrans red₁ red₂) =
    DSK.RTrans (correctE _ red₁) (correctE _ red₂)