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
|
/*
Here, we define infinite streams with some functions and prove a few
properties, drawing from:
Daniel Hausmann, Till Mossakowski and Lutz Schroder:
Iterative Circular Coinduction for CoCasl in Isabelle/HOL.
Some proofs are automatic (EvenZipLemma), whereas some others require a single
recursive call to be made explicitly.
Note that the automatically inserted parallel statement
is in principle strong enough in all cases above, but the incompletness
of reasoning with quantifiers in SMT solvers make the explicit calls
necessary.
*/
codatatype Stream<T> = Cons(hd: T, tl: Stream);
function zip(xs: Stream, ys: Stream): Stream
{ Cons(xs.hd, Cons(ys.hd, zip(xs.tl, ys.tl))) }
function even(xs: Stream): Stream
{ Cons(xs.hd, even(xs.tl.tl)) }
function odd(xs: Stream): Stream
{ even(xs.tl) }
comethod EvenOddLemma(xs: Stream)
ensures zip(even(xs), odd(xs)) == xs;
{ EvenOddLemma(xs.tl.tl); }
comethod EvenZipLemma(xs:Stream, ys:Stream)
ensures even(zip(xs, ys)) == xs;
{ /* Automatic. */ }
function bzip(xs: Stream, ys: Stream, f:bool) : Stream
{ if f then Cons(xs.hd, bzip(xs.tl, ys, !f))
else Cons(ys.hd, bzip(xs, ys.tl, !f)) }
comethod BzipZipLemma(xs:Stream, ys:Stream)
ensures zip(xs, ys) == bzip(xs, ys, true);
{ BzipZipLemma(xs.tl, ys.tl); }
/*
More examples from CoCasl.
*/
function const(n:int): Stream<int>
{
Cons(n, const(n))
}
function blink(): Stream<int>
{
Cons(0, Cons(1, blink()))
}
comethod BzipBlinkLemma()
ensures zip(const(0), const(1)) == blink();
{
BzipBlinkLemma();
}
function zip2(xs: Stream, ys: Stream): Stream
{
Cons(xs.hd, zip2(ys, xs.tl))
}
comethod Zip201Lemma()
ensures zip2(const(0), const(1)) == blink();
{
Zip201Lemma();
}
comethod ZipZip2Lemma(xs:Stream, ys:Stream)
ensures zip(xs, ys) == zip2(xs, ys);
{
ZipZip2Lemma(xs.tl, ys.tl);
}
function bswitch(xs: Stream, f:bool) : Stream
{
if f then Cons(xs.tl.hd, bswitch(Cons(xs.hd, xs.tl.tl), !f))
else Cons(xs.hd, bswitch(xs.tl, !f))
}
comethod BswitchLemma(xs:Stream)
ensures zip(odd(xs), even(xs)) == bswitch(xs, true);
{
BswitchLemma(xs.tl.tl);
}
comethod Bswitch2Lemma(xs:Stream, ys:Stream)
ensures zip(xs, ys) == bswitch(zip(ys, xs), true);
{
Bswitch2Lemma(xs.tl, ys.tl);
}
|
