Change the parser and printer so that they use IZR for real constants.

There are two main issues. First, (-cst)%R is no longer syntactically
equal to (-(cst))%R (though they are still convertible). This breaks some
rewriting rules.

Second, the ring/field_simplify tactics did not know how to refold
real constants. This defect is no longer hidden by the pretty-printer,
which makes these tactics almost unusable on goals containing large
constants.

This commit also modifies the ring/field tactics so that real constant
reification is now constant time rather than linear.

Note that there is now a bit of code duplication between z_syntax and
r_syntax. This should be fixed once plugin interdependencies are supported.

Ideally the r_syntax plugin should just disappear by declaring IZR as a
coercion. Unfortunately the coercion mechanism is not powerful enough yet,
be it for parsing (need the ability for a scope to delegate constant
parsing to another scope) or printing (too many visible coercions left).

1 files changed, 2 insertions, 2 deletions

diff --git a/theories/Reals/R_sqrt.v b/theories/Reals/R_sqrt.v
index 5c975c3f5..0c1e0b7e8 100644
--- a/theories/Reals/R_sqrt.v
+++ b/theories/Reals/R_sqrt.v
@@ -420,10 +420,10 @@ Proof.
   rewrite (Rmult_comm (/ a)).
   rewrite Rmult_assoc.
   rewrite <- Rinv_mult_distr.
-  replace (2 * (2 * a) * a) with (Rsqr (2 * a)).
+  replace (4 * a * a) with (Rsqr (2 * a)).
   reflexivity.
   ring_Rsqr.
-  rewrite <- Rmult_assoc; apply prod_neq_R0;
+  apply prod_neq_R0;
     [ discrR | apply (cond_nonzero a) ].
   apply (cond_nonzero a).
   assumption.