induction.mlw 1.84 KB
 Jean-Christophe Filliatre committed Mar 21, 2015 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 `````` (** Various ways of proving p 0 p 1 forall n: int. 0 <= n -> p n -> p (n+2) --------------------------------------- forall n: int. 0 <= n -> p n by induction using theories int.SimpleInduction or int.Induction or lemma functions. *) theory Hyps use export int.Int predicate p int axiom H0: p 0 axiom H1: p 1 axiom H2: forall n: int. 0 <= n -> p n -> p (n + 2) end module Induction1 "with a simple induction" use import Hyps predicate pr (k: int) = p k && p (k+1) clone import int.SimpleInduction with predicate p = pr, lemma base, lemma induction_step goal G: forall n: int. 0 <= n -> p n end module Induction2 "with a strong induction" use import Hyps clone import int.Induction with predicate p = p, constant bound = zero goal G: forall n: int. 0 <= n -> p n end module LemmaFunction1 "with a recursive lemma function" use import Hyps let rec lemma ind (n: int) requires { 0 <= n} ensures { p n } variant { n } = if n >= 2 then ind (n-2) (** no need to write the following goal, that's just a check this is now proved *) goal G: forall n: int. 0 <= n -> p n end module LemmaFunction2 "with a while loop" use import Hyps use import ref.Ref let lemma ind (n: int) requires { 0 <= n} ensures { p n } = let k = ref n in while !k >= 2 do invariant { 0 <= !k && (p !k -> p n) } variant { !k } k := !k - 2 done goal G: forall n: int. 0 <= n -> p n end module LemmaFunction3 "with an ascending while loop" use import Hyps use import ref.Ref let lemma ind (n: int) requires { 0 <= n} ensures { p n } = let k = ref 0 in while !k <= n - 2 do invariant { 0 <= !k <= n && p !k && p (!k + 1) } variant { n - !k } k := !k + 2 done goal G: forall n: int. 0 <= n -> p n end``````