```
module M2M where

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

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 (App f x) env) = Decompose (App f x env) ctx
load ctx (Closure (Var i) env) = Decompose (Lookup i env) ctx

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 .(Closure (Lam body) env) | Val body env = Closure (Lam body) env
headReduce .(plug ctx (fromRedex redex)) | Decompose redex ctx = plug ctx (contract redex)

--  ******************************************* --
--  ******************************************* --

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)
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) ->
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

--  ******************************************* --
--  ******************************************* --
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'
```