[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

5 files changed, 15 insertions, 34 deletions

diff --git a/theories/Numbers/Cyclic/Int63/Cyclic63.v b/theories/Numbers/Cyclic/Int63/Cyclic63.v
index 2a26b6b12a..4bf971668d 100644
--- a/theories/Numbers/Cyclic/Int63/Cyclic63.v
+++ b/theories/Numbers/Cyclic/Int63/Cyclic63.v
@@ -218,7 +218,6 @@ Lemma div_lt : forall p x y, 0 <= x < y -> x / 2^p < y.
   apply Zdiv_lt_upper_bound;auto with zarith.
   apply Z.lt_le_trans with y;auto with zarith.
   rewrite <- (Zmult_1_r y);apply Zmult_le_compat;auto with zarith.
-  assert (0 < 2^p);auto with zarith.
   replace (2^p) with 0.
   destruct x;change (0<y);auto with zarith.
   destruct p;trivial;discriminate.
diff --git a/theories/Numbers/Cyclic/Int63/Int63.v b/theories/Numbers/Cyclic/Int63/Int63.v
index a3ebe67325..d3fac82d09 100644
--- a/theories/Numbers/Cyclic/Int63/Int63.v
+++ b/theories/Numbers/Cyclic/Int63/Int63.v
@@ -1428,7 +1428,7 @@ Proof.
  assert (Hp3: (0 < Φ (WW ih il))).
  {simpl zn2z_to_Z;apply Z.lt_le_trans with (φ ih * wB)%Z; auto with zarith.
   apply Zmult_lt_0_compat; auto with zarith.
-  refine (Z.lt_le_trans _ _ _ _ Hih); auto with zarith. }
+ }
  cbv zeta.
  case_eq (ih <? j)%int63;intros Heq.
  rewrite -> ltb_spec in Heq.
@@ -1465,7 +1465,6 @@ Proof.
  apply Hrec; rewrite H; clear u H.
  assert (Hf1: 0 <= Φ (WW ih il) / φ j) by (apply Z_div_pos; auto with zarith).
  case (Zle_lt_or_eq 1 (φ j)); auto with zarith; intros Hf2.
- 2: contradict Heq0; apply Zle_not_lt; rewrite <- Hf2, Zdiv_1_r; auto with zarith.
  split.
  replace (φ j + Φ (WW ih il) / φ j)%Z with
         (1 * 2 + ((φ j - 2) + Φ (WW ih il) / φ j)) by lia.
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.