From 8193ca191cc435c108a4842ae38a11d74c7c20a5 Mon Sep 17 00:00:00 2001
From: BESSON Frederic
Date: Wed, 31 Mar 2021 22:16:50 +0200
Subject: [zify] More aggressive application of saturation rules

The role of the `zify_saturate` tactic is to augment the goal with
positivity constraints.  The premisses were previously obtained from
the context. If they are not present, we instantiate the saturation
lemma anyway.

Also,
- Remove saturation rules for Z.mul, the reasoning is performed by lia/nia
- Run zify_saturate after zify_to_euclidean_division_equations
- Better lemma for Z.power
- Ensure that lemma are generated once

Co-authored-by:  Andrej Dudenhefner  <mrhaandi>

Closes #12184, #11656
---
 test-suite/micromega/bug_11656.v   | 11 +++++++++++
 test-suite/micromega/bug_12184.v   |  8 ++++++++
 test-suite/micromega/example.v     |  6 ++++++
 test-suite/micromega/example_nia.v | 35 +++++++++++++++++++++++++++++++----
 test-suite/success/Omega.v         |  1 -
 5 files changed, 56 insertions(+), 5 deletions(-)
 create mode 100644 test-suite/micromega/bug_11656.v
 create mode 100644 test-suite/micromega/bug_12184.v

(limited to 'test-suite')

diff --git a/test-suite/micromega/bug_11656.v b/test-suite/micromega/bug_11656.v
new file mode 100644
index 0000000000..19846ad50a
--- /dev/null
+++ b/test-suite/micromega/bug_11656.v
@@ -0,0 +1,11 @@
+Require Import Lia.
+Require Import NArith.
+Open Scope N_scope.
+
+Goal forall (a b c: N),
+    a <> 0 ->
+    c <> 0 ->
+    a * ((b + 1) * c) <> 0.
+Proof.
+  intros. nia.
+Qed.
diff --git a/test-suite/micromega/bug_12184.v b/test-suite/micromega/bug_12184.v
new file mode 100644
index 0000000000..d329a3fa7f
--- /dev/null
+++ b/test-suite/micromega/bug_12184.v
@@ -0,0 +1,8 @@
+Require Import Lia.
+Require Import ZArith.
+
+Goal forall p : positive, (0 < Z.pos (2^p)%positive)%Z.
+Proof.
+  intros p.
+  lia.
+Qed.
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index d70bb809c6..d22e2b7c8c 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -12,6 +12,12 @@ Open Scope Z_scope.
 Require Import ZMicromega.
 Require Import VarMap.
 
+Lemma power_pos : forall x y, 0 <= x \/ False -> x^ y >= 0.
+Proof.
+  intros.
+  lia.
+Qed.
+
 Lemma not_so_easy : forall x n : Z,
   2*x + 1 <= 2 *n -> x <= n-1.
 Proof.
diff --git a/test-suite/micromega/example_nia.v b/test-suite/micromega/example_nia.v
index 485c24f0c9..e79b76b810 100644
--- a/test-suite/micromega/example_nia.v
+++ b/test-suite/micromega/example_nia.v
@@ -7,10 +7,16 @@
 (************************************************************************)
 
 Require Import ZArith.
-Require Import Psatz.
 Open Scope Z_scope.
-Require Import ZMicromega.
+Require Import ZMicromega Lia.
 Require Import VarMap.
+Unset Nia Cache.
+
+Goal forall (x y: Z), 0 < (1+y^2)^(x^2).
+Proof. nia. Qed.
+
+Goal forall (x y: Z), 0 <= (y^2)^x.
+Proof. nia. Qed.
 
 (* false in Q : x=1/2 and n=1 *)
 
@@ -347,8 +353,8 @@ Lemma hol_light17 : forall x y,
    -> x * y * (x + y) <= x ^ 2 + y ^ 2.
 Proof.
   intros.
-  Fail nia.
-Abort.
+  nia.
+Qed.
 
 
 Lemma hol_light18 : forall x y,
@@ -507,3 +513,24 @@ Proof.
   intros.
   lia.
 Qed.
+
+Lemma mult : forall x x0 x1 x2 n n0 n1 n2,
+    0 <= x -> 0 <= x0 -> 0 <= x1 -> 0 <= x2 ->
+    0 <= n -> 0 <= n0 -> 0 <= n1 -> 0 <= n2 ->
+    (n1 * x <= n2 * x1) ->
+    (n * x0 <= n0 * x2) ->
+  (n1 * n * (x * x0) > n2 * n0 * (x1 * x2)) -> False.
+Proof.
+  intros.
+  nia.
+Qed.
+
+
+Lemma mult_nat : forall x x0 x1 x2 n n0 n1 n2,
+    (n1 * x <= n2 * x1)%nat ->
+    (n * x0 <= n0 * x2)%nat ->
+  (n1 * n * (x * x0) > n2 * n0 * (x1 * x2))%nat -> False.
+Proof.
+  intros.
+  nia.
+Qed.
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index bbdf9762a3..a530c34297 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -1,4 +1,3 @@
-
 Require Import Lia ZArith.
 
 (* Submitted by Xavier Urbain 18 Jan 2002 *)
-- 
cgit v1.2.3