Wiki Agenda Contact Version française

Various ways of proving an induction principle

Various ways of proving an induction principle using theories int.SimpleInduction or int.Induction or lemma functions


Authors: Jean-Christophe Filliâtre

Topics: Mathematics / Ghost code

Tools: Why3

see also the index (by topic, by tool, by reference, by year)


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

With a simple induction

module Induction1
  use Hyps

  predicate pr (k: int) = p k && p (k+1)
  clone int.SimpleInduction
    with predicate p = pr, lemma base, lemma induction_step

  goal G: forall n: int. 0 <= n -> p n

end

With a strong induction

module Induction2
  use Hyps

  clone int.Induction
    with predicate p = p, constant bound = zero

  goal G: forall n: int. 0 <= n -> p n

end

With a recursive lemma function

module LemmaFunction1
  use Hyps

  let rec lemma ind (n: int) requires { 0 <= n} ensures { p n }
    variant { n }
    = if n >= 2 then ind (n-2)

  goal G: forall n: int. 0 <= n -> p n

no need to write the following goal, that's just a check this is now proved

end

With a while loop

module LemmaFunction2
  use Hyps
  use 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

With an ascending while loop

module LemmaFunction3
  use Hyps
  use 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

download ZIP archive

Why3 Proof Results for Project "induction"

Theory "induction.Induction1": fully verified

ObligationsAlt-Ergo 2.0.0CVC4 1.5
SimpleInduction.base0.00---
SimpleInduction.induction_step0.00---
G---0.00

Theory "induction.Induction2": fully verified

ObligationsZ3 4.6.0
G0.02

Theory "induction.LemmaFunction1": fully verified

ObligationsAlt-Ergo 2.0.0
VC ind0.00
G0.00

Theory "induction.LemmaFunction2": fully verified

ObligationsAlt-Ergo 2.0.0
VC ind0.00
G0.00

Theory "induction.LemmaFunction3": fully verified

ObligationsAlt-Ergo 2.0.0
VC ind0.01
G0.00