{-# 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 : Set} {Δ : DSK.Delta}
                    {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 : Set} →
                 {v₁ : var → DSK.value[ var ]} →
                 {v  : DSK.value[ var ]} →
                 {v₂ : DSK.value[ var ]} →
                 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 = DS.sShift
  lemma-SubstV DSK.sShift0 = DS.sShift0

  -- e₁[x:=v] = e₂
  lemma-Subst : {var : Set} {Δ : DSK.Delta} →
                {e₁ : var → DSK.term[ var , Δ ]} →
                {v  : DSK.value[ var ]} →
                {e₂ : DSK.term[ var , Δ ]} →
                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 : Set} {Δ : DSK.Delta} →
                 {c₁ : var → DSK.cont[ var , Δ ]} →
                 {v  : DSK.value[ var ]} →
                 {c₂ : DSK.cont[ var , Δ ]} →
                 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 = DS.sHole
  lemma-SubstC {Δ = DSK.K} (DSK.sKLet sub) =
    DS.sLet DS.sHole (λ x → lemma-Subst (sub x))
  lemma-SubstC {Δ = DSK.•} (DSK.sKLet sub) = 
    DS.sLet DS.sHole (λ x → lemma-Subst (sub x))
  
  -- m₁[x:=v] = m₂
  lemma-SubstM : {var : Set} {Δ : DSK.Delta} {Θ : DSK.Theta} →
                 (ΔΘ : DSK.Delta-Theta Δ Θ) →
                 {m₁ : var → DSK.mcont[ var , Θ ]} →
                 {v  : DSK.value[ var ]} →
                 {m₂ : DSK.mcont[ var , Θ ]} →
                 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.•}
               tt (DSK.sGCons ΔΘ sub-c sub-m) =
    DS.sGReset (lemma-SubstC sub-c) (lemma-SubstM ΔΘ sub-m)

mutual
  -- e₁[k:=c] = e₂
  lemma-CSubst : {var : Set} {Δ : DSK.Delta} →
                 {e₁ : DSK.term[ var , DSK.K ]} →
                 {c  : DSK.cont[ var , Δ ]} →
                 {e₂ : DSK.term[ var , Δ ]} →
                 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 : Set} {Δ : DSK.Delta} →
                  {c₁ : DSK.cont[ var , DSK.K ]} →
                  {c  : DSK.cont[ var , Δ ]} →
                  {c₂ : DSK.cont[ var , Δ ]} →
                  {e  : DS.term[ var ]} →
                  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} DSK.sKVar= = DS.RId
  lemma-CSubstC {Δ = DSK.K}
                {c = DSK.KLet e} DSK.sKVar= = DS.RId
  lemma-CSubstC {Δ = DSK.•}
                {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} (DSK.sKLet₂ csub) = 
    DS.RLet₂ (λ x → lemma-CSubst (csub x))
  lemma-CSubstC {Δ = DSK.K} {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.•} {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 : Set} {Δ : DSK.Delta} →
                  {m₁ : DSK.mcont[ var , DSK.D DSK.K ]} →
                  {c  : DSK.cont[ var , Δ ]} →
                  {m₂ : DSK.mcont[ var , DSK.D Δ ]} →
                  {e : DS.term[ var ]} →
                  DSK.CSubstM m₁ c m₂ →
                  DS.Reduce {var}
                            (DS.plug (embC c)
                              (DS.plugM (embM {Δ = DSK.•} tt m₁) e))
                            (DS.plugM (embM {Δ = DSK.•} tt m₂) e)
  lemma-CSubstM (DSK.sGCons₁ {m = DSK.GVar} csub-c) = lemma-CSubstC csub-c
  lemma-CSubstM (DSK.sGCons₂ csub-m) = lemma-CSubstM csub-m

mutual
  -- e₁[g:=m] = e₂
  lemma-MSubst : {var : Set} {Δ Δ' : DSK.Delta} {Θ : DSK.Theta} →
                 (ΔΘ : DSK.Delta-Theta Δ Θ) →
                 {e₁ : DSK.term[ var , Δ ]} →
                 {m  : DSK.mcont[ var , Θ ]} →
                 {e₂ : DSK.term[ var , Δ' ]} →
                 (eq : Δ' ≡ Δ DSK.++ Θ) →
                 DSK.MSubst e₁ m eq e₂ →
                 DS.plugM (embM ΔΘ m) (embE e₁)
                 ≡ subst (λ Δ → DS.term[ var ])
                         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 : Set} {Δ : DSK.Delta} {Θ Θ' : DSK.Theta}
                  (ΔΘ  : DSK.Delta-Theta (Δ DSK.++ Θ') Θ) →
                  {ΔΘ' : DSK.Delta-Theta Δ (Θ' DSK.+++ Θ)} →
                  {ΔΘ'' : DSK.Delta-Theta Δ Θ'} →
                  {m₁ : DSK.mcont[ var , Θ' ]} →
                  {m  : DSK.mcont[ var , Θ ]} →
                  {m₂ : DSK.mcont[ var , Θ' DSK.+++ Θ ]} →
                  {e  : DS.term[ var ]} →
                  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.mGCons _ _ msub-m) = lemma-MSubstM ΔΘ msub-m


-- RBetaLet
redBetaLet : {var : Set} {Δ : DSK.Delta} {Θ : DSK.Theta} →
             (ΔΘ : DSK.Delta-Theta Δ Θ) →
             {e₁  : var → DSK.term[ var , Δ ]} →
             {v   : DSK.value[ var ]} →
             {e₁' : DSK.term[ var , Δ ]} →
             {m   : DSK.mcont[ var , Θ ]} →
             {e₂  : DSK.term[ var , Δ 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}
           ΔΘ {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.•}
           ΔΘ {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 : Set} →
             {v w : DSK.value[ var ]} →
             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 : Set} {Δ : DSK.Delta} →
             {e e' : DSK.term[ var , Δ ]} →
             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 {w = w} {j} {DSK.GCons ΔΘ c m}) =
    DS.reducePlugM (embM ΔΘ m)
      (DS.reducePlug (embC c) (DS.RShift (embV w) (embC j)))
  correctE (DSK.RShift0 ΔΘ {w} {j} {c} {m}) =
    DS.reducePlugM (embM ΔΘ m)
      (DS.reducePlug (embC c) (DS.RShift0 (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 : Set} {Δ : DSK.Delta} →
             {c c' : DSK.cont[ var , Δ ]} →
             {e : DS.term[ var ]} →
             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} {e} DSK.REtaLet = DS.REtaLet e
  correctC {Δ = DSK.K} {c' = DSK.KLet e₁} DSK.REtaLet =
    DS.RLet₂ (λ x → DS.RBetaLet _ _ _ (lemma-Subst {e₁ = e₁} lemma-Var-subst))
  correctC {Δ = DSK.•} {c' = DSK.KLet e₁} DSK.REtaLet =
    DS.RLet₂ (λ x → DS.RBetaLet _ _ _ (lemma-Subst {e₁ = e₁} lemma-Var-subst))
  correctC {Δ = DSK.K} (DSK.RKLet red) =
    DS.RLet₂ (λ x → correctE (red x))
  correctC {Δ = DSK.•} (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 : Set} {Δ : DSK.Delta} {Θ : DSK.Theta} →
             (ΔΘ : DSK.Delta-Theta Δ Θ) →
             {m m' : DSK.mcont[ var , Θ ]} →
             {e : DS.term[ var ]} →
             DSK.ReduceM m m' →
             DS.Reduce (DS.plugM (embM ΔΘ m) e) (DS.plugM  (embM ΔΘ m') e)
  correctM {Δ = DSK.•} tt (DSK.RGCons₁ ΔΘ {m = m} red-c) =
    DS.reducePlugM (embM ΔΘ m) (correctC red-c)
  correctM {Δ = DSK.•} tt (DSK.RGCons₂ ΔΘ red-m) =
    correctM ΔΘ red-m