Test/dafny3/OpaqueTrees.dfy


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));
      }
  }
}