[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

2 files changed, 57 insertions, 39 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)