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, 4 insertions, 1 deletions

diff --git a/theories/Reals/Ranalysis5.v b/theories/Reals/Ranalysis5.v
index d172139f5..f9da88aad 100644
--- a/theories/Reals/Ranalysis5.v
+++ b/theories/Reals/Ranalysis5.v
@@ -249,8 +249,10 @@ assert (Sublemma : forall x y lb ub, lb <= x <= ub /\ lb <= y <= ub -> lb <= (x+
   split.
   replace lb with ((lb + lb) * /2) by field.
   unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
+  now apply Rlt_le, Rinv_0_lt_compat, IZR_lt.
   replace ub with ((ub + ub) * /2) by field.
   unfold Rdiv ; apply Rmult_le_compat_r ; intuition.
+  now apply Rlt_le, Rinv_0_lt_compat, IZR_lt.
 intros x y P N x_lt_y.
 induction N.
  simpl ; intuition.
@@ -1030,6 +1032,7 @@ intros x ub lb lb_lt_x x_lt_ub.
  assert (T : 0 < ub - lb).
   fourier.
  unfold Rdiv ; apply Rlt_mult_inv_pos ; intuition.
+now apply IZR_lt.
 Qed.
 
 Definition mkposreal_lb_ub (x lb ub:R) (lb_lt_x:lb<x) (x_lt_ub:x<ub) : posreal.
@@ -1102,7 +1105,7 @@ assert (Main : Rabs ((f (x+h) - fn N (x+h)) - (f x - fn N x) + (fn N (x+h) - fn
     rewrite <- Rmult_1_r ; replace 1 with (derive_pt id c (pr2 c P)) by reg.
     replace (- (fn N (x + h) - fn N x)) with (fn N x - fn N (x + h)) by field.
     assumption.
-   solve[apply Rlt_not_eq ; intuition].
+  now apply Rlt_not_eq, IZR_lt.
   rewrite <- Hc'; clear Hc Hc'.
   replace (derive_pt (fn N) c (pr1 c P)) with (fn' N c).
   replace (h * fn' N c - h * g x) with (h * (fn' N c - g x)) by field.