Imported Upstream snapshot 8.3~beta0+13298

7 files changed, 36 insertions, 26 deletions

diff --git a/test-suite/micromega/csdp.cache b/test-suite/micromega/csdp.cache
new file mode 100644
index 00000000..645de69c
--- /dev/null
+++ b/test-suite/micromega/csdp.cache
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index 751fe91e..f424f0fc 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -19,7 +19,7 @@ Lemma not_so_easy : forall x n : Z,
   2*x + 1 <= 2 *n -> x <= n-1.
 Proof.
   intros.
-  lia. 
+  lia.
 Qed.
 
 
@@ -27,19 +27,19 @@ Qed.
 
 Lemma some_pol : forall x, 4 * x ^ 2 + 3 * x + 2 >= 0.
 Proof.
-  intros. 
-  psatz Z 2. 
+  intros.
+  psatz Z 2.
 Qed.
 
 
-Lemma Zdiscr: forall a b c x, 
+Lemma Zdiscr: forall a b c x,
   a * x ^ 2 + b * x + c = 0 -> b ^ 2 - 4 * a * c >= 0.
 Proof.
   intros ; psatz Z 4.
 Qed.
 
 
-Lemma plus_minus : forall x y, 
+Lemma plus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
@@ -48,20 +48,20 @@ Qed.
 
 
 
-Lemma mplus_minus : forall x y, 
+Lemma mplus_minus : forall x y,
   x + y >= 0 -> x -y >= 0 -> x^2 - y^2 >= 0.
 Proof.
   intros; psatz Z 2.
 Qed.
 
-Lemma pol3: forall x y, 0 <= x + y ->  
+Lemma pol3: forall x y, 0 <= x + y ->
   x^3 + 3*x^2*y + 3*x* y^2 + y^3 >= 0.
 Proof.
   intros; psatz Z 4.
 Qed.
 
 
-(* Motivating example from: Expressiveness + Automation + Soundness: 
+(* Motivating example from: Expressiveness + Automation + Soundness:
    Towards COmbining SMT Solvers and Interactive Proof Assistants *)
 Parameter rho : Z.
 Parameter rho_ge : rho >= 0.
@@ -76,7 +76,7 @@ Definition rbound2 (C:Z -> Z -> Z) : Prop :=
 
 
 Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t  /\ correct q t /\
-  rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D  -> 
+  rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D  ->
   Zabs (C p t - D q t) <= Zabs (C p s - D q s) + 2 * rho * (t- s).
 Proof.
   intros.
@@ -194,8 +194,8 @@ Qed.
 (* from hol_light/Examples/sos.ml *)
 
 Lemma hol_light1 : forall a1 a2 b1 b2,
-  a1 >= 0 -> a2 >= 0 -> 
-   (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) -> 
+  a1 >= 0 -> a2 >= 0 ->
+   (a1 * a1 + a2 * a2 = b1 * b1 + b2 * b2 + 2) ->
    (a1 * b1 + a2 * b2 = 0) -> a1 * a2 - b1 * b2 >= 0.
 Proof.
   intros ; psatz Z 4.
@@ -323,7 +323,7 @@ Proof.
 Qed.
 
 
-Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 -> 
+Lemma hol_light24 : forall x1 y1 x2 y2, x1 >= 0 -> x2 >= 0 -> y1 >= 0 -> y2 >= 0 ->
   ((x1 + y1) ^2 + x1 + 1 = (x2 + y2) ^ 2 + x2 + 1)
                 -> (x1 + y1 = x2 + y2).
 Proof.
@@ -333,7 +333,8 @@ Qed.
 
 Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - 3*x^2*y^2) >= 0.
 Proof.
-  intros ; psatz Z.
+  intros.
+  psatz Z 1.
 Qed.
 
 
diff --git a/test-suite/micromega/heap3_vcgen_25.v b/test-suite/micromega/heap3_vcgen_25.v
index 0298303f..efb5c7fd 100644
--- a/test-suite/micromega/heap3_vcgen_25.v
+++ b/test-suite/micromega/heap3_vcgen_25.v
@@ -11,7 +11,7 @@ Require Import Psatz.
 
 Open Scope Z_scope.
 
-Lemma vcgen_25 : forall   
+Lemma vcgen_25 : forall
   (n : Z)
   (m : Z)
   (jt : Z)
diff --git a/test-suite/micromega/qexample.v b/test-suite/micromega/qexample.v
index 1fa250e0..76dc52e6 100644
--- a/test-suite/micromega/qexample.v
+++ b/test-suite/micromega/qexample.v
@@ -10,7 +10,7 @@ Require Import Psatz.
 Require Import QArith.
 Require Import Ring_normalize.
 
-Lemma plus_minus : forall x y, 
+Lemma plus_minus : forall x y,
   0 == x + y -> 0 ==  x -y -> 0 == x /\ 0 == y.
 Proof.
   intros.
@@ -37,7 +37,7 @@ Qed.
 Open Scope Z_scope.
 Open Scope Q_scope.
 
-Lemma vcgen_25 : forall   
+Lemma vcgen_25 : forall
   (n : Q)
   (m : Q)
   (jt : Q)
@@ -67,12 +67,12 @@ Qed.
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
 Proof.
   intros.
-  psatz Q 2.
+  psatz Q 3.
 Qed.
 
 Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 # 1) *x^2*y^2) >= 0.
 Proof.
-  intros ; psatz Q.
+  intros ; psatz Q 3.
 Qed.
 
 
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index d7386a4e..9bb9dacc 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -12,7 +12,7 @@ Require Import Ring_normalize.
 
 Open Scope R_scope.
 
-Lemma yplus_minus : forall x y, 
+Lemma yplus_minus : forall x y,
   0 = x + y -> 0 =  x -y -> 0 = x /\ 0 = y.
 Proof.
   intros.
@@ -34,7 +34,7 @@ Proof.
 Qed.
 
 
-Lemma vcgen_25 : forall   
+Lemma vcgen_25 : forall
   (n : R)
   (m : R)
   (jt : R)
@@ -64,12 +64,12 @@ Qed.
 Goal forall x, -x^2 >= 0 -> x - 1 >= 0 -> False.
 Proof.
   intros.
-  psatz R 2.
+  psatz R 3.
 Qed.
 
 Lemma motzkin' : forall x y, (x^2+y^2+1)*(x^2*y^4 + x^4*y^2 + 1 - (3 ) *x^2*y^2) >= 0.
 Proof.
-  intros ; psatz R.
+  intros ; psatz R 2.
 Qed.
 
 Lemma l1 : forall x y z : R, Rabs (x - z) <= Rabs (x - y) + Rabs (y - z).
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index b78bba25..4c00ffe4 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -20,7 +20,7 @@ Proof.
 intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p).
 assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2
          /\ Zabs p^2 = p^2) by auto.
-assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by 
+assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by
   (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2).
 generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
 intros n IHn p [Hn [Hp Heq]].
@@ -55,7 +55,7 @@ Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
 Proof.
  unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Zmult_1_r.
  intros HQeq.
- assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by 
+ assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by
    (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
  assert (Hnx : (Qnum x <> 0)%Z)
  by (intros Hx; simpl in HQeq; rewrite Hx in HQeq; discriminate HQeq).
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 2b40f6c9..3b246023 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -20,8 +20,17 @@ Proof.
   lia.
 Qed.
 
-Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 -> 7 * x - 9 * y = 4 -> -10 <= 7 * x - 9 * y <= 4 -> False.
+Lemma omega_nightmare : forall x y, 27 <= 11 * x + 13 * y <= 45 ->  -10 <= 7 * x - 9 * y <= 4 -> False.
 Proof.
   intros ; intuition auto.
   lia.
-Qed.  
+Qed.
+
+Lemma compact_proof : forall z,
+ (z < 0) ->
+ (z >= 0) ->
+  (0 >= z \/ 0 < z) -> False.
+Proof.
+ intros.
+ lia.
+Qed.
\ No newline at end of file