The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 06/29/2016 11:45 AM, Soegtrop, Michael wrote:
> Dear Arnaud,
>
>
>
> thanks a lot for the detailed explanation – the “Register” process
> doesn’t seem to be documented in the reference manual, so this is very
> welcome.
>
>
>
> I would say the trust base increase is not that much of a problem, as
> long as this can be switched off easily. I don’t see how this would be
> done in the current implementation of Int32 (other than copying the
> library and removing the register keyword). I would use such features
> mostly for interactive development and use the plain Coq implementation
> in overnight check runs, where speed doesn’t matter that much.

Hi,

The first version of the Big library as described in

A Purely Functional Library for Modular Arithmetic and Its Application 
to Certifying Large Prime Numbers. IJCAR 2006.

was using what you propose. A type with 2^n constructions such that the 
basic operations where encoded by direct pattern matching.
My memory was the biggest n Coq could handle was n = 8.
Then thanks to Arnaud we use the native int31 but I agree with you
it would be good to give the possibility to switch to a "safe" mode.

-
Laurent






We were using

> Btw.: has it been tried to use e.g. hex digit representations in Coq?
> This thesis analyses the speed up of multi-bit digit arithmetic in HOL:
>
>
>
> FORMAL COMPUTATIONS AND METHODS by Alexey Solovyev, Pittsburgh, 2007
>
>
>
> http://d-scholarship.pitt.edu/16721/7/SolovyevThesis_(v._1.02).pdf
>
>
>
> For 5 decimal digit numbers the speed up is about 2.5, from 10 decimal
> digits on one gets a speed increase of about 4 times for 4 bit digits.
>
>
>
> Best regards,
>
>
>
> Michael
>
> Intel Deutschland GmbH
> Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
> Tel: +49 89 99 8853-0, www.intel.de
> Managing Directors: Christin Eisenschmid, Christian Lamprechter
> Chairperson of the Supervisory Board: Nicole Lau
> Registered Office: Munich
> Commercial Register: Amtsgericht Muenchen HRB 186928