datatype Expr = Const(nat) | Var(string) | Node(op: Op, args: List<Expr>)

datatype Op = Add | Mul

datatype List<T> = Nil | Cons(head: T, tail: List<T>)

function Eval(e: Expr, env: map<string, nat>): nat
  requires GoodEnv(e, env)
{
  match e
  case Const(c) => c
  case Var(s) => env[s]
  case Node(op, args) => EvalList(op, args, env)
}

/* E.4.9 => The default decreases clause use lexicographical ordering of the arguments.
This implies the following decreases clause:
    decreases op, args, env

But as "op" is either Add or Mul which and does not have fixed order in a list<Expr>
it jumps around.
for example 10 * 5 + 3 * 10. 
=> Node(Mul, Cons(Const(10), Cons()))

*/

function EvalList(args: List<Expr>, op: Op, 
                  env: map<string, nat>): nat
  decreases args
  requires GoodEnvList(args, env)
{
  match args
  case Nil =>
    (match op case Add => 0 case Mul => 1)
  case Cons(e, tail) =>
    var v0, v1 := Eval(e, env), EvalList(tail, op, env);
    match op
    case Add => v0 + v1
    case Mul => v0 * v1
}

predicate GoodEnv(e: Expr, env: map<string, nat>) {
  match e
  case Const(_) => true
  case Var(s) => s in env.Keys
  case Node(_, args) => GoodEnvList(args, env)
}

predicate GoodEnvList(args: List<Expr>, env: map<string, nat>)
{
  match args
  case Nil => true
  case Cons(e, tail) => GoodEnv(e, env) && GoodEnvList(tail, env)
}

function Substitute(e: Expr, n: string, c: nat): Expr
{
  match e
  case Const(_) => e
  case Var(s) => if s == n then Const(c) else e
  case Node(op, args) => Node(op, SubstituteList(args, n,
                                                 c))
}
function SubstituteList(es: List<Expr>, n: string, c: nat):
  List<Expr>
{
  match es
  case Nil => Nil
  case Cons(e, tail) =>
    Cons(Substitute(e, n, c), SubstituteList(tail, n, c))
}

lemma {:induction false} EvalSubstitute(e: Expr, n: string, c: nat, env: map<string, nat>)
    ensures Eval(Substitute(e, n, c), env) == Eval(e, env[n:=c])
{
    match e
    case Const(_) =>
    case Var(_) =>
    case Node(op, args) =>
        EvalSubstituteList(args, op, n, c, env);
}

lemma {:induction false} EvalSubstituteList(
    args: List<Expr>, op: Op, n: string, c: nat, env: map<string, nat>)
    ensures EvalList(SubstituteList(args, n, c), op, env) == EvalList(args, op, env[n:= c])
{
    match args
    case Nil =>
    case Cons(e, tail) =>
        EvalSubstitute(e, n, c, env);
        EvalSubstituteList(tail, op, n, c, env);
}