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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// A couple of examples from Grigore Rosu and Dorel Lucanu, "Circular coinduction: A proof theoretical
// foundation", CALCO 2009.
codatatype Stream<T> = Cons(head: T, tail: Stream)
// ----- standard examples -----
function zeros(): Stream<int> { Cons(0, zeros()) }
function ones(): Stream<int> { Cons(1, ones()) }
function blink(): Stream<int> { Cons(0, Cons(1, blink())) }
function zip(a: Stream, b: Stream): Stream { Cons(a.head, zip(b, a.tail)) }
colemma BlinkZipProperty()
ensures zip(zeros(), ones()) == blink();
{
BlinkZipProperty();
}
// ----- Thue-Morse sequence -----
datatype Bit = O | I
function bitnot(b: Bit): Bit
{
if b == O then I else O
}
function not(s: Stream<Bit>): Stream<Bit>
{
Cons(bitnot(s.head), not(s.tail))
}
/* Function morse() is essentially this:
function morse(): Stream<int>
{
Cons(0, morseTail())
}
function morseTail(): Stream<int>
{
Cons(1, zip(morseTail(), not(morseTail())))
}
* However, this definition of morseTail() is not allowed in Dafny, because it violates Dafny's
* syntactic guardedness checks. Instead, we give the defining properties of morse() and
* morseTail() as an axiom (that is, an unproved lemma).
*/
function morse(): Stream<Bit>
function morseTail(): Stream<Bit>
lemma MorseProperties()
ensures morse().head == O;
ensures morseTail() == morse().tail;
ensures morseTail().head == I;
ensures morseTail().tail == zip(morseTail(), not(morseTail()));
// We will now define a function f and show that morse() is a fix-point of f.
function f(s: Stream<Bit>): Stream<Bit>
{
Cons(s.head, Cons(bitnot(s.head), f(s.tail)))
}
// The insightful property about f is that it satisfies the following property, which
// we prove by co-induction.
colemma FProperty(s: Stream<Bit>)
ensures f(s) == zip(s, not(s));
{
calc {
zip(s, not(s));
// def. zip
Cons(s.head, zip(not(s), s.tail));
// def. zip
Cons(s.head, Cons(not(s).head, zip(s.tail, not(s).tail)));
}
FProperty(s.tail);
}
// The fix-point theorem now follows easily.
lemma Fixpoint()
ensures f(morse()) == morse();
{
MorseProperties();
FProperty(morseTail());
}
|
