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
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
codatatype Stream<T> = Cons(head: T, tail: Stream)
codatatype IList<T> = Nil | ICons(head: T, tail: IList)
// -----------------------------------------------------------------------
copredicate Pos(s: Stream<int>)
{
s.head > 0 && Pos(s.tail)
}
function Up(n: int): Stream<int>
{
Cons(n, Up(n+1))
}
function Inc(s: Stream<int>): Stream<int>
{
Cons(s.head + 1, Inc(s.tail))
}
lemma {:induction false} UpLemma(k: nat, n: int)
ensures Inc(Up(n)) ==#[k] Up(n+1);
{
if (k != 0) {
UpLemma(k-1, n+1);
}
}
colemma {:induction false} CoUpLemma(n: int)
ensures Inc(Up(n)) == Up(n+1);
{
CoUpLemma(n+1);
}
lemma UpLemma_Auto(k: nat, n: int, nn: int)
ensures nn == n+1 ==> Inc(Up(n)) ==#[k] Up(nn); // note: it would be nice to do an automatic rewrite (from "ensures Inc(Up(n)) ==#[k] Up(n+1)") to obtain the good trigger here
{
}
colemma CoUpLemma_Auto(n: int, nn: int)
ensures nn == n+1 ==> Inc(Up(n)) == Up(nn); // see comment above
{
}
// -----------------------------------------------------------------------
function Repeat(n: int): Stream<int>
{
Cons(n, Repeat(n))
}
colemma RepeatLemma(n: int)
ensures Inc(Repeat(n)) == Repeat(n+1);
{
}
// -----------------------------------------------------------------------
copredicate True(s: Stream)
{
True(s.tail)
}
colemma AlwaysTrue(s: Stream)
ensures True(s);
{
}
copredicate AlsoTrue(s: Stream)
{
AlsoTrue(s)
}
colemma AlsoAlwaysTrue(s: Stream)
ensures AlsoTrue(s);
{
}
copredicate TT(y: int)
{
TT(y+1)
}
colemma AlwaysTT(y: int)
ensures TT(y);
{
}
// -----------------------------------------------------------------------
function Append(M: IList, N: IList): IList
{
match M
case Nil => N
case ICons(x, M') => ICons(x, Append(M', N))
}
function zeros(): IList<int>
{
ICons(0, zeros())
}
function ones(): IList<int>
{
ICons(1, ones())
}
copredicate AtMost(a: IList<int>, b: IList<int>)
{
match a
case Nil => true
case ICons(h,t) => b.ICons? && h <= b.head && AtMost(t, b.tail)
}
colemma ZerosAndOnes_Theorem0()
ensures AtMost(zeros(), ones());
{
}
colemma ZerosAndOnes_Theorem1()
ensures Append(zeros(), ones()) == zeros();
{
}
|
