[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

3 files changed, 14 insertions, 31 deletions

diff --git a/theories/micromega/Zify.v b/theories/micromega/Zify.v
index 01cc9ad810..3a50001b1f 100644
--- a/theories/micromega/Zify.v
+++ b/theories/micromega/Zify.v
@@ -33,5 +33,6 @@ Ltac zify := intros;
              zify_elim_let ;
              zify_op ;
              (zify_iter_specs) ;
-             zify_saturate ;
-             zify_to_euclidean_division_equations ; zify_post_hook.
+             zify_to_euclidean_division_equations ;
+             zify_post_hook;
+             zify_saturate.
diff --git a/theories/micromega/ZifyClasses.v b/theories/micromega/ZifyClasses.v
index a08a56b20e..019d11d951 100644
--- a/theories/micromega/ZifyClasses.v
+++ b/theories/micromega/ZifyClasses.v
@@ -274,3 +274,4 @@ Register impl_morph as ZifyClasses.impl_morph.
 Register not as ZifyClasses.not.
 Register not_morph as ZifyClasses.not_morph.
 Register True as ZifyClasses.True.
+Register I as ZifyClasses.I.
diff --git a/theories/micromega/ZifyInst.v b/theories/micromega/ZifyInst.v
index dd31b998d4..8dee70be45 100644
--- a/theories/micromega/ZifyInst.v
+++ b/theories/micromega/ZifyInst.v
@@ -480,39 +480,20 @@ Add Zify UnOpSpec ZabsSpec.
 
 (** Saturate positivity constraints *)
 
-Instance SatProd : Saturate Z.mul :=
-  {|
-    PArg1 := fun x => 0 <= x;
-    PArg2 := fun y => 0 <= y;
-    PRes  := fun r => 0 <= r;
-    SatOk := Z.mul_nonneg_nonneg
-  |}.
-Add Zify Saturate SatProd.
-
-Instance SatProdPos : Saturate Z.mul :=
+Instance SatPowPos : Saturate Z.pow :=
   {|
     PArg1 := fun x => 0 < x;
-    PArg2 := fun y => 0 < y;
+    PArg2 := fun y => 0 <= y;
     PRes  := fun r => 0 < r;
-    SatOk := Z.mul_pos_pos
+    SatOk := Z.pow_pos_nonneg
   |}.
-Add Zify Saturate SatProdPos.
-
-Lemma pow_pos_strict :
-  forall a b,
-    0 < a -> 0 < b -> 0 < a ^ b.
-Proof.
-  intros.
-  apply Z.pow_pos_nonneg; auto.
-  apply Z.lt_le_incl;auto.
-Qed.
-
+Add Zify Saturate SatPowPos.
 
-Instance SatPowPos : Saturate Z.pow :=
+Instance SatPowNonneg : Saturate Z.pow :=
   {|
-    PArg1 := fun x => 0 < x;
-    PArg2 := fun y => 0 < y;
-    PRes  := fun r => 0 < r;
-    SatOk := pow_pos_strict
+    PArg1 := fun x => 0 <= x;
+    PArg2 := fun y => True;
+    PRes  := fun r => 0 <= r;
+    SatOk := fun a b Ha _ => @Z.pow_nonneg a b Ha
   |}.
-Add Zify Saturate SatPowPos.
+Add Zify Saturate SatPowNonneg.