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
|
// RUN: %dafny /compile:0 /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Example taken from:
// Edsger W. Dijkstra: Heuristics for a Calculational Proof. Inf. Process. Lett. (IPL) 53(3):141-143 (1995)
// Transcribed into Dafny by Valentin Wüstholz and Nadia Polikarpova.
// f is an arbitrary function on the natural numbers
function f(n: nat) : nat
// Predicate P() says that f satisfies a peculiar property
predicate P()
{
forall m: nat :: f(f(m)) < f(m + 1)
}
// The following theorem says that if f satisfies the peculiar property,
// then f is the identity function. The body of the method, and the methods
// that follow, give the proof.
lemma theorem()
requires P()
ensures forall n: nat :: f(n) == n
{
forall n: nat
ensures f(n) == n
{
calc {
f(n);
== { lemma_ping(n, n); lemma_pong(n); }
n;
}
}
}
// Aiming at n <= f(n), but strengthening it for induction
lemma lemma_ping(j: nat, n: nat)
requires P()
ensures j <= n ==> j <= f(n)
{
// The case for j == 0 is trivial
if 0 < j
{
calc {
j <= f(n);
==
j - 1 < f(n);
<== // P with m := n - 1
j - 1 <= f(f(n - 1)) && 1 <= n;
<== { lemma_ping(j - 1, f(n - 1)); }
j - 1 <= f(n - 1) && 1 <= n;
<== { lemma_ping(j - 1, n - 1); }
j - 1 <= n - 1 && 1 <= n;
== // 0 < j
j <= n;
}
}
}
// The other directorion: f(n) <= n
lemma lemma_pong(n: nat)
requires P()
ensures f(n) <= n
{
calc {
f(n) <= n;
==
f(n) < n + 1;
<== { lemma_monotonicity_0(n + 1, f(n)); }
f(f(n)) < f(n + 1);
== // P with m := n
true;
}
}
lemma lemma_monotonicity_0(a: nat, b: nat)
requires P()
ensures a <= b ==> f(a) <= f(b) // or, equivalently: f(b) < f(a) ==> b < a
decreases b - a
{
// The case for a == b is trivial
if a < b {
calc {
f(a);
<= { lemma_monotonicity_1(a); }
f(a + 1);
<= { lemma_monotonicity_0(a + 1, b); }
f(b);
}
}
}
lemma lemma_monotonicity_1(n: nat)
requires P()
ensures f(n) <= f(n + 1)
{
calc {
f(n);
<= { lemma_ping(f(n), f(n)); }
f(f(n));
<= // (0)
f(n + 1);
}
}
|
