diff --git a/drivers/coq.drv b/drivers/coq.drv index dff93b513587d0b20ddf0208ee6d2ab28be22037..fe61232511ee0443c7cd28531ec6cd504918604a 100644 --- a/drivers/coq.drv +++ b/drivers/coq.drv @@ -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)" diff --git a/examples/programs/euler001.mlw b/examples/programs/euler001.mlw index 660f7e54f0fa7c3442d54757838351ddc6e98c9c..79d1e29b92f218bc9462ec88b9f8d5938ff6fdcd 100644 --- a/examples/programs/euler001.mlw +++ b/examples/programs/euler001.mlw @@ -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 } diff --git a/examples/programs/euler001/why3session.xml b/examples/programs/euler001/why3session.xml index 052c20aa66a320fcc1eaacbf32e1a30fd59b036e..6589970fb522077b20234ffcd619a02a79b6ccf7 100644 --- a/examples/programs/euler001/why3session.xml +++ b/examples/programs/euler001/why3session.xml @@ -1,77 +1,425 @@ - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + - - - + + + + + + + + + - - + + - - + + + + + + + + + + + - - - + + + - - + + - - + + - - - + + + - - - + + + + + + + + + - - + + + + + + + + + + - - - + + + + + + + + + - - - + + + - - + + + + + + + + + + - - - - - + + + + + + + + + + + + + + + + + - - + + + + + + + + + + + + + + + + + diff --git a/theories/int.why b/theories/int.why index 3a50bbabe5d8ff834ba099f397cf506512e492df..b5f60ed6e01a6b434d8f6b9e3fcc9eaef44eb590 100644 --- a/theories/int.why +++ b/theories/int.why @@ -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