f_puzzle.why 1.24 KB
 Jean-Christophe Filliatre committed Mar 02, 2013 1 2 `````` (* Let f be a function over natural numbers such that, for all n `````` Jean-Christophe Filliatre committed May 18, 2013 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) *) `````` Jean-Christophe Filliatre committed Mar 02, 2013 12 13 14 `````` theory Puzzle `````` MARCHE Claude committed Mar 08, 2013 15 `````` use export int.Int `````` Jean-Christophe Filliatre committed Mar 02, 2013 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 committed Mar 08, 2013 22 23 24 25 26 27 ``````end theory Step1 (* k <= f(n+k) by induction over k *) use import Puzzle `````` Andrei Paskevich committed Mar 07, 2013 28 `````` predicate p (k: int) = forall n: int. 0 <= n -> k <= f (n+k) `````` Jean-Christophe Filliatre committed Mar 02, 2013 29 30 31 `````` clone int.SimpleInduction as I1 with predicate p = p, lemma base, lemma induction_step `````` MARCHE Claude committed Mar 08, 2013 32 33 34 35 36 37 38 ``````end theory Solution use import Puzzle use import Step1 `````` Andrei Paskevich committed Mar 07, 2013 39 `````` lemma L3: forall n: int. 0 <= n -> n <= f n && f n <= f (f n) `````` Jean-Christophe Filliatre committed Mar 02, 2013 40 41 `````` lemma L4: forall n: int. 0 <= n -> f n < f (n+1) `````` Andrei Paskevich committed Mar 07, 2013 42 `````` (* so f is increasing *) `````` Jean-Christophe Filliatre committed Mar 02, 2013 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 committed Mar 07, 2013 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 `````` Jean-Christophe Filliatre committed Mar 02, 2013 49 50 51 52 `````` goal G: forall n: int. 0 <= n -> f n = n end``````