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

import DS
import DSK
open import DSK-DS

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

-- postulate
postulate
  lemma-Var-subst : {var : DSK.Ty → Set} {τ₁ τ₂ : DSK.Ty}
                    {Δ : DSK.Delta} {σ : DSK.Mc}
                    {e : var τ₁ → DSK.term[ var , Δ ]⟨ σ ⟩ τ₂} →
                    {x : var τ₁} →
                    DSK.Subst e (DSK.Var x) (e x)

-- substitution lemma
mutual
  -- v₁[x:=v] = v₂
  lemma-SubstV : {var : DS.Ty → Set} → {τ₁ τ₂ : DSK.Ty} →
                 {v₁ : (var ∘ embT) τ₁ → DSK.value[ var ∘ embT ] τ₂} →
                 {v  : DSK.value[ var ∘ embT ] τ₁} →
                 {v₂ : DSK.value[ var ∘ embT ] τ₂} →
                 DSK.SubstV v₁ v v₂ →
                 DS.SubstV {var} (λ x → embV (v₁ x)) (embV v) (embV v₂)
  lemma-SubstV DSK.sVar= = DS.sVar=
  lemma-SubstV DSK.sVar≠ = DS.sVar≠
  lemma-SubstV DSK.sNum = DS.sNum
  lemma-SubstV DSK.sBol = DS.sBol
  lemma-SubstV (DSK.sFun sub) = DS.sFun (λ x → lemma-Subst (sub x))
  lemma-SubstV (DSK.sShift id) = DS.sShift (emb-id-cont-type id)
  lemma-SubstV DSK.sShift0 = DS.sShift0

  -- e₁[x:=v] = e₂
  lemma-Subst : {var : DS.Ty → Set} {Δ : DSK.Delta} →
                {τ β : DSK.Ty} {σβ : DSK.Mc} →
                {e₁ : (var ∘ embT) τ → DSK.term[ var ∘ embT , Δ ]⟨ σβ ⟩ β} →
                {v  : DSK.value[ var ∘ embT ] τ} →
                {e₂ : DSK.term[ var ∘ embT , Δ ]⟨ σβ ⟩ β} →
                DSK.Subst e₁ v e₂ →
                DS.Subst {var} (λ x → embE (e₁ x)) (embV v) (embE e₂)
  lemma-Subst (DSK.sVal ΔΘ sub-c sub-v sub-m) =
    DS.substPlugM (lemma-SubstM ΔΘ sub-m)
      (DS.substPlug (lemma-SubstC sub-c) (DS.sVal (lemma-SubstV sub-v)))
  lemma-Subst (DSK.sApp ΔΘ sub-v₁ sub-v₂ sub-c sub-m) =
    DS.substPlugM (lemma-SubstM ΔΘ sub-m)
      (DS.substPlug (lemma-SubstC sub-c)
                    (DS.sNonVal (DS.sApp (DS.sVal (lemma-SubstV sub-v₁))
                                         (DS.sVal (lemma-SubstV sub-v₂)))))

  -- c₁[x:=v] = c₂
  lemma-SubstC : {var : DS.Ty → Set} {Δ : DSK.Delta} →
                 {τ α τ₁ : DSK.Ty} {σα : DSK.Mc} →
                 {c₁ : (var ∘ embT) τ₁ →
                            DSK.cont[ var ∘ embT , Δ , τ ]⟨ σα ⟩ α} →
                 {v  : DSK.value[ var ∘ embT ] τ₁} →
                 {c₂ : DSK.cont[ var ∘ embT , Δ , τ ]⟨ σα ⟩ α} →
                 DSK.SubstC c₁ v c₂ →
                 DS.SubstC {var} (λ x → embC (c₁ x)) (embV v) (embC c₂)
  lemma-SubstC DSK.sKVar≠ = DS.sHole
  lemma-SubstC (DSK.sKId id) = DS.sHole
  lemma-SubstC {Δ = DSK.K (τ₁ DSK.▷⟨ σ ⟩ τ₂)} (DSK.sKLet sub) =
    DS.sLet DS.sHole (λ x → lemma-Subst (sub x))
  lemma-SubstC {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id} (DSK.sKLet sub) = 
    DS.sLet DS.sHole (λ x → lemma-Subst (sub x))
  
  -- m₁[x:=v] = m₂
  lemma-SubstM : {var : DS.Ty → Set} {Δ : DSK.Delta} {Θ : DSK.Theta} →
                 {τ : DSK.Ty} {σ σβ : DSK.Mc} →
                 (ΔΘ : DSK.Delta-Theta Δ Θ) →
                 {m₁ : (var ∘ embT) τ →
                            DSK.mcont[ var ∘ embT , Θ , σβ ] σ } →
                 {v  : DSK.value[ var ∘ embT ] τ} →
                 {m₂ : DSK.mcont[ var ∘ embT , Θ , σβ ] σ} →
                 DSK.SubstM m₁ v m₂ →
                 DS.SubstM {var}
                           (λ x → embM ΔΘ (m₁ x)) (embV v) (embM ΔΘ m₂)
  lemma-SubstM tt DSK.sGVar≠ = DS.sGHole
  lemma-SubstM {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id}
               tt (DSK.sGCons ΔΘ sub-c sub-m) =
    DS.sGReset (emb-id-cont-type id)
               (lemma-SubstC sub-c) (lemma-SubstM ΔΘ sub-m)

mutual
  -- e₁[k:=c] = e₂
  lemma-CSubst : {var : DS.Ty → Set} {Δ : DSK.Delta}
                 {τ α β : DSK.Ty} {σ σα : DSK.Mc} →
                 {e₁ : DSK.term[ var ∘ embT ,
                                     DSK.K (τ DSK.▷⟨ σα ⟩ α) ]⟨ σ ⟩ β} →
                 {c  : DSK.cont[ var ∘ embT , Δ , τ ]⟨ σα ⟩ α} →
                 {e₂ : DSK.term[ var ∘ embT , Δ ]⟨ σ ⟩ β} →
                 DSK.CSubst e₁ c e₂ →
                 DS.Reduce {var} (DS.plug (embC c) (embE e₁)) (embE e₂)
  lemma-CSubst (DSK.sVal₁ {m = DSK.GVar} csub-c) = lemma-CSubstC csub-c
  lemma-CSubst (DSK.sVal₂ csub-m) = lemma-CSubstM csub-m
  lemma-CSubst (DSK.sApp₁ {m = DSK.GVar} csub-c) = lemma-CSubstC csub-c
  lemma-CSubst (DSK.sApp₂ csub-m) = lemma-CSubstM csub-m

  -- c₁[k:=c] = c₂
  lemma-CSubstC : {var : DS.Ty → Set} {Δ : DSK.Delta}
                  {τ α β τ₁ τ₂ : DSK.Ty} {σ σα σβ : DSK.Mc} →
                  {c₁ : DSK.cont[ var ∘ embT ,
                                      DSK.K (τ₁ DSK.▷⟨ σ ⟩ τ₂) , τ ]⟨ σα ⟩ α} →
                  {c  : DSK.cont[ var ∘ embT , Δ , τ₁ ]⟨ σ ⟩ τ₂ } →
                  {c₂ : DSK.cont[ var ∘ embT , Δ , τ ]⟨ σα ⟩ α} →
                  {e  : DS.term[ var , embT τ DS.▷⟨ embMc σα ⟩ embT α
                                                      ]⟨ embMc σβ ⟩ embT β} →
                  DSK.CSubstC c₁ c c₂ →
                  DS.Reduce {var}
                            (DS.plug (embC c) (DS.plug (embC c₁) e))
                            (DS.plug (embC c₂) e)
  lemma-CSubstC {c = DSK.KVar} DSK.sKVar= = DS.RId
  lemma-CSubstC {c = DSK.KId id} DSK.sKVar= = DS.RId
  lemma-CSubstC {Δ = DSK.K (τ₁ DSK.▷⟨ σ ⟩ τ₂)}
                {c = DSK.KLet e} DSK.sKVar= = DS.RId
  lemma-CSubstC {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id}
                {c = DSK.KLet e} DSK.sKVar= = DS.RId
  lemma-CSubstC {c = DSK.KVar} (DSK.sKLet₂ csub) =
    DS.RLet₂ (λ x → lemma-CSubst (csub x))
  lemma-CSubstC {c = DSK.KId id} (DSK.sKLet₂ csub) = 
    DS.RLet₂ (λ x → lemma-CSubst (csub x))
  lemma-CSubstC {Δ = DSK.K (τ₁ DSK.▷⟨ σ ⟩ τ₂)} {c = DSK.KLet e} {e = e'}
                (DSK.sKLet₂ {e₁ = e₁} {e₂ = e₂} csub) = begin
    DS.NonVal
      (DS.Let
        (DS.NonVal (DS.Let e' (λ x → embE (e₁ x))))
        (λ x → embE (e x)))
    ⟶⟨ DS.RAssoc e' (λ x → embE (e₁ x)) (λ x → embE (e x)) ⟩
    DS.NonVal
       (DS.Let e'
        (λ x → DS.NonVal (DS.Let (embE (e₁ x)) (λ x → embE (e x)))))
    ⟶⟨ DS.RLet₂ (λ x → lemma-CSubst (csub x)) ⟩
    DS.NonVal (DS.Let e' (λ x → embE (e₂ x)))
    ∎
    where open DS.Reasoning
  lemma-CSubstC {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id} {c = DSK.KLet e} {e = e'}
                (DSK.sKLet₂ {e₁ = e₁} {e₂ = e₂} csub) = begin
    DS.NonVal
      (DS.Let
        (DS.NonVal (DS.Let e' (λ x → embE (e₁ x))))
        (λ x → embE (e x)))
    ⟶⟨ DS.RAssoc e' (λ x → embE (e₁ x)) (λ x → embE (e x)) ⟩
    DS.NonVal
       (DS.Let e'
        (λ x → DS.NonVal (DS.Let (embE (e₁ x)) (λ x → embE (e x)))))
    ⟶⟨ DS.RLet₂ (λ x → lemma-CSubst (csub x)) ⟩
    DS.NonVal (DS.Let e' (λ x → embE (e₂ x)))
    ∎
    where open DS.Reasoning

  -- m₁[k:=c] = m₂
  lemma-CSubstM : {var : DS.Ty → Set} {Δ : DSK.Delta} {κ : DSK.CTy}
                  {τ α β : DSK.Ty} {σ σα σβ : DSK.Mc} →
                  {id : DSK.id-cont-type κ} →
                  {m₁ : DSK.mcont[ var ∘ embT ,
                                    DSK.D (DSK.K (τ DSK.▷⟨ σα ⟩ α)) , σ ] σβ} →
                  {c  : DSK.cont[ var ∘ embT , Δ , τ ]⟨ σα ⟩ α} →
                  {m₂ : DSK.mcont[ var ∘ embT , DSK.D Δ , σ ] σβ} →
                  {e : DS.term[ var , embΔ (DSK.• κ id)
                                                    ]⟨ embMc σβ ⟩ embT β} →
                  DSK.CSubstM m₁ c m₂ →
                  DS.Reduce {var}
                            (DS.plug (embC c)
                              (DS.plugM (embM {Δ = DSK.• κ id} tt m₁) e))
                            (DS.plugM (embM {Δ = DSK.• κ id} tt m₂) e)
  lemma-CSubstM {κ = γ DSK.▷⟨ σid ⟩ γ'} (DSK.sGCons₁ {m = DSK.GVar} csub-c) =
    lemma-CSubstC csub-c
  lemma-CSubstM {κ = γ DSK.▷⟨ σid ⟩ γ'} (DSK.sGCons₂ csub-m) =
    lemma-CSubstM csub-m

mutual
  -- e₁[g:=m] = e₂
  lemma-MSubst : {var : DS.Ty → Set} {Δ Δ' : DSK.Delta} {Θ : DSK.Theta}
                 {β : DSK.Ty} {σ σβ : DSK.Mc} →
                 (ΔΘ : DSK.Delta-Theta Δ Θ) →
                 {e₁ : DSK.term[ var ∘ embT , Δ ]⟨ σβ ⟩ β} →
                 {m  : DSK.mcont[ var ∘ embT , Θ , σ ] σβ} →
                 {e₂ : DSK.term[ var ∘ embT , Δ' ]⟨ σ ⟩ β} →
                 (eq : Δ' ≡ Δ DSK.++ Θ) →
                 DSK.MSubst e₁ m eq e₂ →
                 DS.plugM (embM ΔΘ m) (embE e₁)
                 ≡ subst (λ Δ → DS.term[ var , Δ ]⟨ embMc σ ⟩ embT β)
                         (cong embΔ eq)
                         (embE e₂)
  lemma-MSubst ΔΘ eq (DSK.sVal _ _ msub-m) = lemma-MSubstM ΔΘ msub-m
  lemma-MSubst ΔΘ eq (DSK.sApp _ _ _ _ _ _ msub-m) =
    lemma-MSubstM ΔΘ msub-m 
 
  -- m₁[g:=m] = m₂
  lemma-MSubstM : {var : DS.Ty → Set} {Δ : DSK.Delta} {Θ Θ' : DSK.Theta}
                  {β : DSK.Ty} {σ σβ σ' : DSK.Mc} →
                  (ΔΘ  : DSK.Delta-Theta (Δ DSK.++ Θ') Θ) →
                  {ΔΘ' : DSK.Delta-Theta Δ (Θ' DSK.+++ Θ)} →
                  {ΔΘ'' : DSK.Delta-Theta Δ Θ'} →
                  {m₁ : DSK.mcont[ var ∘ embT , Θ' , σ' ] σβ} →
                  {m  : DSK.mcont[ var ∘ embT , Θ , σ ] σ'} →
                  {m₂ : DSK.mcont[ var ∘ embT , Θ' DSK.+++ Θ , σ ] σβ} →
                  {e  : DS.term[ var , embΔ Δ ]⟨ embMc σβ ⟩ embT β} →
                  DSK.MSubstM m₁ m refl m₂ →
                  DS.plugM (embM ΔΘ m) (DS.plugM (embM ΔΘ'' m₁) e)
                  ≡ (DS.plugM (embM ΔΘ' m₂) e)
  lemma-MSubstM ΔΘ {ΔΘ'} DSK.mGVar= rewrite DSK.ΔΘ≡ ΔΘ' ΔΘ = refl
  lemma-MSubstM {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id}
                ΔΘ (DSK.mGCons _ _ msub-m) = lemma-MSubstM ΔΘ msub-m


-- RBetaLet
redBetaLet : {var : DS.Ty → Set} {Δ : DSK.Delta} {Θ : DSK.Theta} →
             {τ β : DSK.Ty} {σ σβ : DSK.Mc} →
             (ΔΘ : DSK.Delta-Theta Δ Θ) →
             {e₁  : (var ∘ embT) τ → DSK.term[ var ∘ embT , Δ ]⟨ σ ⟩ β} →
             {v   : DSK.value[ var ∘ embT ] τ} →
             {e₁' : DSK.term[ var ∘ embT , Δ ]⟨ σ ⟩ β} →
             {m   : DSK.mcont[ var ∘ embT , Θ , σβ ] σ} →
             {e₂  : DSK.term[ var ∘ embT , Δ DSK.++ Θ ]⟨ σβ ⟩ β} →
             DSK.Subst e₁ v e₁' →
             DSK.MSubst e₁' m refl e₂ →
             DS.Reduce {var} 
               (DS.plugM (embM ΔΘ m)
                         (DS.plug (embC (DSK.KLet e₁)) (DS.Val (embV v))))
               (embE e₂)
redBetaLet {Δ = DSK.K (τ₁ DSK.▷⟨ σ ⟩ τ₂)}
           ΔΘ {e₁} {v} {e₁'} {m} {e₂} sub msub = begin
  DS.plugM (embM ΔΘ m) (DS.plug (embC (DSK.KLet e₁)) (DS.Val _))
  ⟶⟨ DS.reducePlugM (embM ΔΘ m) (DS.RBetaLet _ _ _ (lemma-Subst sub)) ⟩
  DS.plugM (embM ΔΘ m) (embE e₁')
  ≡⟨ lemma-MSubst ΔΘ refl msub ⟩
  embE e₂
  ∎
  where open DS.Reasoning
redBetaLet {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id}
           ΔΘ {e₁} {v} {e₁'} {m} {e₂} sub msub = begin
  DS.plugM (embM ΔΘ m) (DS.plug (embC (DSK.KLet e₁)) (DS.Val _))
  ⟶⟨ DS.reducePlugM (embM ΔΘ m) (DS.RBetaLet _ _ _ (lemma-Subst sub)) ⟩
  DS.plugM (embM ΔΘ m) (embE e₁')
  ≡⟨ lemma-MSubst ΔΘ refl msub ⟩
  embE e₂
  ∎
  where open DS.Reasoning


-- main theorem
mutual
  -- DSKの値 v,w について v→w ならば、v♮ → w♮
  correctV : {var : DS.Ty → Set} → {τ : DSK.Ty} {β : DS.Ty} {σβ : DS.Mc} →
             {v w : DSK.value[ var ∘ embT ] τ} →
             DSK.ReduceV v w →
             DS.Reduce {var} {β} {σβ = σβ} (DS.Val (embV v)) (DS.Val (embV w))
  correctV {w = w} DSK.REtaV = DS.REtaV (embV w)
  correctV (DSK.RFun red) = DS.RFun (λ x → correctE (red x))
  correctV DSK.RId = DS.RId
  correctV (DSK.RTrans red-v₁ red-v₂) =
    DS.RTrans (correctV red-v₁) (correctV red-v₂)

  -- DSK項 e,e' について e→e' ならば、e# → e'#
  correctE : {var : DS.Ty → Set} {Δ : DSK.Delta} {β : DSK.Ty} {σβ : DSK.Mc} →
             {e e' : DSK.term[ var ∘ embT , Δ ]⟨ σβ ⟩ β} →
             DSK.Reduce e e' →
             DS.Reduce {var} (embE e) (embE e')
  correctE (DSK.RBetaV ΔΘ {e₁} {c = c} {m} {e₁'} {e₁''} {e₂} sub csub msub) = begin
    DS.plugM (embM ΔΘ m)
       (DS.plug (embC c)
        (DS.NonVal (DS.App (DS.Val (DS.Fun (λ x → embE (e₁ x)))) (DS.Val _))))
    ⟶⟨ DS.reducePlugM 
          (embM ΔΘ m)
          (DS.reducePlug (embC c) (DS.RBetaV _ _ _ (lemma-Subst sub))) ⟩
    DS.plugM (embM ΔΘ m) (DS.plug (embC c) (embE e₁'))
    ⟶⟨ DS.reducePlugM (embM ΔΘ m) (lemma-CSubst csub) ⟩
    DS.plugM (embM ΔΘ m) (embE e₁'')
    ≡⟨ lemma-MSubst ΔΘ refl msub ⟩
    embE e₂
    ∎
    where open DS.Reasoning
  correctE (DSK.RBetaLet ΔΘ sub msub) = redBetaLet ΔΘ sub msub
  correctE (DSK.RShift id₁ id₂ {w} {j} {DSK.GCons ΔΘ c m}) =
    DS.reducePlugM (embM ΔΘ m)
      (DS.reducePlug (embC c)
                     (DS.RShift (emb-id-cont-type id₁) (emb-id-cont-type id₂)
                                (embV w) (embC j)))
  correctE (DSK.RShift0 ΔΘ id {w} {j} {c} {m}) =
    DS.reducePlugM (embM ΔΘ m)
      (DS.reducePlug (embC c)
                     (DS.RShift0 (emb-id-cont-type id) (embV w) (embC j)))
  correctE (DSK.RReset ΔΘ {v} {c} {m}) = 
    DS.reducePlugM (embM ΔΘ m) (DS.reducePlug (embC c) (DS.RReset (embV v)))
  correctE (DSK.RVal₁ ΔΘ {m = m} red-c) = 
    DS.reducePlugM (embM ΔΘ m) (correctC red-c)
  correctE (DSK.RVal₂ ΔΘ {c} {m = m} red-v) =
    DS.reducePlugM (embM ΔΘ m) (DS.reducePlug (embC c) (correctV red-v))
  correctE (DSK.RVal₃ ΔΘ red-m) = correctM ΔΘ red-m
  correctE (DSK.RApp₁ ΔΘ {c = c} {m} red-v) = 
    DS.reducePlugM (embM ΔΘ m)
                   (DS.reducePlug (embC c) (DS.RApp₁ (correctV red-v)))
  correctE (DSK.RApp₂ ΔΘ {c = c} {m} red-v) = 
    DS.reducePlugM (embM ΔΘ m)
                   (DS.reducePlug (embC c) (DS.RApp₂ (correctV red-v)))
  correctE (DSK.RApp₃ ΔΘ {m = m} red-c) =
    DS.reducePlugM (embM ΔΘ m) (correctC red-c)
  correctE (DSK.RApp₄ ΔΘ red-m) = correctM ΔΘ red-m
  correctE DSK.RId = DS.RId
  correctE (DSK.RTrans red₁ red₂) = 
    DS.RTrans (correctE red₁) (correctE red₂)
  
  -- DSKの継続 c,c' について c→c' ならば、c♭[e] → c'♭[e]
  correctC : {var : DS.Ty → Set} {τ₃ : DS.Ty} {σ₂ : DS.Mc}
             {Δ : DSK.Delta} {τ₁ τ₂ : DSK.Ty} {σ₁ : DSK.Mc} →
             {c c' : DSK.cont[ var ∘ embT , Δ , τ₁ ]⟨ σ₁ ⟩ τ₂} →
             {e : DS.term[ var , embT τ₁ DS.▷⟨ embMc σ₁ ⟩ embT τ₂ ]⟨ σ₂ ⟩ τ₃} →
             DSK.ReduceC c c' →
             DS.Reduce (DS.plug (embC c) e) (DS.plug (embC c') e)
  correctC {c' = DSK.KVar} {e} DSK.REtaLet = DS.REtaLet e
  correctC {c' = DSK.KId id} {e} DSK.REtaLet = DS.REtaLet e
  correctC {Δ = DSK.K (τ₁ DSK.▷⟨ σ ⟩ τ₂)} {c' = DSK.KLet e₁} DSK.REtaLet =
    DS.RLet₂ (λ x → DS.RBetaLet _ _ _ (lemma-Subst {e₁ = e₁} lemma-Var-subst))
  correctC {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id} {c' = DSK.KLet e₁} DSK.REtaLet =
    DS.RLet₂ (λ x → DS.RBetaLet _ _ _ (lemma-Subst {e₁ = e₁} lemma-Var-subst))
  correctC {Δ = DSK.K (τ₁ DSK.▷⟨ σ ⟩ τ₂)} (DSK.RKLet red) =
    DS.RLet₂ (λ x → correctE (red x))
  correctC {Δ = DSK.• (γ DSK.▷⟨ σid ⟩ γ') id} (DSK.RKLet red) = 
    DS.RLet₂ (λ x → correctE (red x))
  correctC DSK.RId = DS.RId
  correctC (DSK.RTrans red-c₁ red-c₂) = 
    DS.RTrans (correctC red-c₁) (correctC red-c₂)
  
  -- DSKのメタ継続 m,m' について m→m' ならば、m♭♭[e] → m'♭♭[e]
  correctM : {var : DS.Ty → Set} {Δ : DSK.Delta} {Θ : DSK.Theta} →
             {β : DS.Ty} {σ σβ : DSK.Mc} →
             (ΔΘ : DSK.Delta-Theta Δ Θ) →
             {m m' : DSK.mcont[ var ∘ embT , Θ , σβ ] σ} →
             {e : DS.term[ var , embΔ Δ ]⟨ embMc σ ⟩ β} →
             DSK.ReduceM m m' →
             DS.Reduce (DS.plugM (embM ΔΘ m) e) (DS.plugM  (embM ΔΘ m') e)
  correctM {Δ = DSK.• (γ DSK.▷⟨ σ' ⟩ γ') id} tt (DSK.RGCons₁ ΔΘ {m = m} red-c) =
    DS.reducePlugM (embM ΔΘ m) (correctC red-c)
  correctM {Δ = DSK.• (γ DSK.▷⟨ σ' ⟩ γ') id} tt (DSK.RGCons₂ ΔΘ red-m) =
    correctM ΔΘ red-m