[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

12 files changed, 128 insertions, 78 deletions

diff --git a/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 53aa619d10..1018271751 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.ml
@@ -449,6 +449,8 @@ let bound_monomials (sys : WithProof.t list) =
   in
   List.map snd (List.filter has_mon bounds) @ snd l
 
+let bound_monomials = tr_sys "bound_monomials" bound_monomials
+
 let develop_constraints prfdepth n_spec sys =
   LinPoly.MonT.clear ();
   max_nb_cstr := compute_max_nb_cstr sys prfdepth;
@@ -1181,10 +1183,12 @@ let nlia enum prfdepth sys =
       It would only be safe if the variable is linear...
      *)
     let sys1 =
-      elim_simple_linear_equality (WithProof.subst_constant true sys)
+      normalise
+        (elim_simple_linear_equality (WithProof.subst_constant true sys))
     in
+    let bnd1 = bound_monomials sys1 in
     let sys2 = saturate_by_linear_equalities sys1 in
-    let sys3 = nlinear_preprocess (sys1 @ sys2) in
+    let sys3 = nlinear_preprocess (rev_concat [bnd1; sys1; sys2]) in
     let sys4 = make_cstr_system (*sys2@*) sys3 in
     (* [reduction_equations] is too brutal - there should be some non-linear reasoning  *)
     xlia (List.map fst sys) enum reduction_equations sys4
diff --git a/plugins/micromega/zify.ml b/plugins/micromega/zify.ml
index 2cb615170b..b780c1833e 100644
--- a/plugins/micromega/zify.ml
+++ b/plugins/micromega/zify.ml
@@ -59,6 +59,7 @@ let op_iff_morph = lazy (zify "iff_morph")
 let op_not = lazy (zify "not")
 let op_not_morph = lazy (zify "not_morph")
 let op_True = lazy (zify "True")
+let op_I = lazy (zify "I")
 
 (** [unsafe_to_constr c] returns a [Constr.t] without considering an evar_map.
     This is useful for calling Constr.hash *)
@@ -1538,41 +1539,51 @@ let spec_of_hyps =
 let iter_specs = spec_of_hyps
 
 let find_hyp evd t l =
-  try Some (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l))
+  try
+    Some
+      (EConstr.mkVar
+         (fst (List.find (fun (h, t') -> EConstr.eq_constr evd t t') l)))
   with Not_found -> None
 
-let sat_constr c d =
-  Proofview.Goal.enter (fun gl ->
-      let evd = Tacmach.New.project gl in
-      let env = Tacmach.New.pf_env gl in
-      let hyps = Tacmach.New.pf_hyps_types gl in
-      match EConstr.kind evd c with
-      | App (c, args) ->
-        if Array.length args = 2 then
-          let h1 =
-            Tacred.cbv_beta env evd
-              (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
-          in
-          let h2 =
-            Tacred.cbv_beta env evd
-              (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
-          in
-          match (find_hyp evd h1 hyps, find_hyp evd h2 hyps) with
-          | Some h1, Some h2 ->
-            let n =
-              Tactics.fresh_id_in_env Id.Set.empty
-                (Names.Id.of_string "__sat")
-                env
-            in
-            let trm =
-              EConstr.mkApp
-                ( d.ESatT.satOK
-                , [|args.(0); args.(1); EConstr.mkVar h1; EConstr.mkVar h2|] )
-            in
-            Tactics.pose_proof (Names.Name n) trm
-          | _, _ -> Tacticals.New.tclIDTAC
-        else Tacticals.New.tclIDTAC
-      | _ -> Tacticals.New.tclIDTAC)
+let find_proof evd t l =
+  if EConstr.eq_constr evd t (Lazy.force op_True) then Some (Lazy.force op_I)
+  else find_hyp evd t l
+
+(** [sat_constr env evd sub taclist hyps c d]= (sub',taclist',hyps') where
+    -  sub' is a fresh subscript obtained from sub
+    - taclist' is obtained from taclist by posing the lemma 'd' applied to 'c'
+    - hyps' is obtained from hyps'
+    taclist and hyps are threaded to avoid adding duplicates
+ *)
+let sat_constr env evd (sub,taclist, hyps) c d =
+  match EConstr.kind evd c with
+  | App (c, args) ->
+     if Array.length args = 2 then
+       let h1 =
+         Tacred.cbv_beta env evd
+           (EConstr.mkApp (d.ESatT.parg1, [|args.(0)|]))
+       in
+       let h2 =
+         Tacred.cbv_beta env evd
+           (EConstr.mkApp (d.ESatT.parg2, [|args.(1)|]))
+       in
+       let n = Nameops.add_subscript (Names.Id.of_string "__sat") sub in
+       let trm =
+         match (find_proof evd h1 hyps, find_proof evd h2 hyps) with
+         | Some h1, Some h2 ->
+            (EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1; h2|]))
+         | Some h1, _ ->
+            EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1); h1|])
+         | _, _ -> EConstr.mkApp (d.ESatT.satOK, [|args.(0); args.(1)|])
+       in
+       let rtrm = Tacred.cbv_beta env evd trm in
+       let typ  = Retyping.get_type_of env evd rtrm in
+       match find_hyp evd typ hyps with
+       | None -> (Nameops.Subscript.succ sub, (Tactics.pose_proof (Names.Name n) rtrm :: taclist) , (n,typ)::hyps)
+       | Some _ -> (sub, taclist, hyps)
+     else (sub,taclist,hyps)
+  | _ -> (sub,taclist,hyps)
+
 
 let get_all_sat env evd c =
   List.fold_left
@@ -1596,8 +1607,10 @@ let saturate =
           Array.iter sat args;
           if Array.length args = 2 then
             let ds = get_all_sat env evd c in
-            if ds = [] then ()
-            else List.iter (fun x -> CstrTable.HConstr.add table t x.deriv) ds
+            if ds = [] ||  CstrTable.HConstr.mem table t
+            then ()
+            else List.iter (fun x ->
+                     CstrTable.HConstr.add table t x.deriv) ds
           else ()
         | Prod (a, t1, t2) when a.Context.binder_name = Names.Anonymous ->
           sat t1; sat t2
@@ -1606,5 +1619,6 @@ let saturate =
       (* Collect all the potential saturation lemma *)
       sat concl;
       List.iter (fun (_, t) -> sat t) hyps;
-      Tacticals.New.tclTHENLIST
-        (CstrTable.HConstr.fold (fun c d acc -> sat_constr c d :: acc) table []))
+      let s0 = fresh_subscript env in
+      let (_,tacs,_) = CstrTable.HConstr.fold (fun c d acc -> sat_constr env evd acc c d) table (s0,[],hyps) in
+      Tacticals.New.tclTHENLIST tacs)
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 *)
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.