f_puzzle.why 1.22 KB
Newer Older
1 2

(* Let f be a function over natural numbers such that, for all n
3 4 5 6 7 8 9 10 11
     f(f(n)) < f(n+1)
   Show that f(n)=n for all n.

   Inspired by a Dafny example (see http://searchco.de/codesearch/view/28108482)
   Original reference is

    Edsger W. Dijkstra: Heuristics for a Calculational Proof.
    Inf. Process. Lett. (IPL) 53(3):141-143 (1995)
*)
12 13 14

theory Puzzle

MARCHE Claude's avatar
MARCHE Claude committed
15
  use export int.Int
16 17 18 19 20 21

  function f int: int

  axiom H1: forall n: int. 0 <= n -> 0 <= f n
  axiom H2: forall n: int. 0 <= n -> f (f n) < f (n+1)

MARCHE Claude's avatar
MARCHE Claude committed
22 23 24 25
end

theory Step1 (* k <= f(n+k) by induction over k *)

26
  use Puzzle
MARCHE Claude's avatar
MARCHE Claude committed
27

Andrei Paskevich's avatar
Andrei Paskevich committed
28
  predicate p (k: int) = forall n: int. 0 <= n -> k <= f (n+k)
29 30 31
  clone int.SimpleInduction as I1
    with predicate p = p, lemma base, lemma induction_step

MARCHE Claude's avatar
MARCHE Claude committed
32 33 34 35
end

theory Solution

36 37
  use Puzzle
  use Step1
MARCHE Claude's avatar
MARCHE Claude committed
38

Andrei Paskevich's avatar
Andrei Paskevich committed
39
  lemma L3: forall n: int. 0 <= n -> n <= f n && f n <= f (f n)
40 41
  lemma L4: forall n: int. 0 <= n -> f n < f (n+1)

Andrei Paskevich's avatar
Andrei Paskevich committed
42
  (* so f is increasing *)
43 44 45 46
  predicate p' (k: int) = forall n m: int. 0 <= n <= m <= k -> f n <= f m
  clone int.SimpleInduction as I2
    with predicate p = p', lemma base, lemma induction_step

Andrei Paskevich's avatar
Andrei Paskevich committed
47 48
  lemma L5: forall n m: int. 0 <= n <= m -> f n <= f m
  lemma L6: forall n: int. 0 <= n -> f n < n+1
49 50 51 52

  goal G: forall n: int. 0 <= n -> f n = n

end