Commit fee930ef authored by MARCHE Claude's avatar MARCHE Claude

fix mistakes in Coq driver related to division and modulo

parent 3a1212a5
......@@ -96,6 +96,10 @@ theory int.MinMax
end
(* removed: Coq Zdiv is NOT true Euclidean division:
Zmod can be negative, in fact (Zmod x y) has the same sign as y,
which is not the usual convention of programming language either.
theory int.EuclideanDivision
prelude "Require Import Zdiv."
......@@ -110,9 +114,14 @@ theory int.EuclideanDivision
remove prop Div_1
end
*)
theory int.ComputerDivision
(* Coq Z0div provides the division and modulo operators
with the same convention as mainstream programming language
such C, Java, OCaml *)
prelude "Require Import ZOdiv."
syntax function div "(ZOdiv %1 %2)"
......
......@@ -10,7 +10,11 @@ Find the sum of all the multiples of 3 or 5 below 1000.
theory DivModHints
use import int.Int
use import int.EuclideanDivision
use import int.ComputerDivision
lemma mod_div_unique :
forall x y q r:int. y > 0 /\ x = q*y + r /\ 0 <= r < y ->
r = mod x y /\ q = div x y
lemma mod_succ_1 :
forall x y:int. x >= 0 /\ y > 0 ->
......@@ -34,7 +38,7 @@ end
theory SumMultiple
use import int.Int
use import int.EuclideanDivision
use import int.ComputerDivision
(* [sum_multiple_3_5_lt n] is the sum of all the multiples
of 3 or 5 below n] *)
......@@ -64,6 +68,10 @@ theory SumMultiple
use DivModHints
lemma mod_15:
forall n:int.
mod n 15 = 0 <-> mod n 3 = 0 /\ mod n 5 = 0
lemma Closed_formula_n:
forall n:int. n > 0 -> p (n-1) ->
mod n 3 <> 0 /\ mod n 5 <> 0 -> p n
......@@ -91,7 +99,7 @@ module Euler001
use import SumMultiple
use import int.Int
use import int.EuclideanDivision
use import int.ComputerDivision
let solve n =
{ n >= 1 }
......
<?xml version="1.0" encoding="UTF-8"?>
<!DOCTYPE why3session SYSTEM "why3session.dtd">
<why3session name="programs/euler001/why3session.xml">
<prover id="alt-ergo" name="Alt-Ergo" version="0.93"/>
<prover id="coq" name="Coq" version="8.2pl1"/>
<prover id="cvc3" name="CVC3" version="2.2"/>
<prover id="gappa" name="Gappa" version="0.13.0"/>
<prover id="simplify" name="Simplify" version="1.5.4"/>
<prover id="z3" name="Z3" version="2.19"/>
<file name="../euler001.mlw" verified="false" expanded="true">
<theory name="SumMultiple" verified="false" expanded="true">
<goal name="div_minus1_1" sum="13bdc85ec0d359b20dfddb8e00e945f7" proved="true" expanded="true" shape="ainfix =adivainfix +V0c1V1ainfix +adivV0V1c1Iainfix =amodainfix +V0c1V1c0Iainfix >V1c0Aainfix >=V0c0F">
<proof prover="coq" timelimit="5" edited="euler001_SumMultiple_div_minus1_1_1.v" obsolete="false">
<result status="valid" time="0.72"/>
<why3session
name="examples/programs/euler001/why3session.xml">
<prover
id="alt-ergo"
name="Alt-Ergo"
version="0.93"/>
<prover
id="coq"
name="Coq"
version="8.2pl1"/>
<prover
id="cvc3"
name="CVC3"
version="2.2"/>
<prover
id="eprover"
name="Eprover"
version="1.4 Namring"/>
<prover
id="gappa"
name="Gappa"
version="0.15.1"/>
<prover
id="simplify"
name="Simplify"
version="1.5.4"/>
<prover
id="spass"
name="Spass"
version="3.7"/>
<prover
id="vampire"
name="Vampire"
version="0.6"/>
<prover
id="verit"
name="veriT"
version="dev"/>
<prover
id="yices"
name="Yices"
version="1.0.25"/>
<prover
id="z3"
name="Z3"
version="2.19"/>
<file
name="../euler001.mlw"
verified="false"
expanded="true">
<theory
name="DivModHints"
verified="false"
expanded="true">
<goal
name="mod_div_unique"
sum="dad7f26312903f3c0ce7ea31f08a8a94"
proved="false"
expanded="true"
shape="ainfix =V2adivV0V1Aainfix =V3amodV0V1Iainfix <V3V1Aainfix <=c0V3Aainfix =V0ainfix +ainfix *V2V1V3Aainfix >V1c0F">
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.05"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.13"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.37"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
</goal>
<goal name="div_minus1_2" sum="98f2f9456ee9de20238d9421ce48bd13" proved="false" expanded="true" shape="ainfix =adivainfix +V0c1V1adivV0V1Iainfix =amodainfix +V0c1V1c0NIainfix >V1c0Aainfix >=V0c0F">
<proof prover="simplify" timelimit="5" edited="" obsolete="false">
<result status="unknown" time="0.06"/>
<goal
name="mod_succ_1"
sum="0a9a4fed2057820683962116afbcf691"
proved="false"
expanded="true"
shape="ainfix =amodainfix +V0c1V1ainfix +amodV0V1c1Iainfix =amodainfix +V0c1V1c0NIainfix >V1c0Aainfix >=V0c0F">
<proof
prover="coq"
timelimit="5"
edited="euler001_DivModHints_mod_succ_1_1.v"
obsolete="false">
<result status="unknown" time="1.54"/>
</proof>
<proof
prover="simplify"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.07"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="timeout" time="5.02"/>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<result status="unknown" time="0.35"/>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="gappa"
timelimit="5"
edited=""
obsolete="false">
<result status="unknown" time="0.02"/>
</proof>
<proof
prover="vampire"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.01"/>
</proof>
<proof
prover="spass"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.06"/>
</proof>
</goal>
<goal name="Closed_formula_0" sum="0efd59f4730df5b0fb1c583cf34ac0f5" proved="true" expanded="true" shape="apc0">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.21"/>
<goal
name="mod_succ_2"
sum="d10d5aa2a6f8a1ece4e07b571cd6ab5a"
proved="false"
expanded="true"
shape="ainfix =amodV0V1ainfix -V1c1Iainfix =amodainfix +V0c1V1c0Iainfix >V1c0Aainfix >=V0c0F">
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
<proof prover="alt-ergo" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.09"/>
</proof>
<proof prover="z3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.10"/>
</proof>
</goal>
<goal name="Closed_formula_n" sum="d861eeda33c9e160cd35f3381f03748a" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.38"/>
<goal
name="div_succ_1"
sum="773313eff1da137611f6b6782b46b107"
proved="true"
expanded="false"
shape="ainfix =adivainfix +V0c1V1ainfix +adivV0V1c1Iainfix =amodainfix +V0c1V1c0Iainfix >V1c0Aainfix >=V0c0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.10"/>
</proof>
</goal>
<goal name="Closed_formula_n_3" sum="1ae550c85222b80bcc3d01ae6bed6d36" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.04"/>
<goal
name="div_succ_2"
sum="500683558e28d63d764f874cc487b206"
proved="true"
expanded="false"
shape="ainfix =adivainfix +V0c1V1adivV0V1Iainfix =amodainfix +V0c1V1c0NIainfix >V1c0Aainfix >=V0c0F">
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="1.28"/>
</proof>
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.09"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.75"/>
</proof>
</goal>
<goal name="Closed_formula_n_5" sum="ccf1855da190fb697da5c2885d47048a" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
</theory>
<theory
name="SumMultiple"
verified="false"
expanded="true">
<goal
name="Closed_formula_0"
sum="d92d1f799a0a4fc4c1fdc50a2fbc0154"
proved="true"
expanded="false"
shape="apc0">
<proof
prover="cvc3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.07"/>
</proof>
<proof
prover="alt-ergo"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.99"/>
</proof>
<proof
prover="z3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.07"/>
</proof>
</goal>
<goal name="Closed_formula_n_15" sum="4a7fb49695cc456d61575fa99a11fa87" proved="true" expanded="true" shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
<proof prover="alt-ergo" timelimit="5" edited="" obsolete="false">
<result status="valid" time="0.03"/>
<goal
name="mod_15"
sum="071e467d1502abbcf3367fb8f2269e3c"
proved="true"
expanded="false"
shape="ainfix =amodV0c5c0Aainfix =amodV0c3c0qainfix =amodV0c15c0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.37"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="3.05"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.10"/>
</proof>
</goal>
<goal name="Closed_formula" sum="8c080d79afa6158714c9ba082a4c98a9" proved="true" expanded="true" shape="apV0Iainfix <=c0V0F">
<proof prover="cvc3" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.11"/>
<goal
name="Closed_formula_n"
sum="a5c87710b2664ff581de5ef657e5afe1"
proved="true"
expanded="false"
shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="3.24"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.13"/>
</goal>
<goal
name="Closed_formula_n_3"
sum="6d49427a8f97ca827908d662744a9687"
proved="false"
expanded="true"
shape="apV0Iainfix =amodV0c5c0NAainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.10"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.07"/>
</proof>
</goal>
</theory>
<theory name="WP Euler001" verified="true" expanded="true">
<goal name="WP_parameter solve" expl="normal postcondition" sum="60edaf51943c778798200b51f190aed1" proved="true" expanded="true" shape="ainfix =adivainfix -ainfix +ainfix *ainfix *c3adivainfix -V0c1c3ainfix +adivainfix -V0c1c3c1ainfix *ainfix *c5adivainfix -V0c1c5ainfix +adivainfix -V0c1c5c1ainfix *ainfix *c15adivainfix -V0c1c15ainfix +adivainfix -V0c1c15c1c2asum_multiple_3_5_ltV0Iainfix >=V0c1F">
<proof prover="cvc3" timelimit="5" edited="" obsolete="false">
<result status="valid" time="3.60"/>
<goal
name="Closed_formula_n_5"
sum="dc51b25fcf9abe8309b6d18bb6e9846e"
proved="false"
expanded="true"
shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0NIapainfix -V0c1Iainfix >V0c0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.09"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.09"/>
</proof>
</goal>
<goal
name="Closed_formula_n_15"
sum="c88e46eef0ee5c74ac4cbe91b7f606d1"
proved="false"
expanded="true"
shape="apV0Iainfix =amodV0c5c0Aainfix =amodV0c3c0Iapainfix -V0c1Iainfix >V0c0F">
<proof
prover="cvc3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.08"/>
</proof>
<proof
prover="alt-ergo"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.07"/>
</proof>
<proof prover="simplify" timelimit="2" edited="" obsolete="false">
<result status="valid" time="0.20"/>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="timeout" time="5.07"/>
</proof>
</goal>
<goal
name="Closed_formula"
sum="d91a34e848796aac5aed95527121e949"
proved="true"
expanded="false"
shape="apV0Iainfix <=c0V0F">
<proof
prover="cvc3"
timelimit="2"
edited=""
obsolete="false">
<result status="valid" time="0.29"/>
</proof>
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.38"/>
</proof>
</goal>
</theory>
<theory
name="WP Euler001"
verified="true"
expanded="false">
<goal
name="WP_parameter solve"
expl="normal postcondition"
sum="9d0d476bc8b0e5302b671752c80d437b"
proved="true"
expanded="false"
shape="ainfix =adivainfix -ainfix +ainfix *ainfix *c3adivainfix -V0c1c3ainfix +adivainfix -V0c1c3c1ainfix *ainfix *c5adivainfix -V0c1c5ainfix +adivainfix -V0c1c5c1ainfix *ainfix *c15adivainfix -V0c1c15ainfix +adivainfix -V0c1c15c1c2asum_multiple_3_5_ltV0Iainfix >=V0c1F">
<proof
prover="z3"
timelimit="5"
edited=""
obsolete="false">
<result status="valid" time="0.11"/>
</proof>
</goal>
</theory>
......
......@@ -49,6 +49,9 @@ end
theory EuclideanDivision
(* division and modulo operators with the convention that division
rounds down, and thus modulo is always non-negative *)
use import Int
use import Abs
......@@ -72,6 +75,11 @@ end
theory ComputerDivision
(* division and modulo operators with the same conventions as
mainstream programming language such C, Java, OCaml, that is
division rounds towards zero, and thus (x mod y) as the same sign
as x *)
use import Int
use import Abs
......
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