Ana de Almeida Borges (Apr 12 2023 at 14:32): Ana de Almeida Borges (Apr 12 2023 at 14:32):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?
Michael Soegtrop (Apr 12 2023 at 16:33):@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
Michael Soegtrop (Apr 12 2023 at 16:35):The advantage (in the VST context) of the tactic I have is that it can handle a mix of CompCert integers and Z
Bas Spitters (Apr 13 2023 at 09:34):@Andres Erbsen has been very helpful in making some of the fiat-crypto work more generally available, so he may be interested in this.
Karl Palmskog (Apr 13 2023 at 11:11):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.
Michael Soegtrop (Apr 13 2023 at 12:11):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.
Ana de Almeida Borges (Apr 13 2023 at 13:59):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.
Michael Soegtrop (Apr 13 2023 at 14:57):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: Oct 13 2024 at 01:02 UTC