92 lines
2.4 KiB
Plaintext
92 lines
2.4 KiB
Plaintext
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);
|
|
} |