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

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

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)

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

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