Merge branch 'v8.6'

7 files changed, 195 insertions, 93 deletions

diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 52bf5ed3df..6974f8d998 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -8,7 +8,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria)      2013                             *)
+(*  Frédéric Besson (Irisa/Inria)      2013-2016                        *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -19,24 +19,24 @@ Require Import VarMap.
 Require Coq.micromega.Tauto.
 Declare ML Module "micromega_plugin".
 
+
 Ltac preprocess :=
   zify ; unfold Z.succ in * ; unfold Z.pred in *.
 
-Ltac lia :=
-  preprocess;
-  xlia ;
-  abstract (
-      intros __wit __varmap __ff ;
-      change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
-
-Ltac nia :=
-  preprocess;
-  xnlia ;
-  abstract (
-      intros __wit __varmap __ff ;
-      change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
+Ltac zchange := 
+  intros __wit __varmap __ff ;
+  change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
+  apply (ZTautoChecker_sound __ff __wit).
+
+Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity.
+
+Ltac zchecker_abstract := abstract (zchange ; vm_cast_no_check (eq_refl true)).
+
+Ltac zchecker := zchecker_abstract || zchecker_no_abstract .
+
+Ltac lia := preprocess; xlia ; zchecker.
+               
+Ltac nia := preprocess; xnlia ; zchecker.
 
 
 (* Local Variables: *)
diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v
new file mode 100644
index 0000000000..e3414b8497
--- /dev/null
+++ b/plugins/micromega/Lqa.v
@@ -0,0 +1,54 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria)      2016                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import QMicromega.
+Require Import QArith.
+Require Import RingMicromega.
+Require Import VarMap.
+Require Coq.micromega.Tauto.
+Declare ML Module "micromega_plugin".
+
+Ltac rchange := 
+  intros __wit __varmap __ff ;
+  change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
+  apply (QTautoChecker_sound __ff __wit).
+
+Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.
+Ltac rchecker_abstract   := abstract (rchange ; vm_cast_no_check (eq_refl true)).
+
+Ltac rchecker := (rchecker_abstract || rchecker_no_abstract).
+
+(** Here, lra stands for linear rational arithmetic *)
+Ltac lra := lra_Q ; rchecker.
+
+(** Here, nra stands for non-linear rational arithmetic *)
+Ltac nra := xnqa ; rchecker.
+
+Ltac xpsatz dom d :=
+  let tac := lazymatch dom with
+  | Q =>
+    (sos_Q || psatz_Q d) ;
+      (* If csdp is not installed, the previous step might not produce any
+    progress: the rest of the tactical will then fail. Hence the 'try'. *)
+      try  rchecker
+  | _ => fail "Unsupported domain"
+  end in tac.
+
+Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
+Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
+
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/Lra.v b/plugins/micromega/Lra.v
new file mode 100644
index 0000000000..4d9cf22dd5
--- /dev/null
+++ b/plugins/micromega/Lra.v
@@ -0,0 +1,55 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria)      2016                             *)
+(*                                                                      *)
+(************************************************************************)
+
+Require Import RMicromega.
+Require Import QMicromega.
+Require Import Rdefinitions.
+Require Import RingMicromega.
+Require Import VarMap.
+Require Coq.micromega.Tauto.
+Declare ML Module "micromega_plugin".
+
+Ltac rchange := 
+  intros __wit __varmap __ff ;
+  change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
+  apply (RTautoChecker_sound __ff __wit).
+
+Ltac rchecker_no_abstract := rchange ; vm_compute ; reflexivity.
+Ltac rchecker_abstract   := abstract (rchange ; vm_cast_no_check (eq_refl true)).
+
+Ltac rchecker := rchecker_abstract || rchecker_no_abstract.
+
+(** Here, lra stands for linear real arithmetic *)
+Ltac lra := unfold Rdiv in * ;   lra_R ; rchecker.
+
+(** Here, nra stands for non-linear real arithmetic *)
+Ltac nra := unfold Rdiv in * ; xnra ; rchecker.
+
+Ltac xpsatz dom d :=
+  let tac := lazymatch dom with
+  | R =>
+    (sos_R || psatz_R d) ;
+    (* If csdp is not installed, the previous step might not produce any
+    progress: the rest of the tactical will then fail. Hence the 'try'. *)
+    try rchecker
+  | _ => fail "Unsupported domain"
+ end in tac.
+
+Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
+Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
+
+
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index fafd8a5f21..c81c025a55 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -8,7 +8,7 @@
 (*                                                                      *)
 (* Micromega: A reflexive tactic using the Positivstellensatz           *)
 (*                                                                      *)
-(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2016                             *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -21,50 +21,30 @@ Require Import Rdefinitions.
 Require Import RingMicromega.
 Require Import VarMap.
 Require Coq.micromega.Tauto.
-Declare ML Module "micromega_plugin".
+Require Lia.
+Require Lra.
+Require Lqa.
 
-Ltac preprocess := 
-    zify ; unfold Z.succ in * ; unfold Z.pred in *.
+Declare ML Module "micromega_plugin".
 
-Ltac lia :=
-  preprocess;
-  xlia ;
-  abstract (
-  intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
+Ltac lia := Lia.lia.
 
-Ltac nia :=
-  preprocess;
-  xnlia ;
-  abstract (
-  intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)).
+Ltac nia := Lia.nia.
 
 
 Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | Z =>
-    (sos_Z || psatz_Z d) ;
-      abstract(
-    intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-    apply (ZTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true))
+    (sos_Z || psatz_Z d) ; Lia.zchecker
   | R =>
     (sos_R || psatz_R d) ;
     (* If csdp is not installed, the previous step might not produce any
     progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try (abstract(intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-        apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
-  | Q =>
-    (sos_Q || psatz_Q d) ;
+    try Lra.rchecker
+  | Q => (sos_Q || psatz_Q d) ;
     (* If csdp is not installed, the previous step might not produce any
     progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try  (abstract(intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-        apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
+    try  Lqa.rchecker
   | _ => fail "Unsupported domain"
   end in tac.
 
@@ -73,22 +53,9 @@ Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1).
 
 Ltac psatzl dom :=
   let tac := lazymatch dom with
-  | Z => lia
-  | Q =>
-    psatzl_Q ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try (abstract(intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ;
-        apply (QTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
-  | R =>
-    unfold Rdiv in * ; 
-    psatzl_R ;
-    (* If csdp is not installed, the previous step might not produce any
-    progress: the rest of the tactical will then fail. Hence the 'try'. *)
-    try abstract((intros __wit __varmap __ff ;
-        change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-        apply (RTautoChecker_sound __ff __wit); vm_cast_no_check (eq_refl true)))
+  | Z => Lia.lia
+  | Q => Lqa.lra
+  | R => Lra.lra
   | _ => fail "Unsupported domain"
   end in tac.
 
@@ -97,13 +64,7 @@ Ltac lra :=
   first [ psatzl R | psatzl Q ].
 
 Ltac nra := 
-  unfold Rdiv in * ; 
-  xnra ;     
-  abstract 
-    (intros __wit __varmap __ff ;
-     change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ;
-     apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
-                                                                       
+  first [ Lra.nra | Lqa.nra ].  
 
 
 (* Local Variables: *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index b8e5e66cab..faf3b3e69d 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1437,7 +1437,36 @@ let rcst_domain_spec  = lazy {
 
 open Proofview.Notations
 
- 
+(** Naive topological sort of constr according to the subterm-ordering *)
+
+(* An element is minimal x is minimal w.r.t y if 
+   x <= y or (x and y are incomparable) *)
+
+let is_min le x y =
+  if le x y then true
+  else    if le y x then false else true
+
+let is_minimal le l c = List.for_all (is_min le c) l
+    
+let find_rem p l =
+  let rec xfind_rem  acc l =
+    match l with
+    | [] -> (None, acc)
+    | x :: l -> if p x then (Some x, acc @ l)
+      else xfind_rem (x::acc) l in
+  xfind_rem [] l
+
+let find_minimal le l = find_rem (is_minimal le l) l
+  
+let rec mk_topo_order le l =
+  match find_minimal le l with
+  | (None , _) -> []
+  | (Some v,l') -> v ::  (mk_topo_order le l')
+
+    
+let topo_sort_constr l = mk_topo_order Termops.dependent l
+
+
 (**
   * Instanciate the current Coq goal with a Micromega formula, a varmap, and a
   * witness.
@@ -1464,7 +1493,7 @@ let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*
       ]
       (Tacmach.pf_concl gl))
    ;
-   Tactics.generalize env ;
+      Tactics.generalize (topo_sort_constr env) ;
    Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
   ] 
   end }
@@ -1774,7 +1803,7 @@ let micromega_order_changer cert env ff  =
          ("__wit", cert, cert_typ)
         ]
         (Tacmach.pf_concl gl)));
-      Tactics.generalize env ;
+      Tactics.generalize (topo_sort_constr env) ;
       Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
      ]
   end }
@@ -1851,7 +1880,7 @@ module Cache = PHashtable(struct
   let hash  = Hashtbl.hash
 end)
 
-let csdp_cache = "csdp.cache"
+let csdp_cache = ".csdp.cache"
 
 (**
   * Build the command to call csdpcert, and launch it. This in turn will call
@@ -1997,9 +2026,9 @@ module CacheQ = PHashtable(struct
   let hash  = Hashtbl.hash
 end)
 
-let memo_zlinear_prover = CacheZ.memo "lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s)
-let memo_nlia = CacheZ.memo "nlia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s)
-let memo_nra = CacheQ.memo "nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
+let memo_zlinear_prover = CacheZ.memo ".lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s)
+let memo_nlia = CacheZ.memo ".nia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s)
+let memo_nra = CacheQ.memo ".nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
 
 
  
@@ -2064,7 +2093,6 @@ let non_linear_prover_Z str o  = {
   pp_f    =  fun o x -> pp_pol pp_z o (fst x)
 }
 
-
 let linear_Z =   {
   name    = "lia";
  get_option = get_lia_option;
@@ -2100,11 +2128,7 @@ let tauto_lia ff =
   * solvers
   *)
 
-let psatzl_Z =
- micromega_gen parse_zarith  Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
-  [ linear_Z ] 
-
-let psatzl_Q =
+let lra_Q =
  micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
   [ linear_prover_Q ] 
 
@@ -2112,7 +2136,7 @@ let psatz_Q i  =
  micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
   [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ]
 
-let psatzl_R  =
+let lra_R  =
  micromega_genr [ linear_prover_R ]
 
 let psatz_R i  =
@@ -2136,21 +2160,21 @@ let sos_R  =
  micromega_genr  [ non_linear_prover_R "pure_sos" None ] 
 
 
-let xlia  =
-  try 
-    micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
+let xlia  =  micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ linear_Z ] 
-  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 let xnlia  =
-  try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
       [ nlinear_Z ] 
-  with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
 let nra  = 
  micromega_genr  [ nlinear_prover_R ] 
 
+let nqa  =
+ micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
+  [ nlinear_prover_R ]
+
+   
 
 (* Local Variables: *)
 (* coding: utf-8 *)
diff --git a/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index e6b5cc60d4..974dcee870 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.ml4
@@ -37,6 +37,12 @@ TACTIC EXTEND NRA
 [ "xnra"  ] -> [  (Coq_micromega.nra)]
 END
 
+TACTIC EXTEND NQA
+[ "xnqa"  ] -> [  (Coq_micromega.nqa)]
+END
+
+
+  
 TACTIC EXTEND Sos_Z
 | [ "sos_Z" ] -> [ (Coq_micromega.sos_Z) ]
    END
@@ -50,11 +56,11 @@ TACTIC EXTEND Sos_R
 END
 
 TACTIC EXTEND LRA_Q
-[ "psatzl_Q"  ] -> [   (Coq_micromega.psatzl_Q) ]
+[ "lra_Q"  ] -> [   (Coq_micromega.lra_Q) ]
 END
 
 TACTIC EXTEND LRA_R
-[ "psatzl_R"  ] -> [   (Coq_micromega.psatzl_R) ]
+[ "lra_R"  ] -> [   (Coq_micromega.lra_R) ]
 END
 
 TACTIC EXTEND PsatzR
diff --git a/plugins/micromega/vo.itarget b/plugins/micromega/vo.itarget
index bf6a1a7db2..cb4b2b8a55 100644
--- a/plugins/micromega/vo.itarget
+++ b/plugins/micromega/vo.itarget
@@ -10,4 +10,6 @@ Tauto.vo
 VarMap.vo
 ZCoeff.vo
 ZMicromega.vo
-Lia.vo
\ No newline at end of file
+Lia.vo
+Lqa.vo
+Lra.vo
\ No newline at end of file