blob: 432d107a9c25744ae33f24ec3f41fbe3874a5d84 (
plain)
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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
datatype Tree<T> = Leaf(T) | Node(Tree, Tree)
function {:opaque} size(t: Tree): nat
{
match t
case Leaf(_) => 1
case Node(left, right) => 1 + size(left) + size(right)
}
function {:opaque} mirror<T>(t: Tree<T>): Tree<T>
{
match t
case Leaf(_) => t
case Node(left, right) => Node(mirror(right), mirror(left))
}
lemma {:induction false} MirrorSize(t: Tree)
ensures size(mirror(t)) == size(t);
{
match t {
case Leaf(x) =>
calc {
size(mirror(Leaf(x)));
== { reveal_mirror(); }
size(Leaf(x));
}
case Node(left, right) =>
calc {
size(mirror(Node(left, right)));
== { reveal_mirror(); }
size(Node(mirror(right), mirror(left)));
== { reveal_size(); }
1 + size(mirror(right)) + size(mirror(left));
== { MirrorSize(right); MirrorSize(left); } // induction hypothesis
1 + size(right) + size(left);
== { reveal_size(); }
size(Node(left, right));
}
}
}
|