Michael Soegtrop said:

[...]

I have e reflexive tactic which computes bounds of integer arithmetic expressions (similar to coq-interval, but specialised on integers).

[...]

@Michael Soegtrop is this tactic publicly available?

@Ana de Almeida Borges : not yet, but I plan to either do a PR to VST or publish it separately soon after the Coq Platform release. Please note that fiat-crypto has a nice lemma library for integer range arithmetic here

The advantage (in the VST context) of the tactic I have is that it can handle a mix of CompCert integers and Z

@Andres Erbsen has been very helpful in making some of the fiat-crypto work more generally available, so he may be interested in this.

the best thing would be to move the integer range arithmetic lemma to the `coq-coqutil`

package, which is easier to install than fiat-crypto. We already have a Coq-community issue about this general effort.

fiat-crypto is also in Coq Platform since the 2022.09 release, which should make such utilities much more accessible.

@Ana de Almeida Borges : in case you have an urgent need I can see what I can do quicker - maybe you can post me an example goal in a PM and I can see if it is suitable at all. I got pretty far with a combination of coq-interval and gappa (for converting Z to R division), but at some point it became simply to slow for my purposes and also in rare cases I had issues with proving tight bounds.

Thanks! I am in no urgent need at all, merely curious. I've been using a very dumb but effective tactic, which was developed before we discovered `coq-interval`

and `mczify`

. Now I'm comparing every similar-purpose tactic I find.

I had a look at the examples at the end of the file - it looks similar to what I do with my tactic.

A note: you can use gappa to convert the integer divisions to real divisions - gappa can do the deviation proofs between Z divisions seen as approximations to R divisions. It is a bit awkward to use, though - especially error messages are not always terribly informative and it is quite picky about the formulation of goals. If you never used it, I can send you examples for combining interval and gappa.

Interval can also do such proofs using Zfloor, but gappa can do much more complicated things like heavily nested divisions like one has in a polynomial approximation. As far as I can tell as long as one does not nest divisions (or Zfloor calls), interval can handle them quite efficiently. In this sense your examples 1 and 2 might be on the edge for interval without gappa, while 3..5 should be fine. (I am assuming %/ means integer division).

Last updated: Jul 23 2024 at 21:01 UTC