diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-03-05 20:48:52 +0100 |
|---|---|---|
| committer |  Maxime Dénès <mail@maximedenes.fr> | 2017-03-22 17:19:51 +0100 |
| commit | a4a76c253474ac4ce523b70d0150ea5dcf546385 (patch) | |
| tree | ebde19ff337a88fd8029ac5dc9eca03df1202367 /theories/Reals/Rbasic_fun.v | |
| parent | ddbc3839923731686a89a401d0f9dd44f3ad339b (diff) | |
Make IZR use a compact representation of integers.
That way, (IZR 5) is no longer reduced to 2 + 1 + 1 + 1 (which is not
convertible to 5) but instead to 1 + 2 * 2 (which is). Moreover, it means
that, after reduction, real constants no longer exponentially blow up.
Note that I was not able to fix the test-suite for the declarative mode,
so the missing proof terms have been admitted.
Diffstat (limited to 'theories/Reals/Rbasic_fun.v')
| -rw-r--r-- | theories/Reals/Rbasic_fun.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/theories/Reals/Rbasic_fun.v b/theories/Reals/Rbasic_fun.v index c889d7347..fe5402e6e 100644 --- a/theories/Reals/Rbasic_fun.v +++ b/theories/Reals/Rbasic_fun.v @@ -613,11 +613,12 @@ Qed. Lemma Rabs_Zabs : forall z:Z, Rabs (IZR z) = IZR (Z.abs z). Proof. - intros z; case z; simpl; auto with real. - apply Rabs_right; auto with real. - intros p0; apply Rabs_right; auto with real zarith. + intros z; case z; unfold Zabs. + apply Rabs_R0. + now intros p0; apply Rabs_pos_eq, (IZR_le 0). + unfold IZR at 1. intros p0; rewrite Rabs_Ropp. - apply Rabs_right; auto with real zarith. + now apply Rabs_pos_eq, (IZR_le 0). Qed. Lemma abs_IZR : forall z, IZR (Z.abs z) = Rabs (IZR z). |