The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

To trade-off some of the correctness guarantees for speed, you may want to replace functions like Z.add (which calls BinPos.add) with native Haskell ones by adding the following imports before invoking extraction:

Require Import ExtrHaskellZInteger. 

Require Import ExtrHaskellZNum.

For better correctness guarantees, you may also want to look at:

https://coq.inria.fr/library/Coq.Numbers.Rational.BigQ.BigQ.html

Also, you may want to generalize your code to be parametrically polymorphic over an interface of rationals (see MathClasses).

Then you would be able to swap in and out various implementations of rationals easily.

(It is quite likely that much weaker interfaces suffice for parts of your code.)

-- Abhishek

http://www.cs.cornell.edu/~aa755/

On Wed, Mar 22, 2017 at 8:04 PM, Milad Ketabii <ketabii.math AT gmail.com> wrote:

Good Day

We're using coq libraries for rational arithmetic to formalize some electronic voting schemes, and then extract in Haskell to actually do the counting for a real election. Our extracted code in Haskell works fine for up tp 68 number of votes. However, when we go for 69 (or above) the program does not terminate!

When we do profiling, there is nothing strange with respect to memory consumption or time for numbers below 69. However, there is a function "add" from library "BinPos" for adding two Positives, which takes up to 70% of the memory. It seems this function is the culprit, but such behaviour is weird. Has anyone ever encountered something similar with Coq rational arithmetic before? Any suggestion is welcome.

Best

Milad