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, 8 deletions

diff --git a/theories/Reals/Exp_prop.v b/theories/Reals/Exp_prop.v
index 569518f7b..e9de24898 100644
--- a/theories/Reals/Exp_prop.v
+++ b/theories/Reals/Exp_prop.v
@@ -439,20 +439,16 @@ Proof.
   repeat rewrite <- Rmult_assoc.
   rewrite <- Rinv_r_sym.
   rewrite Rmult_1_l.
-  replace (INR N * INR N) with (Rsqr (INR N)); [ idtac | reflexivity ].
-  rewrite Rmult_assoc.
-  rewrite Rmult_comm.
-  replace 4 with (Rsqr 2); [ idtac | ring_Rsqr ].
+  change 4 with (Rsqr 2).
   rewrite <- Rsqr_mult.
   apply Rsqr_incr_1.
-  replace 2 with (INR 2).
-  rewrite <- mult_INR; apply H1.
-  reflexivity.
+  change 2 with (INR 2).
+  rewrite Rmult_comm, <- mult_INR; apply H1.
   left; apply lt_INR_0; apply H.
   left; apply Rmult_lt_0_compat.
-  prove_sup0.
   apply lt_INR_0; apply div2_not_R0.
   apply lt_n_S; apply H.
+  now apply IZR_lt.
   cut (1 < S N)%nat.
   intro; unfold Rsqr; apply prod_neq_R0; apply not_O_INR; intro;
     assert (H4 := div2_not_R0 _ H2); rewrite H3 in H4;