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/Rpower.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/Rpower.v')
| -rw-r--r-- | theories/Reals/Rpower.v | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/theories/Reals/Rpower.v b/theories/Reals/Rpower.v index a053c349e..f62ed2a6c 100644 --- a/theories/Reals/Rpower.v +++ b/theories/Reals/Rpower.v @@ -488,12 +488,9 @@ Proof. rewrite Rinv_r. apply exp_lt_inv. apply Rle_lt_trans with (1 := exp_le_3). - change (3 < 2 ^R 2). + change (3 < 2 ^R (1 + 1)). repeat rewrite Rpower_plus; repeat rewrite Rpower_1. - repeat rewrite Rmult_plus_distr_r; repeat rewrite Rmult_plus_distr_l; - repeat rewrite Rmult_1_l. - pattern 3 at 1; rewrite <- Rplus_0_r; replace (2 + 2) with (3 + 1); - [ apply Rplus_lt_compat_l; apply Rlt_0_1 | ring ]. + now apply (IZR_lt 3 4). prove_sup0. discrR. Qed. @@ -715,7 +712,7 @@ Definition arcsinh x := ln (x + sqrt (x ^ 2 + 1)). Lemma arcsinh_sinh : forall x, arcsinh (sinh x) = x. intros x; unfold sinh, arcsinh. assert (Rminus_eq_0 : forall r, r - r = 0) by (intros; ring). -pattern 1 at 5; rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus. +rewrite <- exp_0, <- (Rminus_eq_0 x); unfold Rminus. rewrite exp_plus. match goal with |- context[sqrt ?a] => replace a with (((exp x + exp(-x))/2)^2) by field |