From fee930efed948f1062574132d20902978c75bf43 Mon Sep 17 00:00:00 2001 From: Claude Marche Date: Wed, 28 Sep 2011 08:56:58 +0200 Subject: [PATCH] fix mistakes in Coq driver related to division and modulo --- drivers/coq.drv | 9 + examples/programs/euler001.mlw | 14 +- examples/programs/euler001/why3session.xml | 446 ++++++++++++++++++--- theories/int.why | 8 + 4 files changed, 425 insertions(+), 52 deletions(-) diff --git a/drivers/coq.drv b/drivers/coq.drv index dff93b513..fe6123251 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 660f7e54f..79d1e29b9 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 052c20aa6..6589970fb 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 3a50bbabe..b5f60ed6e 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 -- GitLab