## Various ways of proving an induction principle

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

Auteurs: Jean-Christophe Filliâtre

Catégories: Mathematics / Ghost code

Outils: 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
```

# Why3 Proof Results for Project "induction"

## Theory "induction.Induction1": fully verified

 Obligations CVC4 1.5 Z3 4.12.2 SimpleInduction.base --- 0.01 SimpleInduction.induction_step --- 0.01 G 0.00 ---

## Theory "induction.Induction2": fully verified

 Obligations Z3 4.12.2 G 0.02

## Theory "induction.LemmaFunction1": fully verified

 Obligations Z3 4.12.2 VC for ind 0.01 G 0.01

## Theory "induction.LemmaFunction2": fully verified

 Obligations Z3 4.12.2 VC for ind 0.01 G 0.01

## Theory "induction.LemmaFunction3": fully verified

 Obligations Z3 4.12.2 VC for ind 0.01 G 0.01