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, 0 insertions, 9 deletions

diff --git a/theories/Reals/DiscrR.v b/theories/Reals/DiscrR.v
index 4e2a7c3c6..05911cd53 100644
--- a/theories/Reals/DiscrR.v
+++ b/theories/Reals/DiscrR.v
@@ -31,9 +31,6 @@ Ltac discrR :=
   try
    match goal with
    |  |- (?X1 <> ?X2) =>
-       change 2 with (IZR 2);
-       change 1 with (IZR 1);
-       change 0 with (IZR 0);
        repeat
          rewrite <- plus_IZR ||
            rewrite <- mult_IZR ||
@@ -52,9 +49,6 @@ Ltac prove_sup0 :=
   end.
 
 Ltac omega_sup :=
-  change 2 with (IZR 2);
-  change 1 with (IZR 1);
-  change 0 with (IZR 0);
   repeat
     rewrite <- plus_IZR ||
       rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;
@@ -72,9 +66,6 @@ Ltac prove_sup :=
   end.
 
 Ltac Rcompute :=
-  change 2 with (IZR 2);
-  change 1 with (IZR 1);
-  change 0 with (IZR 0);
   repeat
     rewrite <- plus_IZR ||
       rewrite <- mult_IZR || rewrite <- Ropp_Ropp_IZR || rewrite Z_R_minus;