micromega : improve efficiency/termination of type-checking

* unused terms are generalised
* proof is abstract

3 files changed, 40 insertions, 16 deletions

diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v
index 4553f03e3..add394539 100644
--- a/plugins/micromega/Lia.v
+++ b/plugins/micromega/Lia.v
@@ -19,19 +19,24 @@ Require Import VarMap.
 Require Tauto.
 Declare ML Module "micromega_plugin".
 
+Ltac preprocess :=
+  zify ; unfold Z.succ in * ; unfold Z.pred in *.
+
 Ltac lia :=
-  zify ; unfold Z.succ in * ;
+  preprocess;
   (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ;
-  intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
+  abstract (
+      intros __wit __varmap __ff ;
+      change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
+      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
 
 Ltac nia :=
-  zify ; unfold Z.succ in * ;
+  preprocess;
   xnlia ;
+  abstract (
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
+      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
 
 
 (* Local Variables: *)
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index 69b0046b9..94b1fe950 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -23,19 +23,24 @@ Require Import VarMap.
 Require Tauto.
 Declare ML Module "micromega_plugin".
 
+Ltac preprocess := 
+    zify ; unfold Z.succ in * ; unfold Z.pred in *.
+
 Ltac lia :=
-  zify ; unfold Z.succ in * ;
+  preprocess;
   (*cbv delta - [Z.add Z.sub Z.opp Z.mul Z.pow Z.gt Z.ge Z.le Z.lt iff not] ;*) xlia ;
+  abstract (
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
+      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
 
 Ltac nia :=
-  zify ; unfold Z.succ in * ;
+  preprocess;
   xnlia ;
+  abstract (
   intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
-      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
+      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity).
 
 
 Ltac xpsatz dom d :=
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 2ddd33c99..36eee9828 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -831,6 +831,11 @@ struct
    coq_Qeq, Mc.OpEq
   ]
 
+  let has_typ gl t1 typ = 
+   let ty = Retyping.get_type_of (Tacmach.pf_env gl) (Tacmach.project gl) t1 in
+   Constr.equal ty typ
+
+
   let is_convertible gl t1 t2 = 
    Reductionops.is_conv (Tacmach.pf_env gl) (Tacmach.project gl) t1 t2
 
@@ -1377,22 +1382,31 @@ let rcst_domain_spec  = lazy {
   * witness.
   *)
 
-let micromega_order_change spec cert cert_typ env ff gl =
+
+
+let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic = 
+ let ids = List.mapi (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) env in 
  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
- let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
+ let ff  = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
  let vm = dump_varmap (spec.typ) env in
+ (* todo : directly generate the proof term - or generalize befor conversion? *)
+ Tacticals.tclTHENSEQ [
+  (fun gl -> 
   Tactics.change_concl
    (set
      [
       ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
       ("__varmap", vm, Term.mkApp
        (Coqlib.gen_constant_in_modules "VarMap"
-	 [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|]));
+	 [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); 
       ("__wit", cert, cert_typ)
      ]
-     (Tacmach.pf_concl gl)
-   )
-   gl
+     (Tacmach.pf_concl gl)) gl);
+  Tactics.generalize env ;
+  Tacticals.tclTHENSEQ (List.map Tactics.introduction ids) ; 
+ ] 
+
+
 
 (**
   * The datastructures that aggregate prover attributes.