module M2M where

--  Code accompanying "From Math to Machine: A formal derivation of an
--  executable Krivine machine"
-- 
--  Copyright (c) 2011 Wouter Swierstra.
--  All rights reserved.

module Prelude where

  id : forall {a : Set} -> a -> a
  id x = x

  data Empty : Set where

  magic : forall {a : Set} -> Empty -> a
  magic ()

  record Unit : Set where

  unit : Unit
  unit = record {}

  data Pair (a b : Set) : Set where
    _,_ : a -> b -> Pair a b

  fst : forall {a b} -> Pair a b -> a
  fst (x , _) = x

  snd : forall {a b} -> Pair a b -> b
  snd (_ , y) = y

  data List (a : Set) : Set where
    Nil : List a
    Cons : a -> List a -> List a

  postulate
    Level : Set
    zero  : Level
    suc   : Level  Level
    _⊔_   : Level  Level  Level

  {-#  COMPILED_TYPE Level ()      #-}
  {-#  COMPILED zero ()            #-}
  {-#  COMPILED suc  (\_ -> ())    #-}
  {-#  COMPILED _⊔_  (\_ _ -> ())  #-}

  {-#  BUILTIN LEVEL     Level  #-}
  {-#  BUILTIN LEVELZERO zero   #-}
  {-#  BUILTIN LEVELSUC  suc    #-}
  {-#  BUILTIN LEVELMAX  _⊔_    #-}

  data _==_ {i : Level} {a : Set i} (x : a) : a -> Set i where
    Refl : x == x

  infix 6 _==_

  sym : {a : Set} {x y : a} -> x == y -> y == x
  sym Refl = Refl

  cong : {a b : Set} {x y : a} -> (f : a -> b) -> x == y -> f x == f y
  cong f Refl = Refl

  data Exists (a : Set) (b : a -> Set) : Set where
    Witness : (x : a) -> b x -> Exists a b

  fsts : forall {a b} -> Exists a b -> a
  fsts (Witness x _) = x

  snds : forall {a b} -> (x : Exists a b) -> (b (fsts x))
  snds (Witness _ y) = y

  {-#  BUILTIN EQUALITY _==_  #-}
  {-#  BUILTIN REFL Refl  #-}  

--  ******************************************* --
--                 Basic Terms                  --
--  ******************************************* --
module Terms where

  open Prelude

  data Ty : Set where
    O : Ty
    _=>_ : Ty -> Ty -> Ty

  Context : Set
  Context = List Ty

  data Ref : Context -> Ty -> Set where
    Top : forall {G u} -> Ref (Cons u G) u
    Pop : forall {G u v} -> Ref G u -> Ref (Cons v G) u

  data Term : Context -> Ty -> Set where
    Lam : forall { G u v} -> Term (Cons u G) v -> Term G (u => v)
    App : forall { G u v} -> Term G (u => v) -> Term G u -> Term G v
    Var : forall { G u} -> Ref G u -> Term G u

  mutual

    data Closed : Ty -> Set where
      Closure : forall { G u} -> Term G u -> Env G -> Closed u
      Clapp : forall { u v} -> Closed (u => v) -> Closed u -> Closed v

    data Env : Context -> Set where
      Nil : Env Nil
      _·_ : forall { G u} -> Closed u -> Env G -> Env (Cons u G)

  isVal : forall {u} -> Closed u -> Set
  isVal (Closure (Lam body) env) = Unit
  isVal _ = Empty

  data Value (u : Ty) : Set where
    Val : (c : Closed u) -> isVal c -> Value u

--  ******************************************* --
--            Redex and contraction             --
--  ******************************************* --
module Redex where

  open Prelude
  open Terms  

  data Redex : Ty -> Set where
    Lookup : forall { G u} -> Ref G u -> Env G -> Redex u
    App : forall { G u v} -> Term G (u => v) -> Term G u -> Env G -> Redex v
    Beta : forall { G u v} -> Term (Cons u G) v -> Env G -> Closed u -> Redex v

  fromRedex : forall { u} -> Redex u -> Closed u
  fromRedex (Lookup i env) = Closure (Var i) env
  fromRedex (App f x env) = Closure (App f x) env
  fromRedex (Beta body env arg) = Clapp (Closure (Lam body) env) arg

  _!_ : forall { G u} -> Env G -> Ref G u -> Closed u
  Nil ! ()
  (x · _)  ! Top = x  
  (x · xs) ! Pop r = xs ! r

  contract : forall { u} -> Redex u -> Closed u
  contract (Lookup i env) = env ! i
  contract (App f x env) = Clapp (Closure f env) (Closure x env)
  contract (Beta body env arg) = Closure body (arg · env)

  data EvalContext : Ty -> Ty -> Set where
    MT : forall { u} -> EvalContext u u
    ARG : forall { u v w} -> Closed u -> EvalContext v w -> EvalContext (u => v) w

  plug : forall {u v} -> EvalContext u v -> Closed u -> Closed v
  plug MT f = f
  plug (ARG x ctx) f = plug ctx (Clapp f x)

  data Decomposition : forall {u} -> Closed u -> Set where
     Val : forall {u v G} -> (body : Term (Cons u G) v) -> (env : Env G) -> 
       Decomposition (Closure (Lam body) env)
     Decompose : forall {v u} -> (r : Redex u) -> (ctx : EvalContext u v) -> 
       Decomposition (plug ctx (fromRedex r))

  mutual

    load : forall { u v} -> (ctx : EvalContext u v) (c : Closed u) -> Decomposition (plug ctx c)
    load ctx (Closure (Lam body) env) = unload ctx body env
    load ctx (Closure (App f x) env) = Decompose (App f x env) ctx
    load ctx (Closure (Var i) env) = Decompose (Lookup i env) ctx
    load ctx (Clapp f x) = load (ARG x ctx) f

    unload : forall { u v w G} -> (ctx : EvalContext (u => v) w) (body : Term (Cons u G) v) (env : Env G) 
      -> Decomposition (plug ctx (Closure (Lam body) env))
    unload MT body env = Val body env
    unload (ARG arg ctx) body env = Decompose (Beta body env arg) ctx

  decompose : forall {u} -> (c : Closed u) -> Decomposition c
  decompose c = load MT c

  headReduce : forall {u} -> Closed u -> Closed u
  headReduce c with decompose c
  headReduce .(Closure (Lam body) env) | Val body env = Closure (Lam body) env
  headReduce .(plug ctx (fromRedex redex)) | Decompose redex ctx = plug ctx (contract redex)

  --  ******************************************* --
  --          Lemmas about decomposition          --
  --  ******************************************* --

  decomposePlug : forall {u v} -> (ctx : EvalContext u v) (c : Closed u) ->
    decompose (plug ctx c) == load ctx c
  decomposePlug MT c = Refl
  decomposePlug (ARG x ctx) t 
    rewrite decomposePlug ctx (Clapp t x) = Refl

  decomposeRedex : forall {u v} -> (ctx : EvalContext u v) (r : Redex u) ->
    load ctx (fromRedex r) == Decompose r ctx
  decomposeRedex MT (Lookup i env) = Refl
  decomposeRedex (ARG arg ctx) (Lookup i env) = Refl
  decomposeRedex MT (App f x env) = Refl
  decomposeRedex (ARG arg ctx) (App f x env) = Refl
  decomposeRedex MT (Beta body env x) = Refl
  decomposeRedex (ARG arg ctx) (Beta body env x) = Refl

  headReducePlug : forall {u v} -> (ctx : EvalContext u v) (r : Redex u) ->
    headReduce (plug ctx (fromRedex r)) == plug ctx (contract r)
  headReducePlug ctx r 
    rewrite decomposePlug ctx (fromRedex r)
      | decomposeRedex ctx r = Refl


  --  ******************************************* --
  --                The Snoc View                 --
  --  ******************************************* --

  snoc : forall {u v w} -> EvalContext u (v => w) -> Closed v -> EvalContext u w
  snoc MT u = ARG u MT
  snoc (ARG arg ctx) u = ARG arg (snoc ctx u)

  data SnocView : {u v : Ty} -> EvalContext u v -> Set where
    Nil : forall {u} -> SnocView {u} {u} MT
    Snoc : forall {u v w} -> (x : Closed v) (ctx : EvalContext u (v => w)) -> SnocView (snoc ctx x)

  viewSnoc : forall {u v} -> (ctx : EvalContext u v) -> SnocView ctx
  viewSnoc MT = Nil
  viewSnoc (ARG arg ctx) with viewSnoc ctx
  viewSnoc (ARG arg .MT) | Nil = Snoc arg MT
  viewSnoc (ARG arg .(snoc ctx x)) | Snoc x ctx = Snoc x (ARG arg ctx)

  --  The snocClapp function is the main property of snoc that we use
  snocClapp : forall {u v w} ->
     (ctx : EvalContext u (v => w)) (x : Closed v) -> 
     (t : Closed u) ->
     plug (snoc ctx x) t == Clapp (plug ctx t) x
  snocClapp MT x t = Refl
  snocClapp (ARG arg ctx) x t rewrite snocClapp ctx x (Clapp t arg) = Refl

  --  Some useful auxiliary properties of equalities
  clappL : forall {u v} -> {f f' : Closed (u => v)} {x x' : Closed u} ->
    Clapp f x == Clapp f' x' -> f == f'
  clappL Refl = Refl

  clappR : forall {u v} -> {f f' : Closed (u => v)} {x x' : Closed u} ->
    Clapp f x == Clapp f' x' -> x == x'
  clappR Refl = Refl

  clappU : forall {u u' v} -> {f : Closed (u => v)} {f' : Closed (u' => v)} {x : Closed u} {x' : Closed u'} ->
    Clapp f x == Clapp f' x' -> u == u'
  clappU Refl = Refl

  --  ******************************************* --
  --     The property needed in lemma1            --
  --  ******************************************* --

  headReduceLemma : forall {u v} -> (f : Closed (u => v)) (x : Closed u) (fx : Closed v) ->
     (Clapp f x == fx) ->
     (isVal f -> Empty) ->
     headReduce fx == Clapp (headReduce f) x
  headReduceLemma f x fx eq p with decompose fx
  headReduceLemma f x ._ () p | Val body env
  headReduceLemma f x .(plug ctx (fromRedex r)) eq p | Decompose r ctx with viewSnoc ctx
  headReduceLemma f x ._ () p | Decompose (Lookup _ _) .MT | Nil
  headReduceLemma f x ._ () p | Decompose (App _ _ _) .MT | Nil
  headReduceLemma f x ._ eq p | Decompose (Beta _ _ _) .MT | Nil with clappU eq
  ... | Refl rewrite (clappL eq) = magic (p unit)
  headReduceLemma f x' ._ eq p | Decompose r .(snoc ctx x) | Snoc x ctx
    rewrite snocClapp ctx x (contract r) | snocClapp ctx x (fromRedex r) with clappU eq
  ... | Refl rewrite clappR eq | clappL eq | headReducePlug ctx r = Refl

--  ******************************************* --
--           Iterated head reduction            --
--  ******************************************* --
module Section4 where

  open Prelude
  open Terms
  open Redex

  data Trace : forall { u} -> {c : Closed u} -> Decomposition c -> Set where
    Done : forall {u v G} -> (body : Term (Cons u G) v) -> (env : Env G) -> Trace (Val body env)
    Step : {u v : Ty} {r : Redex u} {ctx : EvalContext u v} -> Trace (decompose (plug ctx (contract r))) -> Trace (Decompose r ctx)

  iterate : forall { u : Ty} -> {c : Closed u} -> (d : Decomposition c) -> Trace d -> Value u
  iterate (Val body env) (Done .(body) .(env)) = Val (Closure (Lam body) env) unit
  iterate (Decompose r ctx) (Step step) = iterate (decompose (plug ctx (contract r))) step

  Reducible : {u : Ty} -> (t : Closed u) -> Set
  Reducible {O} t = Trace (decompose t)
  Reducible {u => v} t =  Pair  (Trace (decompose t)) 
                                ((x : Closed u) -> Reducible x -> Reducible (Clapp t x))

  ReducibleEnv : forall {G} -> Env G -> Set
  ReducibleEnv Nil = Unit
  ReducibleEnv (x · env) = Pair (Reducible x) (ReducibleEnv env)

  deref : forall {G u} (env : Env G) (r : Ref G u) -> ReducibleEnv env -> Reducible (env ! r)
  deref Nil () _
  deref (x · _) Top (red , _) = red
  deref (_ · env) (Pop i) (_ , redEnv) = deref env i redEnv

  step : forall {u} -> (c : Closed u) -> (t : Trace (decompose (headReduce c))) -> Trace (decompose c)
  step c trace with decompose c
  step ._ trace | Val body env = Done body env
  step ._ trace | Decompose r ctx = Step {r = r} {ctx = ctx} trace

  lemma1 : forall {u} -> (t : Closed u) -> Reducible (headReduce t) -> Reducible t
  lemma1 {O} t red = step t red
  lemma1 {u => v} (Closure (Lam body) env) (_ , red) = 
    (Done body env , \x redX -> red x redX)
  lemma1 {u => v} (Closure (App f x) env) (wn , red) = 
    (step (Closure (App f x) env) wn , \y redY -> lemma1 (Clapp (Closure (App f x) env) y) (red y redY))
  lemma1 {u => v} (Closure (Var i) env) (wn , red) = 
    (step (Closure (Var i) env) wn , λ x redX  lemma1 (Clapp (Closure (Var i) env) x) (red x redX))
  lemma1 {u => v} (Clapp {s} f x) (wn , red) = 
    step (Clapp f x) wn , \y redY -> lemma1 (Clapp (Clapp f x) y) (forceStep y (red y redY))
    where
    forceStep : (y : Closed u) ->
      Reducible (Clapp (headReduce (Clapp f x)) y) -> 
      Reducible (headReduce (Clapp (Clapp f x) y) )
    forceStep y h rewrite headReduceLemma (Clapp f x) y (Clapp (Clapp f x) y) Refl id = h

  lemma2 : forall {G u} -> (t : Term G u) (env : Env G) -> 
    (ReducibleEnv env) -> Reducible (Closure t env)
  lemma2 (Lam {G} {s} {t} body) env redenv = 
    let bodyRed : (term : Closed s) -> Reducible term -> 
                  Reducible (Closure body (term · env))
        bodyRed t redT = lemma2 body (t · env) (redT , redenv)
    in (Done body env ,
        \x redX -> lemma1 (Clapp (Closure (Lam body) env) x) (bodyRed x redX))
  lemma2 (App f x) env redenv =
    let redF : Reducible (Closure f env)
        redF = lemma2 f env redenv
    in let redX : Reducible (Closure x env)
           redX = lemma2 x env redenv
    in lemma1 (Closure (App f x) env) (snd redF (Closure x env) redX)
  lemma2 (Var i) env redenv = 
    let redVar : Reducible (env ! i)
        redVar = deref env i redenv 
    in lemma1 (Closure (Var i) env) redVar

  mutual    
    theorem : forall {u} -> (c : Closed u) -> Reducible c
    theorem (Closure t env) = lemma2 t env (envTheorem env)
    theorem (Clapp f x) = snd (theorem f) x (theorem x)

    envTheorem : forall {G} -> (env : Env G) -> ReducibleEnv env
    envTheorem Nil = unit
    envTheorem (t · ts) = (theorem t , envTheorem ts)

  termination : {u : Ty} -> (c : Closed u) -> Trace (decompose c)
  termination {O} c = theorem c
  termination {u => v} c = fst (theorem c)

  evaluate : forall {u} -> Closed u -> Value u
  evaluate t = iterate (decompose t) (termination t)

--  ******************************************* --
--                    Refocusing                --
--  ******************************************* --
module Section5 where

  open Prelude
  open Terms
  open Redex

  refocus : forall {u v} -> (ctx : EvalContext u v) (c : Closed u) -> Decomposition (plug ctx c)
  refocus MT (Closure (Lam body) env) = Val body env
  refocus (ARG x ctx) (Closure (Lam body) env) = Decompose (Beta body env x) ctx
  refocus ctx (Closure (Var i) env) = Decompose (Lookup i env) ctx
  refocus ctx (Closure (App f x) env) = Decompose (App f x env) ctx
  refocus ctx (Clapp f x) = refocus (ARG x ctx) f

  refocusCorrect : forall { v u} -> (ctx : EvalContext u v) (c : Closed u) -> 
     refocus ctx c == decompose (plug ctx c)

  refocusCorrect MT (Closure (Lam body) env) = Refl
  refocusCorrect (ARG x ctx) (Closure (Lam body) env)
    rewrite decomposePlug ctx (Clapp (Closure (Lam body) env ) x) = Refl
  refocusCorrect MT (Closure (Var i) env) = Refl
  refocusCorrect (ARG x ctx) (Closure (Var i) env) 
    rewrite decomposePlug ctx (Clapp (Closure (Var i) env) x) = Refl
  refocusCorrect MT (Closure (App f x) env) = Refl
  refocusCorrect (ARG arg ctx) (Closure (App f x) env) 
    rewrite decomposePlug ctx (Clapp (Closure (App f x) env) arg) = Refl
  refocusCorrect MT (Clapp f x) = refocusCorrect (ARG x MT) f 
  refocusCorrect (ARG arg ctx) (Clapp f x) = refocusCorrect (ARG x (ARG arg ctx)) f

  data Trace : {u : Ty} {c : Closed u} -> Decomposition c -> Set where
     Done : forall {G u v} -> (body : Term (Cons u G) v) -> (env : Env G) -> Trace (Val body env)
     Step : forall {u v} -> {r : Redex u} {ctx : EvalContext u v} -> Trace (refocus ctx (contract r)) -> Trace  (Decompose r ctx)

  termination : forall {u} -> (c : Closed u) -> Trace (refocus MT c)

  termination t rewrite refocusCorrect MT t = lemma t (Section4.termination t)
    where 
      rewriteStep : forall {u v} -> (ctx : EvalContext u v) (t : Closed u) -> 
        Trace (decompose (plug ctx t)) -> Trace (refocus ctx t)
      rewriteStep ctx t p rewrite refocusCorrect ctx t = p
      lemma : forall {u} -> (t : Closed u) -> Section4.Trace (decompose t) -> Trace (decompose t)
      lemma t p with decompose t
      lemma ._ p | Val body env = Done body env
      lemma {u} .(plug ctx (fromRedex r)) (Section4.Step p) | Decompose r ctx 
        = Step {r = r} {ctx = ctx}  (rewriteStep ctx (contract r) (lemma (plug ctx (contract r)) p))

  iterate : forall {u} -> {c : Closed u} -> (d : Decomposition c) -> Trace d -> Value u
  iterate (Val body env) (Done .(body) .(env)) = Val (Closure (Lam body) env) unit
  iterate (Decompose r ctx) (Step step) = iterate (refocus ctx (contract r)) step

  evaluate : forall {u} -> Closed u -> Value u
  evaluate c = iterate (refocus MT c) (termination c)

  correctness : forall {u} -> {t : Closed u}-> 
    (trace : Trace (refocus MT t)) -> (trace' : Section4.Trace (decompose t)) ->
    iterate (refocus MT t) trace == Section4.iterate (decompose t) trace'

  correctness {u} {t} t1 t2 rewrite refocusCorrect MT t = lemma t t1 t2
    where
    lemma : forall {u} -> (t : Closed u) -> (t1 : Trace (decompose t)) -> (t2 : Section4.Trace (decompose t)) ->
      iterate (decompose t) t1 == Section4.iterate (decompose t) t2
    lemma t t1 t2 with decompose t
    lemma .(Closure (Lam body) env) (Done .body .env) (Section4.Done .body .env) | Val body env = Refl
    lemma .(plug ctx (fromRedex r)) (Step t1) (Section4.Step t2) | Decompose r ctx 
      rewrite refocusCorrect ctx (contract r) = lemma (plug ctx (contract r)) t1 t2

  corollary : forall {u} -> (t : Closed u) -> evaluate t == Section4.evaluate t
  corollary t = correctness (termination t) (Section4.termination t)

--  ******************************************* --
--            The Krivine Machine               --
--  ******************************************* --
module Section6 where

  open Prelude
  open Terms
  open Redex

  mutual
    isValidClosure : forall {u} -> Closed u -> Set
    isValidClosure (Closure t env) = isValidEnv env
    isValidClosure (Clapp f x) = Empty

    isValidEnv : forall {D} -> Env D -> Set
    isValidEnv Nil = Unit
    isValidEnv (c · env) = Pair (isValidClosure c) (isValidEnv env)

  isValidContext : forall {u v} -> EvalContext u v -> Set
  isValidContext MT = Unit
  isValidContext (ARG (Closure t env) ctx) = Pair (isValidEnv env) (isValidContext ctx)
  isValidContext (ARG (Clapp f x) env) = Empty

  getContext : forall {u} -> Exists (Closed u) isValidClosure -> Context
  getContext (Witness (Closure {G} t env) _) = G
  getContext (Witness (Clapp f x) ())

  getEnv : forall {u} -> (c : Exists (Closed u) isValidClosure) -> Env (getContext c)
  getEnv (Witness (Closure t env) p) = env
  getEnv (Witness (Clapp f x) ())

  getTerm : forall {u} -> (c : Exists (Closed u) isValidClosure) -> Term (getContext c) u
  getTerm (Witness (Closure t env) p) = t
  getTerm (Witness (Clapp f x) ())

  lookup : forall {u G} -> Ref G u -> (env : Env G) -> isValidEnv env -> 
    Exists (Closed u) isValidClosure
  lookup Top (Closure t env · _) (p1 , p2) = Witness (Closure t env) p1
  lookup Top (Clapp _ _ · _) (() , _)
  lookup (Pop i) (_ · env) (_ , p) = lookup i env p

  lookupClosure : forall {u G} -> (env : Env G) (i : Ref G u) -> (p : isValidEnv env) ->  
    let c = lookup i env p in
    env ! i == Closure (getTerm c) (getEnv c)
  lookupClosure Nil () p
  lookupClosure (Closure t env · env') Top (y1 , y2) = Refl
  lookupClosure (Clapp f x · env) Top (() , y2)
  lookupClosure (c · env) (Pop i) (_ , p) = lookupClosure env i p

  lookupLemma : forall {u G} -> (env : Env G) (i : Ref G u) (p : isValidEnv env) ->
    isValidEnv (getEnv (lookup i env p))
  lookupLemma Nil () p
  lookupLemma (Closure t env · _) Top (p , _) = p
  lookupLemma (Clapp f x · env) Top (() , p)
  lookupLemma (c · env) (Pop i) (p1 , p2) = lookupLemma env i p2

  data Trace : forall {G u v} -> Term G u -> Env G -> EvalContext u v -> Set where
    Lookup : forall {u v G} -> {ctx : EvalContext u v} {env : Env G} (i : Ref G u) (p : isValidEnv env) -> 
      let c = lookup i env p in
      Trace (getTerm c) (getEnv c) ctx -> Trace (Var i) env ctx
    App : forall { u G v w} -> {env : Env G} {ctx : EvalContext v w} (f : Term G (u => v)) (x : Term G u) ->
      Trace f env (ARG (Closure x env) ctx) ->
      Trace (App f x) env ctx
    Beta : forall {G u v w H} -> {env : Env G} (ctx : EvalContext u w) ->
      (arg : Term H v) -> (argEnv : Env H) ->
      (body : Term (Cons v G) u) -> 
      Trace body (Closure arg argEnv · env) ctx ->
      Trace (Lam body) env (ARG (Closure arg argEnv) ctx)
    Done : forall {G u v} -> {env : Env G} (body : Term (Cons v G) u) -> Trace (Lam body) env MT

  refocus : forall {G u v} -> (ctx : EvalContext u v) (t : Term G u) (env : Env G) ->
   Trace t env ctx -> Value v
  refocus ctx .(Var i) env (Lookup i q step) = 
    let c = lookup i env q in
    refocus ctx (getTerm c) (getEnv c) step
  refocus ctx .(App f x) env (App f x step) 
    = refocus (ARG (Closure x env) ctx) f env step
  refocus .(ARG (Closure arg env') ctx) .(Lam body) env (Beta ctx arg env' body step) 
    = refocus ctx body ((Closure arg env') · env) step
  refocus .(MT) .(Lam body) env (Done body) = Val (Closure (Lam body) env) unit

  invariant : forall { G u v} -> EvalContext u v -> Env G -> Set
  invariant ctx env = Pair (isValidEnv env) (isValidContext ctx)

  termination : forall {u} -> (t : Term Nil u) -> Trace t Nil MT
  termination t = lemma MT t Nil (unit , unit) (Section5.termination (Closure t Nil))
    where
    lemma : forall {G u v} -> (ctx : EvalContext u v) (t : Term G u) (env : Env G) ->
      invariant ctx env -> Section5.Trace (Section5.refocus ctx (Closure t env)) -> 
      Trace t env ctx    

    lemma MT (Lam .body) .env p (Section5.Done body env) = Done body
    lemma MT (App f x) env p (Section5.Step step) = App f x (lemma (ARG (Closure x env) MT) f env ((fst p) , p) step)
    lemma MT (Var i) env (p1 , p2) (Section5.Step step) rewrite lookupClosure env i p1 
      = Lookup i p1 (lemma MT (getTerm (lookup i env p1)) (getEnv (lookup i env p1)) (lookupLemma env i p1 , p2) step)
    lemma (ARG (Closure arg env') ctx) (Lam body) env (p1 , (p2 , p3)) (Section5.Step step) 
      = Beta ctx arg env' body (lemma ctx body ((Closure arg env') · env) ((p2 , p1) , p3) step)
    lemma (ARG (Clapp _ _) ctx) (Lam _) env (_ , ()) (Section5.Step _)
    lemma (ARG arg ctx) (App (Lam body) x) env p (Section5.Step step) 
      = App (Lam body) x (lemma (ARG (Closure x env) (ARG arg ctx)) (Lam body) env ((fst p) , p) step)
    lemma (ARG arg ctx) (App (App f y) x) env p (Section5.Step step) 
      = App (App f y) x (lemma (ARG (Closure x env) (ARG arg ctx)) (App f y) env ((fst p) , p) step)
    lemma (ARG arg ctx) (App (Var i) x) env p (Section5.Step step) 
      rewrite lookupClosure env i (fst p) 
      = let c = lookup i env (fst p) in
        App (Var i) x (lemma (ARG (Closure x env) (ARG arg ctx)) (Var i) env ((fst p) , p) step)
    lemma (ARG arg ctx) (Var i) env p (Section5.Step step) 
      rewrite lookupClosure env i (fst p) 
      = let c = lookup i env (fst p) in
        Lookup i (fst p) (lemma (ARG arg ctx) (getTerm c) (getEnv c) ((lookupLemma env i (fst p)) , (snd p)) step)

  evaluate : forall {u} -> Term Nil u -> Value u
  evaluate t = refocus MT t Nil (termination t)

  correctness :  forall {u v G} -> (ctx : EvalContext u v) (t : Term G u) (env : Env G) ->
   (t1 : Trace t env ctx) -> 
   (t2 : Section5.Trace (Section5.refocus ctx (Closure t env))) ->
   refocus ctx t env t1 == Section5.iterate (Section5.refocus ctx (Closure t env)) t2

  correctness MT .(Var i) env (Lookup i p t1) (Section5.Step t2) 
    rewrite lookupClosure env i p
    = let c = lookup i env p in
      correctness MT (getTerm c) (getEnv c) t1 t2
  correctness MT .(App f x) env (App f x t1) (Section5.Step t2) 
    = correctness (ARG (Closure x env) MT) f env t1 t2
  correctness MT .(Lam body) .env (Done .body) (Section5.Done body env) = Refl
  correctness (ARG arg ctx) .(Var i)  env (Lookup i p t1) (Section5.Step t2) 
    rewrite lookupClosure env i p
    = let c = lookup i env p in
      correctness (ARG arg ctx) (getTerm c) (getEnv c) t1 t2
  correctness (ARG arg ctx) .(App f x) env (App f x t1) (Section5.Step t2) 
    = correctness (ARG (Closure x env) (ARG arg ctx)) f env t1 t2
  correctness (ARG .(Closure arg argEnv) ctx) .(Lam body) env (Beta ._ arg argEnv body t1) (Section5.Step t2) 
    = correctness ctx body (Closure arg argEnv · env) t1 t2

  corollary : forall {u} -> (t : Term Nil u) -> evaluate t == Section5.evaluate (Closure t Nil)
  corollary t =  let trace   = termination t in
                 let trace'  = Section5.termination (Closure t Nil) in
                 correctness MT t Nil trace trace'