The Coq mailing list

[bertot <Yves.Bertot AT inria.fr>]

Dear all,

I had an excited memory about the progress made by CoRN as a tool to 
compute mathematical expressions, even for people like me who are 
accustomed to using Coq's standard library.  For one of my pet projects, 
I currently would like to prove that

2 ^ 3321941 < 10 ^ (10 ^ 6 + 4) < 2 ^ 3321942

I was already able to prove it in two different ways (for example direct 
computation of these comparisons using BigZ solves the goal, although it 
requires more than a minute of computation on my old laptop, the second 
approach also uses computations of powers using BigZ, but it cuts 
half-way through, by comparing 2^3302 with the corresponding power of 
10, and takes only a few seconds to verify).

Now, I would like to use a more direct proof, more in line with what I 
think a mathematician or an engineer would do: just compute the 
logarithms of 10 and 2, perform the division with enough precision, and 
that's it (it is basically how I came up with the constant 3321942 to 
begin with).

I thought I would be able to do it using CoRN, but my attempts so far 
have failed.  It seems that the library has suffered from some bit rot 
since the Kaliszyk-O'Connor paper of 2009 (JFR, Vol.2, No. 1, 2009, 
Pages 27-39).

First, I had to use the version provided in Coq's user contributions, 
because I was unable to compile the "current" version of CoRN, as 
available on github.  Then, it appeared that the example files from the 
Coq site's version are not re-compiled every night, so that the 
notations used in file CoRN/examples/RealFast.v are not working anymore, 
so that I had to perform some modifications to be able to reproduce 
something that I could copy and modify for my own experiments.  I 
provide a difference file for the naive modifications I performed just 
to be able to recompile that file.

I think it is a pity that the distributed files are not correct. This 
happens because this example file does not belong to the files that are 
verified every night, and in the end the developers who maintain these 
libraries don't see when they get broken.  These example files are 
removed from the nightly build because the y take a lot of time.  I 
would suggest to add an extra file of example that would only make small 
computations, that don't take too much time, and that would be verified 
regularly, so that issues with their maintenance would not go unnoticed.

Now, I would like to prove the following (from now on, the text is Coq 
parsable text,
so that my remarks are written inside comments).

Require Import Rsign CRsign.
Require Import Rreals_iso.


Open Scope R_scope.

Example : ln 2 < 1.

(* I just use the same tactic as found in the Kaliszyk-O'Connor paper *)

Fail R_solve_ineq (QposMake 1 2).

(* This fails, probably because Log is a partial function, you need a proof
  that 0 < 2 *)
apply R_lt_as_IR.
assert (X : Zero [<] RasIR 2).
 assert (dummy: RasIR 0 [<] RasIR 2).
  apply IR_lt_as_R; apply Rlt_0_2.
 revert dummy.
 Fail rewrite R_Zero_as_IR.
 admit.
Fail rewrite (R_ln_as_IR _ X).


(* So I you can see, I stumble from failure to failure.  Are there CoRN 
specialists around
that could help me with this problem? *)








38c38
<  let (a,b) := (approximate r (QposMake 1 m))*QposMake m 1 in
---
>  let (a,b) := (approximate r (1#m)%Qpos)*m in
43d42
< Search Q.
45c44
< Time Eval vm_compute in answer 10 ('(7#1))%CR.
---
> Time Eval vm_compute in answer 10 ('7)%CR.
55d53
< 
68c66
< Time Eval vm_compute in answer 1 (exp (compress (rational_sqrt (163#1) * 
CRpi)))%CR. 
---
> Time Eval vm_compute in answer 1 (exp (compress (rational_sqrt 163 * 
> CRpi)))%CR. 
84c82
< Example xkcd217A : (exp (CRpi) - CRpi < '(20%Z#1))%CR.
---
> Example xkcd217A : (exp (CRpi) - CRpi < '(20%Z:Q))%CR.