examples/f_puzzle.mlw

   1
   2 (* Let f be a function over natural numbers such that, for all n
   3      f(f(n)) < f(n+1)
   4    Show that f(n)=n for all n.
   5
   6    Inspired by a Dafny example (see http://searchco.de/codesearch/view/28108482)
   7    Original reference is
   8
   9     Edsger W. Dijkstra: Heuristics for a Calculational Proof.
  10     Inf. Process. Lett. (IPL) 53(3):141-143 (1995)
  11 *)
  12
  13 theory Puzzle
  14
  15   use export int.Int
  16
  17   function f int: int
  18
  19   axiom H1: forall n: int. 0 <= n -> 0 <= f n
  20   axiom H2: forall n: int. 0 <= n -> f (f n) < f (n+1)
  21
  22 end
  23
  24 theory Step1 (* k <= f(n+k) by induction over k *)
  25
  26   use Puzzle
  27
  28   predicate p (k: int) = forall n: int. 0 <= n -> k <= f (n+k)
  29   clone int.SimpleInduction as I1
  30     with predicate p = p, lemma base, lemma induction_step
  31
  32 end
  33
  34 theory Solution
  35
  36   use Puzzle
  37   use Step1
  38
  39   lemma L3: forall n: int. 0 <= n -> n <= f n && f n <= f (f n)
  40   lemma L4: forall n: int. 0 <= n -> f n < f (n+1)
  41
  42   (* so f is increasing *)
  43   predicate p' (k: int) = forall n m: int. 0 <= n <= m <= k -> f n <= f m
  44   clone int.SimpleInduction as I2
  45     with predicate p = p', lemma base, lemma induction_step
  46
  47   lemma L5: forall n m: int. 0 <= n <= m -> f n <= f m
  48   lemma L6: forall n: int. 0 <= n -> f n < n+1
  49
  50   goal G: forall n: int. 0 <= n -> f n = n
  51
  52 end