summaryrefslogtreecommitdiff
path: root/Test/dafny3/Dijkstra.dfy
blob: 56719180d3f10906351ab6fedc5041ae593b3cbc (plain)
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 direction: 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);
  }
}