Idris fast implementation of let evaulation

Let.idr

VarName : Type
VarName = Nat

total
nameEq : (a : VarName) -> (b : VarName) -> Dec (a = b)
nameEq Z Z = Yes Refl
nameEq Z (S k) = No ZnotS
nameEq (S k) Z = No (negEqSym ZnotS)
nameEq (S k) (S j) with (nameEq k j)
  | Yes p = Yes $ cong p
  | No p = No $ \h : (S k = S j) => p $ succInjective k j h

data Lexpr = LN Double | LV VarName | LPlus Lexpr Lexpr | Let VarName Lexpr Lexpr
data Aexpr = AN Double | AV VarName | APlus Aexpr Aexpr

total
inlineReplace : (x : VarName) -> (xdef : Aexpr) -> (expr : Aexpr) -> Aexpr
inlineReplace x xdef (AN y) = AN y
inlineReplace x xdef (AV y) = case nameEq x y of
  (Yes prf) => xdef
  (No contra) => AV y
inlineReplace x xdef (APlus y z) = APlus (inlineReplace x xdef y) (inlineReplace x xdef z)

total
inline : Lexpr -> Aexpr
inline (LN x) = AN x
inline (LV x) = AV x
inline (LPlus x y) = APlus (inline x) (inline y)
inline (Let x xdef expr) = let xdef' = inline xdef
  in inlineReplace x xdef' (inline expr)

St : Type
St = List (VarName, Double)

varVal : St -> VarName -> Double
varVal [] name = 0
varVal ((nm, val) :: xs) name = case nameEq nm name of
  Yes prf => val
  No contra => varVal xs name

varSet : St -> VarName -> Double -> St
varSet [] name val = [(name, val)]
varSet (v@(nm, _) :: xs) name val = case nameEq nm name of
  Yes prf => (nm, val) :: xs
  No contra => v :: varSet xs name val

varSetGetProof : {name : VarName} -> (st : St) -> varVal (varSet st name x) name = x
varSetGetProof {name} [] with (nameEq name name)
  | Yes prf = Refl
  | No contra = ?varSetGetProof_rhs_6
varSetGetProof (x :: xs) = ?varSetGetProof_rhs_2

lval : St -> Lexpr -> Double
lval st (LN x) = x
lval st (LV nm) = varVal st nm
lval st (LPlus x y) = lval st x + lval st y
lval st (Let name def expr) = let
  val = lval st def
  st' = varSet st name val
  in lval st' expr

aval : St -> Aexpr -> Double
aval st (AN x) = x
aval st (AV nm) = varVal st nm
aval st (APlus x y) = aval st x + aval st y

mutual
  inlinePlusProof : (x : Lexpr) -> (y : Lexpr) -> (st : St)
    -> lval st x + lval st y = aval st (inline x) + aval st (inline y)
  inlinePlusProof x y st =
    rewrite inlineProof x st in
    rewrite inlineProof y st in
    Refl

  inlineLetProof : (name : VarName) -> (def : Lexpr) -> (expr : Lexpr) -> (st : St)
    -> lval (varSet st name (lval st def)) expr = aval st (inlineReplace name (inline def) (inline expr))
  inlineLetProof name (LN x) (LN y) st = Refl
  inlineLetProof name (LN x) (LV y) st with (nameEq name y)
    | (Yes prf) = case prf of Refl => varSetGetProof st
    | (No contra) = case st of
      [] => ?hole_1
      (x :: xs) => ?hole_3
  inlineLetProof name (LN x) (LPlus y z) st = ?inlineLetProof_rhs_7
  inlineLetProof name (LN x) (Let y z w) st = ?inlineLetProof_rhs_8
  inlineLetProof name (LV x) expr st = ?inlineLetProof_rhs_2
  inlineLetProof name (LPlus x y) expr st = ?inlineLetProof_rhs_3
  inlineLetProof name (Let x y z) expr st = ?inlineLetProof_rhs_4

  inlineProof : (lexpr : Lexpr) -> (st : St) -> lval st lexpr = aval st (inline lexpr)
  inlineProof (LN x) st = Refl
  inlineProof (LV x) st = Refl
  inlineProof (LPlus x y) st = inlinePlusProof x y st
  inlineProof (Let name def expr) st = inlineLetProof name def expr st