plugin micromega : nra also handles non-linear rational arithmetic over Q (Fixed #4985)

Lqa.v defines the tactics lra and nra working over Q.
Lra.v defines the tactics lra and nra working over R.

2 files changed, 15 insertions, 14 deletions

diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index 47e6005b9..d001e8f7f 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -6,32 +6,29 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import Psatz.
+Require Import Lqa.
 Require Import QArith.
 
 Lemma plus_minus : forall x y,
   0 == x + y -> 0 ==  x -y -> 0 == x /\ 0 == y.
 Proof.
   intros.
-  psatzl Q.
+  lra.
 Qed.
 
-
-
-
 (* Other (simple) examples *)
 Open Scope Q_scope.
 
 Lemma binomial : forall x y:Q, ((x+y)^2 == x^2 + (2 # 1) *x*y + y^2).
 Proof.
   intros.
-  psatzl Q.
+  lra.
 Qed.
 
 
 Lemma hol_light19 : forall m n, (2 # 1) * m + n == (n + m) + m.
 Proof.
-  intros ; psatzl Q.
+  intros ; lra.
 Qed.
 Open Scope Z_scope.
 Open Scope Q_scope.
@@ -60,7 +57,11 @@ Lemma vcgen_25 : forall
   (( 1# 1) == (-2 # 1) * i + it).
 Proof.
   intros.
-  psatzl Q.
+  lra.
+Qed.
+
+Goal forall x : Q, x * x >= 0.
+  intro; nra. 
 Qed.
 
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 2eed7e951..89c08c770 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -6,7 +6,7 @@
 (*                                                                      *)
 (************************************************************************)
 
-Require Import Psatz.
+Require Import Lra.
 Require Import Reals.
 
 Open Scope R_scope.
@@ -15,7 +15,7 @@ Lemma yplus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
-  psatzl R.
+  lra.
 Qed.
 
 (* Other (simple) examples *)
@@ -23,13 +23,13 @@ Qed.
 Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2).
 Proof.
   intros.
-  psatzl R.
+  lra.
 Qed.
 
 
 Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
 Proof.
-  intros ; psatzl R.
+  intros ; lra.
 Qed.
 
 
@@ -57,7 +57,7 @@ Lemma vcgen_25 : forall
   (( 1 ) = (-2  ) * i + it).
 Proof.
   intros.
-  psatzl R.
+  lra.
 Qed.
 
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
@@ -72,5 +72,5 @@ Proof.
 Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
-intros; split_Rabs; psatzl R.
+intros; split_Rabs; lra.
 Qed.
\ No newline at end of file