induction.mlw 1.84 KB
Newer Older
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