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, 7 insertions, 11 deletions

diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v
index fe5402e6e..df1662497 100644
--- a/theories/Reals/Rbasic_fun.v
+++ b/theories/Reals/Rbasic_fun.v
@@ -451,20 +451,16 @@ Qed.
 
 Lemma Rabs_Ropp : forall x:R, Rabs (- x) = Rabs x.
 Proof.
-  intro; cut (- x = -1 * x).
-  intros; rewrite H.
+  intro; replace (-x) with (-1 * x) by ring.
   rewrite Rabs_mult.
-  cut (Rabs (-1) = 1).
-  intros; rewrite H0.
-  ring.
+  replace (Rabs (-1)) with 1.
+  apply Rmult_1_l.
   unfold Rabs; case (Rcase_abs (-1)).
   intro; ring.
-  intro H0; generalize (Rge_le (-1) 0 H0); intros.
-  generalize (Ropp_le_ge_contravar 0 (-1) H1).
-  rewrite Ropp_involutive; rewrite Ropp_0.
-  intro; generalize (Rgt_not_le 1 0 Rlt_0_1); intro; generalize (Rge_le 0 1 H2);
-    intro; exfalso; auto.
-  ring.
+  rewrite <- Ropp_0.
+  intro H0; apply Ropp_ge_cancel in H0.
+  elim (Rge_not_lt _ _ H0).
+  apply Rlt_0_1.
 Qed.
 
 (*********)