From 337cac2055c0e0ff7af7b6232464d999c9a41fa5 Mon Sep 17 00:00:00 2001 From: Jean-Christophe Filliatre Date: Sat, 21 Mar 2015 13:58:26 +0100 Subject: [PATCH] induction example --- examples/induction.mlw | 90 +++++++++++++++++++++++++++++ examples/induction/why3session.xml | 51 ++++++++++++++++ examples/induction/why3shapes.gz | Bin 0 -> 383 bytes 3 files changed, 141 insertions(+) create mode 100644 examples/induction.mlw create mode 100644 examples/induction/why3session.xml create mode 100644 examples/induction/why3shapes.gz diff --git a/examples/induction.mlw b/examples/induction.mlw new file mode 100644 index 000000000..a19db063f --- /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 000000000..dd1e6d93b --- /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 GIT binary patch literal 383 zcmV-_0f7D=iwFP!00000|E-cgkJ~T|#rOLZ*\$)Tsk3>p9Q{a{W0Xlo9NEygd1fBZv zE8n?^eF@N|n<@EG@BK)FnR7Qm*6dKw1Vlg z9-Xg=Xm@@ycbw=J0G&?v1h^!4j^ngP@Gzgbbg+`VG~_hAYA!ye1gM!u^rt}\$&1N=n zO&PT3)H!uYk()a4ocBTR&^P{J?{j~Cy)7g82bB\$wferqJ=XHx`NN_v%^QJw1w%=HJ dSegakP2lh\$@GpC{t^EHW{sRQ!lC;_b003t#x(omS literal 0 HcmV?d00001 -- 2.26.2