1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
datatype List {
Nil;
Cons(Expr, List);
}
datatype Expr {
Const(int);
Var(int);
Nary(int, List);
}
static function Subst(e: Expr, v: int, val: int): Expr
decreases e;
{
match e
case Const(c) => e
case Var(x) => if x == v then #Expr.Const(val) else e
case Nary(op, args) => #Expr.Nary(op, SubstList(args, v, val))
}
static function SubstList(l: List, v: int, val: int): List
decreases l;
{
match l
case Nil => l
case Cons(e, tail) => #List.Cons(Subst(e, v, val), SubstList(tail, v, val))
}
static ghost method Theorem(e: Expr, v: int, val: int)
ensures Subst(Subst(e, v, val), v, val) == Subst(e, v, val);
decreases e;
{
match e {
case Const(c) =>
case Var(x) =>
case Nary(op, args) =>
call Lemma(args, v, val);
}
}
static ghost method Lemma(l: List, v: int, val: int)
ensures SubstList(SubstList(l, v, val), v, val) == SubstList(l, v, val);
decreases l;
{
match l {
case Nil =>
case Cons(e, tail) =>
call Theorem(e, v, val);
call Lemma(tail, v, val);
}
}
// -------------------------------
datatype Expression {
Const(int);
Var(int);
Nary(int, seq<Expression>);
}
static function Substitute(e: Expression, v: int, val: int): Expression
decreases e, true;
{
match e
case Const(c) => e
case Var(x) => if x == v then #Expression.Const(val) else e
case Nary(op, args) => #Expression.Nary(op, SubstSeq(e, args, v, val))
}
static function SubstSeq(/*ghost*/ parent: Expression,
q: seq<Expression>, v: int, val: int): seq<Expression>
requires (forall a :: a in q ==> a < parent);
decreases parent, false, q;
{
if q == [] then [] else
SubstSeq(parent, q[..|q|-1], v, val) + [Substitute(q[|q|-1], v, val)]
}
static ghost method TheoremSeq(e: Expression, v: int, val: int)
ensures Substitute(Substitute(e, v, val), v, val) == Substitute(e, v, val);
decreases e, true;
{
match e {
case Const(c) =>
case Var(x) =>
case Nary(op, args) =>
ghost var seArgs := SubstSeq(e, args, v, val);
call LemmaSeq(e, args, v, val);
ghost var se := Substitute(e, v, val);
ghost var seArgs2 := SubstSeq(se, seArgs, v, val);
call LemmaSeq(se, seArgs, v, val);
var N := |args|;
var j := 0;
while (j < N)
invariant j <= N;
invariant (forall k :: 0 <= k && k < j ==> seArgs2[k] == seArgs[k]);
{
call TheoremSeq(args[j], v, val);
j := j + 1;
}
assert seArgs == seArgs2;
}
}
static ghost method LemmaSeq(ghost parent: Expression, ghost q: seq<Expression>,
v: int, val: int)
requires (forall a :: a in q ==> a < parent);
ensures |SubstSeq(parent, q, v, val)| == |q|;
ensures (forall k :: 0 <= k && k < |q| ==>
SubstSeq(parent, q, v, val)[k] == Substitute(q[k], v, val));
decreases q;
{
if (q == []) {
} else {
call LemmaSeq(parent, q[..|q|-1], v, val);
}
}
|
