diff --git a/examples/induction.mlw b/examples/induction.mlw new file mode 100644 index 0000000000000000000000000000000000000000..a19db063fbe08d9f3943fd8b44c6736e21c1b06b --- /dev/null +++ b/examples/induction.mlw @@ -0,0 +1,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 diff --git a/examples/induction/why3session.xml b/examples/induction/why3session.xml new file mode 100644 index 0000000000000000000000000000000000000000..dd1e6d93b74ba29e80c3908a9c4b99138d64ad67 --- /dev/null +++ b/examples/induction/why3session.xml @@ -0,0 +1,51 @@ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + diff --git a/examples/induction/why3shapes.gz b/examples/induction/why3shapes.gz new file mode 100644 index 0000000000000000000000000000000000000000..a2f7daafecdfabedbd97550a3f0f791187749a9c Binary files /dev/null and b/examples/induction/why3shapes.gz differ