induction example

parent 4ed1e418
(** 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
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v5//EN"
"http://why3.lri.fr/why3session.dtd">
<why3session shape_version="4">
<prover id="0" name="Z3" version="4.3.1" timelimit="6" memlimit="1000"/>
<prover id="1" name="Alt-Ergo" version="0.95.2" timelimit="6" memlimit="1000"/>
<file name="../induction.mlw" expanded="true">
<theory name="Hyps" sum="d41d8cd98f00b204e9800998ecf8427e" expanded="true">
</theory>
<theory name="Induction1" sum="9221b97d5cf79194e00ff2b0ad12ab27" expanded="true">
<goal name="SimpleInduction.base" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="3"/></proof>
</goal>
<goal name="SimpleInduction.induction_step" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="12"/></proof>
</goal>
<goal name="G" expanded="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
</theory>
<theory name="Induction2" sum="758b34abfd620b640c0847bc03ffba3d" expanded="true">
<goal name="G" expanded="true">
<proof prover="0"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="LemmaFunction1" sum="0b97221ee56665c396f229c342892274" expanded="true">
<goal name="WP_parameter ind" expl="VC for ind" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="11"/></proof>
</goal>
<goal name="G" expanded="true">
<proof prover="1"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
</theory>
<theory name="LemmaFunction2" sum="bac118e1088f3adc890ccd3ff1bf0913" expanded="true">
<goal name="WP_parameter ind" expl="VC for ind" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="16"/></proof>
</goal>
<goal name="G" expanded="true">
<proof prover="1"><result status="valid" time="0.01" steps="4"/></proof>
</goal>
</theory>
<theory name="LemmaFunction3" sum="5452936ba24ac5f71b4ccf89f38e7496" expanded="true">
<goal name="WP_parameter ind" expl="VC for ind" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="38"/></proof>
</goal>
<goal name="G" expanded="true">
<proof prover="1"><result status="valid" time="0.02" steps="4"/></proof>
</goal>
</theory>
</file>
</why3session>
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment