diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-05 21:03:51 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 17:31:30 +0100 |
| commit | e1ef9491edaf8f7e6f553c49b24163b7e2a53825 (patch) | |
| tree | 08f89d143cfc92de4a4d7fe80aa13cb8d5137f20 /theories/Reals/ArithProp.v | |
| parent | a4a76c253474ac4ce523b70d0150ea5dcf546385 (diff) | |
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).
Diffstat (limited to 'theories/Reals/ArithProp.v')
| -rw-r--r-- | theories/Reals/ArithProp.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Reals/ArithProp.v b/theories/Reals/ArithProp.v index 7d9fff276..67584f775 100644 --- a/theories/Reals/ArithProp.v +++ b/theories/Reals/ArithProp.v @@ -106,7 +106,7 @@ Proof. split. ring. unfold k0; case (Rcase_abs y) as [Hlt|Hge]. - assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; change (IZR 1) with 1; + assert (H0 := archimed (x / - y)); rewrite <- Z_R_minus; simpl; unfold Rminus. replace (- ((1 + - IZR (up (x / - y))) * y)) with ((IZR (up (x / - y)) - 1) * y); [ idtac | ring ]. @@ -140,10 +140,10 @@ Proof. rewrite <- Ropp_mult_distr_r_reverse; rewrite (Ropp_inv_permute _ H); elim H0; unfold Rdiv; intros H1 _; exact H1. apply Ropp_neq_0_compat; assumption. - assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; change (IZR 1) with 1; + assert (H0 := archimed (x / y)); rewrite <- Z_R_minus; simpl; cut (0 < y). intro; unfold Rminus; - replace (- ((IZR (up (x / y)) + -1) * y)) with ((1 - IZR (up (x / y))) * y); + replace (- ((IZR (up (x / y)) + -(1)) * y)) with ((1 - IZR (up (x / y))) * y); [ idtac | ring ]. split. apply Rmult_le_reg_l with (/ y). |