Test/dafny0/CoPredicates.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
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58

codatatype Stream<T> = Cons(head: T, tail: Stream);

function Upward(n: int): Stream<int>
{
  Cons(n, Upward(n + 1))
}

copredicate Pos(s: Stream<int>)
{
  0 < s.head && Pos(s.tail)
}

copredicate X(s: Stream)
{
  X(s)
}

ghost method AlwaysLemma(s: Stream)
  ensures X(s);
{
}

function Doubles(n: int): Stream<int>
{
  Cons(2*n, Doubles(n + 1))
}

copredicate Even(s: Stream<int>)
{
  s.head % 2 == 0 && Even(s.tail)
}

ghost method Lemma0(n: int)
  ensures Even(Doubles(n));
{
}

function UpwardBy2(n: int): Stream<int>
{
  Cons(n, UpwardBy2(n + 2))
}

ghost method Lemma1(n: int)
  ensures Even(UpwardBy2(2*n));  // error:  this is true, but Dafny can't prove it
{
}

function U2(n: int): Stream<int>
  requires n % 2 == 0;
{
  UpwardBy2(n)
}

ghost method Lemma2(n: int)
  ensures Even(UpwardBy2(2*n));  // this is true, but Dafny can't prove it
{
  assert Even(U2(2*n));  // ... thanks to this lemma
}