diff options
| author | Frédéric Besson | 2019-12-09 15:28:14 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-12-17 11:14:21 +0100 |
| commit | 7d961a914a8eaa889a982a4f84b3ba368d9e8ebc (patch) | |
| tree | ff057865c1656b2c2db45f25f4f3fb08b15103c0 /theories/QArith | |
| parent | 82918ec41ccab3b1623e41139b448938f4760a80 (diff) | |
[micromega] fix efficiency regression
PR #9725 fixes completness bugs introduces some inefficiency. The
current PR intends to fix the inefficiency while retaining
completness. The fix removes a pre-processing step and instead relies
on a more elaborate proof format introducing positivity constraints on
the fly.
Solve bootstrapping issues: RMicromega <-> Rbase <-> lia.
Fixes #11063 and fixes #11242 and fixes #11270
Diffstat (limited to 'theories/QArith')
| -rw-r--r-- | theories/QArith/Qreals.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v index 5b3d6ea30e..b1f0d9bc39 100644 --- a/theories/QArith/Qreals.v +++ b/theories/QArith/Qreals.v @@ -8,7 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -Require Export Rbase. +Require Import Rdefinitions Raxioms RIneq. Require Export QArith_base. (** Injection of rational numbers into real numbers. *) @@ -48,7 +48,7 @@ set (Y1 := IZR y1) in *; assert (Y2nz := IZR_nz y2); set (Y2 := IZR (Zpos y2)) in *. assert ((X1 * Y2)%R = (Y1 * X2)%R). unfold X1, X2, Y1, Y2; do 2 rewrite <- mult_IZR. - apply IZR_eq; auto. +f_equal; auto. clear H. field_simplify_eq; auto. rewrite H0; ring. |