The Coq mailing list

["Satrajit Roy" <satrajit.roy AT gmail.com>]

Thank you folks. That was very helpful.

 

While on the subject though, I have one more basic question.

 

Are there tactics already available for proving inequalities like the following:

 

(f (x + m)) (>= or <=) (g (y + n)) given that that m >= n and (f x) >=  (g x) where f and g are monotonous functions involving arithmetic operations? 

 

Frama-C generates quite a few goals like that for pointer validation.

Thanks again.

 

On Thu, Oct 30, 2008 at 5:34 PM, Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr> wrote:

On Thu, Oct 30, 2008 at 01:19:13PM -0700, Andrew McCreight wrote:
>
> If there's a better way to prove these sorts of things, I'd love to know
> about it.
>
> -Andrew
>

Hi Satrajit, Hi Andrew,

Indeed, proving things about Zdiv can be quite tedious. In particular,
lots of properties are lacking in the Zdiv.v file of Coq 8.1 and
earlier. Some months ago, I've tried to improve this situation, by
collecting various tids and bits about Zdiv and adding mine. As a
result, the Zdiv.v coming along with the next version 8.2 should be
more decent. Beta versions of this 8.2 are already available, I
encourage you to have a test and check whether this new Zdiv.v fits
your needs, see http://coq.inria.fr/V8.2beta/. The content of Zdiv.v
can be accessed directly at:

https://gforge.inria.fr/plugins/scmsvn/viewcvs.php/branches/v8.2/theories/ZArith/Zdiv.v?root=coq&view=markup

For instance, your example can now be proved this way:

Lemma test : forall z,
 z > 0 -> z <> 1 -> 4*(z-1)/4-1 >= 0.
Proof.
intros.
apply Zle_ge. (* we switch from >= to <= (more results about <=) *)
apply Zle_minus_le_0. (* we move the -1 to the left hand-side *)
apply Zdiv_le_lower_bound; auto with zarith.
Qed.

Best,
Pierre Letouzey

PS: Since the initial exemple mentionned things like int32 that sounds
quite hardware-related, you might be interested by two other additions
to this forthcoming 8.2 :
 - I've added an alternate division named ZOdiv (see ZOdiv_defs.v and
ZOdiv.v at the same place as Zdiv.v). The idea is that (Zdiv a b) when
(b<0) does _not_ follow the convention of most languages (Ocaml,C,...)
and processors. Unfortunately, we cannot say that there is a "good"
or "bad" behavior, so instead of "fixing" Zdiv, we propose now two
variants.
 - Coq 8.2 also provides Int31 integers in the spirit of Ocaml (see
theories/Numbers/Cyclic/Int31/Int31.v). These bounded numbers are used
in particular to provide efficient arbitrary-size integers: usual
operations upon Int31 will be computed primitively by the hardware.
You might be interested to know that this Int31.v has been carefully
crafted as to be independent of 31, you can obtain an Int32.v by a
simple sed -e "s/31/32/g", you will simply loose the "hardware
acceleration".



--------------------------------------------------------
Bug reports: http://logical.futurs.inria.fr/coq-bugs
Archives: http://pauillac.inria.fr/pipermail/coq-club
         http://pauillac.inria.fr/bin/wilma/coq-club
Info: http://pauillac.inria.fr/mailman/listinfo/coq-club