f_puzzle.why 1.24 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 26 27
end

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

  use import Puzzle

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 36 37 38
end

theory Solution

  use import Puzzle
  use import Step1

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