{-# 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 : DSK.Ty → Set} → {τ₁ τ₂ : DS.Ty} →
                 {v₁ : (var ∘ knT) τ₁ → DS.value[ var ∘ knT ] τ₂} →
                 {v  : DS.value[ var ∘ knT ] τ₁} →
                 {v₂ : DS.value[ var ∘ knT ] τ₂} →
                 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 id) = DSK.sShift (kn-id-cont-type id)
  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 : DSK.Ty → Set} {τ₁ τ₂ α β : DS.Ty} {σ σα σβ : DS.Mc}
                {Δ : DSK.Delta} {Θ : DSK.Theta} →
                (ΔΘ : DSK.Delta-Theta Δ Θ) →
                {e₁ : (var ∘ knT) τ₂ →
                        DS.term[ var ∘ knT , τ₁ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β} →
                {c₁ : (var ∘ knT) τ₂ →
                        DSK.cont[ var , Δ ,
                                  knT τ₁ ]⟨ knMc σα ⟩ knT α} →
                {m₁ : (var ∘ knT) τ₂ →
                        DSK.mcont[ var , Θ , knMc σ ] knMc σβ} →
                {v  : DS.value[ var ∘ knT ] τ₂} →
                {e₂ : DS.term[ var ∘ knT , τ₁ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β} →
                {c₂ : DSK.cont[ var , Δ ,
                                  knT τ₁ ]⟨ knMc σα ⟩ knT α} →
                {m₂ : DSK.mcont[ var , Θ , knMc σ ] knMc σβ} →
                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 : DSK.Ty → Set} {Δ : DSK.Delta}
                {τ α β τ' α' τ₁ τ₂ : DS.Ty} {σ σα σβ σα' σ₁ : DS.Mc} →
                {γ γ' : DSK.Ty} {σid : DSK.Mc} →
                {id : DSK.id-cont-type (γ DSK.▷⟨ σid ⟩ γ')} →
                (e  : DS.term[ var ∘ knT , τ₁ DS.▷⟨ σ₁ ⟩ τ₂
                                              ]⟨ τ DS.⇨⟨ σα ⟩ α ∷ σβ ⟩ β) →
                {c  : DSK.cont[ var , DSK.• (γ DSK.▷⟨ σid ⟩ γ') id ,
                                                knT τ₁ ]⟨ knMc σ₁ ⟩ knT τ₂} →
                {m₁ : DSK.mcont[ var ,
                        DSK.D (DSK.K (knT τ' DSK.▷⟨ knMc σα' ⟩ knT α')) ,
                          knMc σ ] (knT τ DSK.⇨⟨ knMc σα ⟩ knT α ∷ knMc σβ)} →
                {c'  : DSK.cont[ var , Δ , knT τ' ]⟨ knMc σα' ⟩ knT α'} →
                {m₂ : DSK.mcont[ var , DSK.D Δ , knMc σ
                        ] (knT τ DSK.⇨⟨ knMc σα ⟩ knT α ∷ knMc σβ)} →
                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 id 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 : DSK.Ty → Set} {Δ : DSK.Delta}
                {τ α β τ' α' : DS.Ty} {σα σβ σα' : DS.Mc} →
                (e  : DS.term[ var ∘ knT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
                {c₁ : DSK.cont[ var , DSK.K (knT τ' DSK.▷⟨ knMc σα' ⟩ knT α') ,
                                                    knT τ ]⟨ knMc σα ⟩ knT α} →
                {c  : DSK.cont[ var , Δ , knT τ' ]⟨ knMc σα' ⟩ knT α'} →
                {c₂ : DSK.cont[ var , Δ , knT τ ]⟨ knMc σα ⟩ knT α} →
                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 id 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 : DSK.Ty → Set} {τ α β : DS.Ty} {σ σ' σα σβ : DS.Mc} →
               {Δ : DSK.Delta} {Θ Θ' : DSK.Theta} →
               {ΔΘ₁ : DSK.Delta-Theta Δ Θ} →
               {ΔΘ₂ : DSK.Delta-Theta Δ (Θ DSK.+++ Θ')} →
               (e  : DS.term[ var ∘ knT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
               {c  : DSK.cont[ var , Δ , knT τ ]⟨ knMc σα ⟩ knT α} →
               {m₁ : DSK.mcont[ var , Θ , knMc σ' ] knMc σβ} →
               {m  : DSK.mcont[ var , Θ' , knMc σ ] knMc σ'} →
               {m₂ : DSK.mcont[ var , Θ DSK.+++ Θ' , knMc σ ] knMc σβ} →
               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 id 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 : DSK.Ty → Set} {Δ : DSK.Delta}
            {τ τ₄ τ₅ α : DS.Ty} {σ₅ σα : DS.Mc} →
            (j : DS.pcontext[ var ∘ knT , τ₄ DS.▷⟨ σ₅ ⟩ τ₅ , τ ]⟨ σα ⟩ α) →
            (c : DSK.cont[ var , Δ , knT τ₄ ]⟨ knMc σ₅ ⟩ knT τ₅) →
            Σ[ j' ∈ DSK.cont[ var  , Δ , knT τ ]⟨ knMc σα ⟩ knT α ]
            ({β : DS.Ty} {σ σβ : DS.Mc} {Θ : DSK.Theta}
             (ΔΘ : DSK.Delta-Theta Δ Θ) →
             (p : DS.nonvalue[ var ∘ knT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β ) →
             (m : DSK.mcont[ var , Θ , knMc σ ] knMc σβ) →
             knE ΔΘ (DS.plug j (DS.NonVal p)) c m ≡ knE ΔΘ (DS.NonVal p) j' m)
            ×
            ({σ' : DS.Mc} {Θ' : DSK.Theta}
             (ΔΘ' : DSK.Delta-Theta Δ Θ') →
             (v : DS.value[ var ∘ knT ] τ) →
             (m' : DSK.mcont[ var , Θ' , knMc σ' ] knMc σα) →
            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 : DSK.Ty → Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
           {τ τ₁ τ₂ τ₃ τ₄ τ₅ α α₁ β γ γ' : DS.Ty}
           {σ σ₁ σ₂ σ₅ σα σβ σid : DS.Mc} →
           (ΔΘ : DSK.Delta-Theta Δ Θ) →
           (id₁ : DS.id-cont-type γ σid γ') →
           (id₂ : DS.id-cont-type τ₄ σ₅ τ₅) →
           (v : DS.value[ var ∘ knT ]
                          ((τ₁ DS.⇒ τ₂ ⟨ σ₁ ⟩ τ₃ ⟨ σ₂ ⟩ α₁) DS.⇒
                              γ ⟨ σid ⟩ γ' ⟨ τ DS.⇨⟨ σα ⟩ α ∷ σβ ⟩ β)) →
           (j : DS.pcontext[ var ∘ knT , τ₄ DS.▷⟨ σ₅ ⟩ τ₅ ,
                                            τ₁ ]⟨ τ₂ DS.⇨⟨ σ₁ ⟩ τ₃ ∷ σ₂ ⟩ α₁) →
           {c : DSK.cont[ var , Δ , knT τ ]⟨ knMc σα ⟩ knT α} →
           {m : DSK.mcont[ var , Θ , knMc σ ] knMc σβ } →
           DSK.Reduce
             (knE tt
               (DS.plug j (DS.NonVal (DS.App (DS.Val (DS.Shift id₁)) (DS.Val v))))
               (DSK.KId (kn-id-cont-type id₂)) (DSK.GCons ΔΘ c m))
             (DSK.App tt (knV v)
               (DSK.Fun (λ x →
                 knE tt (DS.plug j (DS.Val (DS.Var x)))
                        (DSK.KId (kn-id-cont-type id₂))
                        (DSK.GCons tt DSK.KVar DSK.GVar)))
               (DSK.KId (kn-id-cont-type id₁)) (DSK.GCons ΔΘ c m))
redShift {var} {Δ} {Θ} ΔΘ id₁ id₂ v j {c} {m}
  with contExist {var} j (DSK.KId (kn-id-cont-type id₂))
... | j' , eq , red = begin
  knE tt (DS.plug j (DS.NonVal (DS.App (DS.Val (DS.Shift id₁)) (DS.Val v))))
         (DSK.KId (kn-id-cont-type id₂)) (DSK.GCons ΔΘ c m)
  ≡⟨ eq tt (DS.App (DS.Val (DS.Shift id₁)) (DS.Val v)) (DSK.GCons ΔΘ c m) ⟩
  knE tt  (DS.NonVal (DS.App (DS.Val (DS.Shift id₁)) (DS.Val v)))
          j' (DSK.GCons ΔΘ c m)
  ⟶⟨ DSK.RShift (kn-id-cont-type id₁) (kn-id-cont-type id₂) ⟩
  DSK.App tt (knV v)
    (DSK.Fun (λ x → DSK.Val tt j' (DSK.Var x) (DSK.GCons tt DSK.KVar DSK.GVar)))
    (DSK.KId (kn-id-cont-type id₁)) (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 (kn-id-cont-type id₂)) (DSK.GCons tt DSK.KVar DSK.GVar)))
    (DSK.KId (kn-id-cont-type id₁)) (DSK.GCons ΔΘ c m)
  ∎
  where open DSK.Reasoning

redShift0 : {var : DSK.Ty → Set} {Δ : DSK.Delta} {Θ : DSK.Theta}
            {τ τ₁ τ₂ τ₃ τ₄ τ₅ α α₁ β : DS.Ty}
            {σ₁ σ₂ σ₅ σ σα σβ : DS.Mc} →
            (ΔΘ : DSK.Delta-Theta Δ Θ) →
            (id : DS.id-cont-type τ₄ σ₅ τ₅) →
            (v : DS.value[ var ∘ knT ]
                           ((τ₁ DS.⇒ τ₂ ⟨ σ₁ ⟩ τ₃ ⟨ σ₂ ⟩ α₁) DS.⇒
                                                 τ ⟨ σα ⟩ α ⟨ σβ ⟩ β)) →
            (j : DS.pcontext[ var ∘ knT , τ₄ DS.▷⟨ σ₅ ⟩ τ₅ ,
                                             τ₁ ]⟨ τ₂ DS.⇨⟨ σ₁ ⟩ τ₃ ∷ σ₂ ⟩ α₁) →
            {c : DSK.cont[ var , Δ , knT τ ]⟨ knMc σα ⟩ knT α} →
            {m : DSK.mcont[ var , Θ , knMc σ ] knMc σβ } →
            DSK.Reduce
              (knE tt
                (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v))))
                (DSK.KId (kn-id-cont-type id)) (DSK.GCons ΔΘ c m))
              (DSK.App ΔΘ (knV v)
                (DSK.Fun
                  (λ x →
                    knE tt (DS.plug j (DS.Val (DS.Var x)))
                    (DSK.KId (kn-id-cont-type id)) (DSK.GCons tt DSK.KVar DSK.GVar)))
                c m)
redShift0 {var} {Δ} {Θ} ΔΘ id v j {c} {m}
  with contExist {var} j (DSK.KId (kn-id-cont-type id))
... | j' , eq , red = begin
  knE tt (DS.plug j (DS.NonVal (DS.App (DS.Val DS.Shift0) (DS.Val v))))
         (DSK.KId (kn-id-cont-type id)) (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 ΔΘ (kn-id-cont-type id) ⟩
  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 (kn-id-cont-type id)) (DSK.GCons tt DSK.KVar DSK.GVar)))
    c m
  ∎
  where open DSK.Reasoning

-- Reduction Presevation by : in the 3rd argument
correctM : {var : DSK.Ty → Set} {τ α β : DS.Ty} {σ σα σβ : DS.Mc} →
            {Δ : DSK.Delta} → {Θ : DSK.Theta} →
            (ΔΘ : DSK.Delta-Theta Δ Θ) →
            (e : DS.term[ var ∘ knT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
            {c : DSK.cont[ var , Δ , knT τ ]⟨ knMc σα ⟩ knT α} →
            {m m' : DSK.mcont[ var , Θ , knMc σ ] knMc σβ} →
            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 id 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 : DSK.Ty → Set} {τ α β : DS.Ty} {σ σα σβ : DS.Mc} →
            {Δ : DSK.Delta} → {Θ : DSK.Theta} →
            (ΔΘ : DSK.Delta-Theta Δ Θ) →
            (e : DS.term[ var ∘ knT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β) →
            {c c' : DSK.cont[ var , Δ , knT τ ]⟨ knMc σα ⟩ knT α} →
            {m : DSK.mcont[ var , Θ , knMc σ ] knMc σβ} →
            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 id 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 : DSK.Ty → Set} {τ β : DS.Ty} {σβ : DS.Mc} →
             {v w : DS.value[ var ∘ knT ] τ} →
             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 : DSK.Ty → Set} {τ α β : DS.Ty} {σ σα σβ : DS.Mc} →
             {Δ : DSK.Delta} → {Θ : DSK.Theta} →
             (ΔΘ : DSK.Delta-Theta Δ Θ) →
             {e e' : DS.term[ var ∘ knT , τ DS.▷⟨ σα ⟩ α ]⟨ σβ ⟩ β} →
             {c : DSK.cont[ var , Δ , knT τ ]⟨ knMc σα ⟩ knT α} →
             {m : DSK.mcont[ var , Θ , knMc σ ] knMc σβ} →
             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 id₁ id₂ v j) = redShift _ id₁ id₂ v j
  correctE ΔΘ (DS.RShift0 id v j) = redShift0 _ id 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₁ id red) = correctE _ red
  correctE ΔΘ DS.RId = DSK.RId
  correctE ΔΘ (DS.RTrans red₁ red₂) =
    DSK.RTrans (correctE _ red₁) (correctE _ red₂)