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, 10 insertions, 22 deletions

diff --git a/theories/Reals/Ranalysis3.v b/theories/Reals/Ranalysis3.v
index 4e88714d6..d4597aeba 100644
--- a/theories/Reals/Ranalysis3.v
+++ b/theories/Reals/Ranalysis3.v
@@ -201,8 +201,8 @@ Proof.
   apply Rabs_pos_lt.
   unfold Rdiv, Rsqr; repeat rewrite Rmult_assoc.
   repeat apply prod_neq_R0; try assumption.
-  red; intro; rewrite H15 in H6; elim (Rlt_irrefl _ H6).
-  apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption.
+  now apply Rgt_not_eq.
+  apply Rinv_neq_0_compat; apply prod_neq_R0; [discrR | assumption].
   apply H13.
   split.
   apply D_x_no_cond; assumption.
@@ -213,8 +213,7 @@ Proof.
   red; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6).
   assumption.
   assumption.
-  apply Rinv_neq_0_compat; repeat apply prod_neq_R0;
-    [ discrR | discrR | discrR | assumption ].
+  apply Rinv_neq_0_compat; apply prod_neq_R0; [discrR | assumption].
 (***********************************)
 (*        Third case               *)
 (*     (f1 x)<>0  l1=0  l2=0       *)
@@ -224,11 +223,11 @@ Proof.
   elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x))));
     [ idtac
       | apply Rabs_pos_lt; unfold Rdiv, Rsqr; repeat rewrite Rmult_assoc;
-        repeat apply prod_neq_R0;
+        repeat apply prod_neq_R0 ;
           [ assumption
             | assumption
-            | red; intro; rewrite H11 in H6; elim (Rlt_irrefl _ H6)
-            | apply Rinv_neq_0_compat; repeat apply prod_neq_R0; discrR || assumption ] ].
+            | now apply Rgt_not_eq
+            | apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption ] ].
   intros alp_f2d H12.
   cut (0 < Rmin (Rmin eps_f2 alp_f2) (Rmin alp_f1d alp_f2d)).
   intro.
@@ -295,8 +294,10 @@ Proof.
   elim (H0 (Rabs (Rsqr (f2 x) * eps / (8 * f1 x))));
     [ idtac
       | apply Rabs_pos_lt; unfold Rsqr, Rdiv;
-        repeat rewrite Rinv_mult_distr; repeat apply prod_neq_R0;
-          try assumption || discrR ].
+        repeat apply prod_neq_R0 ;
+          [ assumption..
+            | now apply Rgt_not_eq
+            | apply Rinv_neq_0_compat; apply prod_neq_R0; discrR || assumption ] ].
   intros alp_f2d H11.
   assert (H12 := derivable_continuous_pt _ _ X).
   unfold continuity_pt in H12.
@@ -380,15 +381,9 @@ Proof.
   repeat apply prod_neq_R0; try assumption.
   red; intro H18; rewrite H18 in H6; elim (Rlt_irrefl _ H6).
   apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
   apply Rinv_neq_0_compat; assumption.
   apply Rinv_neq_0_compat; assumption.
   discrR.
-  discrR.
-  discrR.
-  discrR.
-  discrR.
   apply prod_neq_R0; [ discrR | assumption ].
   elim H13; intros.
   apply H19.
@@ -408,16 +403,9 @@ Proof.
   repeat apply prod_neq_R0; try assumption.
   red; intro H13; rewrite H13 in H6; elim (Rlt_irrefl _ H6).
   apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
   apply Rinv_neq_0_compat; assumption.
   apply Rinv_neq_0_compat; assumption.
   apply prod_neq_R0; [ discrR | assumption ].
-  red; intro H11; rewrite H11 in H6; elim (Rlt_irrefl _ H6).
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; discrR.
-  apply Rinv_neq_0_compat; assumption.
 (***********************************)
 (*         Fifth case              *)
 (*    (f1 x)<>0  l1<>0  l2=0       *)