Commit 5073ebc8 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Attempt to prove euler002

parent 6d71591f
......@@ -11,21 +11,26 @@ exceed four million, find the sum of the even-valued terms. *)
theory Fib "Definition of Fibonacci sequence"
use export int.Int
use import int.Int
function fib int : int
axiom fib0: fib 0 = 1
axiom fib1: fib 1 = 2
axiom fibn: forall n:int [fib n].
n >= 2 -> fib n = fib (n-1) + fib (n-2)
goal smoke : false
end
theory FibSumEven "sum of even-valued Fibonacci numbers"
use import int.Int
use import Fib
use import int.EuclideanDivision
use import int.ComputerDivision
(* [fib_sum_even_lt m] is the sum of even-valued terms
of the Fibonacci sequence that are less than m
......@@ -53,20 +58,19 @@ theory FibSumEven "sum of even-valued Fibonacci numbers"
function fib_sum_even_lt (m:int) : int = fib_sum_even_lt_from m 0
goal smoke : false
end
theory FibOnlyEven
use export Fib
use import int.EuclideanDivision
goal smoke0 : false
use import int.Int
use import int.ComputerDivision
use import Fib
lemma fib_even : forall n:int. n >= 0 ->
(mod (fib n) 2 = 0 <-> mod n 3 = 1)
goal smoke1 : false
(* we pose xn = f(3n+1), that is
x_0 = 2, x_1 = 8, x_{n+2} = 4 x_{n+1} + x_n
*)
......@@ -81,15 +85,15 @@ theory FibOnlyEven
lemma fib_even_correct :
forall n:int. fib_even n = fib (3*n+1)
goal smoke2 : false
use export FibSumEven
goal smoke : false
end
module Solve
use import int.Int
use import ref.Ref
use import FibSumEven
use import FibOnlyEven
let f m : int
......@@ -99,6 +103,7 @@ module Solve
let y = ref 8 in
let sum = ref 0 in
while !x < m do
invariant { !sum = fib_sum_even_lt !x }
let tmp = !x in
x := !y;
y := 4 * !y + tmp;
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session PUBLIC "-//Why3//proof session v2//EN" "http://why3.lri.fr/why3session.dtd">
<why3session shape_version="2">
<prover
id="0"
name="Alt-Ergo"
version="0.94"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95"/>
<prover
id="2"
name="CVC3"
version="2.2"/>
<prover
id="3"
name="CVC3"
version="2.4.1"/>
<prover
id="4"
name="CVC4"
version="1.0"/>
<prover
id="5"
name="Z3"
version="2.19"/>
<prover
id="6"
name="Z3"
version="3.2"/>
<prover
id="7"
name="Z3"
version="4.2"/>
<file
name="../euler002.mlw"
verified="false"
expanded="true">
<theory
name="Fib"
locfile="../euler002.mlw"
loclnum="12" loccnumb="7" loccnume="10"
verified="false"
expanded="true">
<label
name="Definition of Fibonacci sequence"/>
<goal
name="smoke"
locfile="../euler002.mlw"
loclnum="25" loccnumb="7" loccnume="12"
sum="d24698e36750dd69ab5214ee7fd9d3a4"
proved="false"
expanded="true"
shape="f">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.26"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.00"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.17"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
</proof>
</goal>
</theory>
<theory
name="FibSumEven"
locfile="../euler002.mlw"
loclnum="29" loccnumb="7" loccnume="17"
verified="false"
expanded="true">
<label
name="sum of even-valued Fibonacci numbers"/>
<goal
name="smoke"
locfile="../euler002.mlw"
loclnum="61" loccnumb="7" loccnume="12"
sum="4c2ab4907bff825f7aeae35a3445585c"
proved="false"
expanded="true"
shape="f">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.27"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.04"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.05"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.15"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
</proof>
</goal>
</theory>
<theory
name="FibOnlyEven"
locfile="../euler002.mlw"
loclnum="65" loccnumb="7" loccnume="18"
verified="false"
expanded="true">
<goal
name="fib_even"
locfile="../euler002.mlw"
loclnum="71" loccnumb="8" loccnume="16"
sum="d486dc78b6862c9ad860b8f66867d892"
proved="false"
expanded="true"
shape="ainfix =amodV0c3c1qainfix =amodafibV0c2c0Iainfix &gt;=V0c0F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.00"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.65"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="2.20"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.11"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.21"/>
</proof>
</goal>
<goal
name="fib_even_correct"
locfile="../euler002.mlw"
loclnum="85" loccnumb="8" loccnume="24"
sum="95a3ceefca0ff2c3fba77386e957227d"
proved="false"
expanded="true"
shape="ainfix =afib_evenV0afibainfix +ainfix *c3V0c1F">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="1.86"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.05"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.16"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.12"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.10"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.10"/>
</proof>
</goal>
<goal
name="smoke"
locfile="../euler002.mlw"
loclnum="88" loccnumb="7" loccnume="12"
sum="3e18086c1fc95d379468f2ccc72cd74c"
proved="false"
expanded="true"
shape="f">
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="4.99"/>
</proof>
<proof
prover="2"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.14"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="unknown" time="0.09"/>
</proof>
<proof
prover="5"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.11"/>
</proof>
</goal>
</theory>
<theory
name="Solve"
locfile="../euler002.mlw"
loclnum="92" loccnumb="7" loccnume="12"
verified="false"
expanded="true">
<goal
name="WP_parameter f"
locfile="../euler002.mlw"
loclnum="99" loccnumb="6" loccnume="7"
expl="VC for f"
sum="05284a9e3094335743434a24c35e9e50"
proved="false"
expanded="true"
shape="iainfix &lt;V3V0ainfix =V6afib_sum_even_ltV4Iainfix =V6ainfix +V1V3FIainfix =V5ainfix +ainfix *c4V2V3FIainfix =V4V2Fainfix =V1afib_sum_even_ltV0Iainfix =V1afib_sum_even_ltV3FAainfix =c0afib_sum_even_ltc2Iainfix &gt;=V0c0F">
<label
name="expl:VC for f"/>
<transf
name="split_goal_wp"
proved="false"
expanded="true">
<goal
name="WP_parameter f.1"
locfile="../euler002.mlw"
loclnum="99" loccnumb="6" loccnume="7"
expl="1. loop invariant init"
sum="0b96243886f60fcb271e6d947b08dfca"
proved="true"
expanded="false"
shape="ainfix =c0afib_sum_even_ltc2Iainfix &gt;=V0c0F">
<label
name="expl:VC for f"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.01"/>
</proof>
<proof
prover="6"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
</proof>
<proof
prover="7"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.04"/>
</proof>
</goal>
<goal
name="WP_parameter f.2"
locfile="../euler002.mlw"
loclnum="99" loccnumb="6" loccnume="7"
expl="2. loop invariant preservation"
sum="e0896c831fae96710d54659263487778"
proved="false"
expanded="true"
shape="ainfix =V6afib_sum_even_ltV4Iainfix =V6ainfix +V1V3FIainfix =V5ainfix +ainfix *c4V2V3FIainfix =V4V2FIainfix &lt;V3V0Iainfix =V1afib_sum_even_ltV3FIainfix &gt;=V0c0F">
<label
name="expl:VC for f"/>
<proof
prover="0"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.13"/>
</proof>
<proof
prover="1"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="3"
timelimit="5"
memlimit="1000"
obsolete="false"
archived="false">
<result status="timeout" time="5.23"/>
</proof>
<proof
prover="4"
timelimit="5"
memlimit="1000"