Elementary properties of integer division

Sep 11, 2014 at 2:20 PM
Edited Sep 11, 2014 at 3:38 PM
I would be gratefull if someone could help me to find some .dfy file proving the most elementary properties of integer division (and product), like e.g. the following two lemmas:
lemma L1 (x:int,y:int)
    requires x > 0 ;
    ensures (y/x) * x == y;

lemma L2 (x:int,y:int,m:int)
    requires x > 0 ;
    ensures m == y/x  <==>  m*x == y;
In addition, how can one prove a lemma that ensures that forall x,y :: x>0 ==> (x*y) % x == 0;?
I'm involved in many basic properties of integer division that Dafny can not prove automatically,
or I don't know what should be proved first, all them are related.
Sep 12, 2014 at 10:12 AM
Adding some modulo operations, Dafny immediately verifies most of the statements intended by lemmata L1 and L2:
ghost method Lemma3 (x:int,y:int)
    requires x != 0;
    ensures (y/x) * x + y%x == y;
{}

ghost method Lemma4 (x:int,y:int,m:int)
    requires x != 0;
    ensures m == y/x && y%x == 0  ==>  m*x == y;
    ensures m*x == y  ==>  (m == y/x  <==>  y%x == 0);
    //ensures m*x == y  ==>  m == y/x && y%x == 0;
{}
However, Dafny fails to verify the (I believe) correct and much stronger postcondition I have commented out. (I am probably using an older version of Dafny (1.6.3.00320) and Z3.)

Dafny's definition of integer division apparently is the Euclidean one (in contrast to the floored and truncated versions), where the remainder is always greater or equal to 0, independently of the signs of numerator and denominator, as evidenced by the following lemma, which Dafny proves immediately:
ghost method Lemma5 (x:int,y:int)
  requires x != 0;
  ensures y == x * (y/x) + y%x;
  ensures 0 < x ==> 0 <= y%x <  x;
  ensures x < 0 ==> 0 <= y%x < -x;
{}
But I believe the concrete results above hold in any of these versions.

Edgar
Sep 12, 2014 at 2:08 PM
Hi Edgar,
Many thanks for the lemmas that Dafny proves automatically.
Your commented postcondition
    //ensures m*x == y  ==>  m == y/x && y%x == 0;
is netither proved in my MVS version, nor in the Dafny online.
But using one of your lemmas, I achieve a proof of the ifff that
you can find in
http://rise4fun.com/Dafny/HZUT
(sorry, var names are permuted w.r.t. your commented post).

My problem now is that this file is perfectly verified online (check, please),
but not in my version on MVS.

Paqui
Sep 12, 2014 at 2:16 PM
Sorry, I just realize that not only var names are changed, but it is a similar and dual property to yours:
    //ensures m*x == y  ==>  m == y/x && y%x == 0;
Anyway, does your MVS-Dafny verify the file in http://rise4fun.com/Dafny/HZUT ?
Sep 12, 2014 at 4:29 PM
Edited Sep 13, 2014 at 11:23 AM
Hi again,
A surprising (at least, for me) automatic Dafny-proof involving integer division is "The square root of 2 is irrational".
What is even more surprising for me is that Dafny is able to prove one formulation, but not the other equivalent.
Please see
http://rise4fun.com/Dafny/cNAsl

Have you any explanation?
Paqui