From 6231f07b2b7b31db93ce9fd4606450e3fa8b747f Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 30 Aug 2016 11:59:01 +0200 Subject: micromega cache files are now hidden files (cf #4156) csdp.cache -> .csdp.cache lia.cache -> .lia.cache nlia.cache -> .nia.cache --- plugins/micromega/coq_micromega.ml | 10 +++------- 1 file changed, 3 insertions(+), 7 deletions(-) (limited to 'plugins') diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index cce0a72805..fdc41eeddc 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -1766,7 +1766,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 @@ -1960,12 +1960,8 @@ module CacheZ = PHashtable(struct let hash = Hashtbl.hash end) -let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.lia) -let memo_nlia = CacheZ.memo "nlia.cache" (lift_pexpr_prover Certificate.nlia) - -(*let memo_zlinear_prover = (lift_pexpr_prover Lia.lia)*) -(*let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.zlinear_prover)*) - +let memo_zlinear_prover = CacheZ.memo ".lia.cache" (lift_pexpr_prover Certificate.lia) +let memo_nlia = CacheZ.memo ".nia.cache" (lift_pexpr_prover Certificate.nlia) let linear_Z = { -- cgit v1.2.3 From 721637c98514a77d05d080f53f226cab3a8da1e7 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Tue, 30 Aug 2016 17:12:27 +0200 Subject: plugin micromega : nra also handles non-linear rational arithmetic over Q (Fixed #4985) Lqa.v defines the tactics lra and nra working over Q. Lra.v defines the tactics lra and nra working over R. --- plugins/micromega/Lqa.v | 55 +++++++++++++++++++++++++++++++++++++ plugins/micromega/Lra.v | 56 ++++++++++++++++++++++++++++++++++++++ plugins/micromega/Psatz.v | 40 +++++++++++++++------------ plugins/micromega/coq_micromega.ml | 20 ++++++-------- plugins/micromega/g_micromega.ml4 | 10 +++++-- plugins/micromega/vo.itarget | 4 ++- 6 files changed, 152 insertions(+), 33 deletions(-) create mode 100644 plugins/micromega/Lqa.v create mode 100644 plugins/micromega/Lra.v (limited to 'plugins') diff --git a/plugins/micromega/Lqa.v b/plugins/micromega/Lqa.v new file mode 100644 index 0000000000..0055600a08 --- /dev/null +++ b/plugins/micromega/Lqa.v @@ -0,0 +1,55 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (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))) + | _ => 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..7ffe1e4ed0 --- /dev/null +++ b/plugins/micromega/Lra.v @@ -0,0 +1,56 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* + (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))) + | _ => 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..b1f242f58a 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 *) (* *) (************************************************************************) @@ -75,35 +75,39 @@ 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))) + lra_Q ; + (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))) - | _ => fail "Unsupported domain" + lra_R ; + (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)))) +| _ => fail "Unsupported domain" end in tac. Ltac lra := first [ psatzl R | psatzl Q ]. -Ltac nra := +Ltac nra_R := 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). - + change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; + apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity). + +Ltac nra_Q := + xnqa ; + (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))). + +Ltac nra := + first [ nra_R | nra_Q ]. (* Local Variables: *) diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index b8e5e66cab..edcb00b90b 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -2100,11 +2100,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 +2108,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 +2132,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 -- cgit v1.2.3 From 7d4b8108bc8fa6951e605cb9b42580ff6f8e583f Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Wed, 31 Aug 2016 19:12:15 +0200 Subject: Fix Bug #5005 : micromega tactics is now robust to failure of 'abstract'. If 'abstract' fails e.g. if there are existentials. The tactic runs an abstract-free alternative. --- plugins/micromega/Lia.v | 32 ++++++++++----------- plugins/micromega/Lqa.v | 27 +++++++++--------- plugins/micromega/Lra.v | 27 +++++++++--------- plugins/micromega/Psatz.v | 73 ++++++++++------------------------------------- 4 files changed, 57 insertions(+), 102 deletions(-) (limited to 'plugins') 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 index 0055600a08..e3414b8497 100644 --- a/plugins/micromega/Lqa.v +++ b/plugins/micromega/Lqa.v @@ -19,18 +19,21 @@ 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 ; - (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))). +Ltac lra := lra_Q ; rchecker. (** Here, nra stands for non-linear rational arithmetic *) -Ltac nra := - xnqa ; - (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))). +Ltac nra := xnqa ; rchecker. Ltac xpsatz dom d := let tac := lazymatch dom with @@ -38,9 +41,7 @@ Ltac xpsatz dom d := (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 rchecker | _ => fail "Unsupported domain" end in tac. @@ -48,8 +49,6 @@ 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 index 7ffe1e4ed0..4d9cf22dd5 100644 --- a/plugins/micromega/Lra.v +++ b/plugins/micromega/Lra.v @@ -20,20 +20,21 @@ 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 ; - (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)))). +Ltac lra := unfold Rdiv in * ; lra_R ; rchecker. (** Here, nra stands for non-linear real arithmetic *) -Ltac nra := - xnra ; - (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)))). +Ltac nra := unfold Rdiv in * ; xnra ; rchecker. Ltac xpsatz dom d := let tac := lazymatch dom with @@ -41,9 +42,7 @@ Ltac xpsatz dom d := (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))) + try rchecker | _ => fail "Unsupported domain" end in tac. diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index b1f242f58a..c81c025a55 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -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,41 +53,18 @@ Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:(-1). Ltac psatzl dom := let tac := lazymatch dom with - | Z => lia - | Q => - lra_Q ; - (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 * ; - lra_R ; - (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)))) -| _ => fail "Unsupported domain" + | Z => Lia.lia + | Q => Lqa.lra + | R => Lra.lra + | _ => fail "Unsupported domain" end in tac. Ltac lra := first [ psatzl R | psatzl Q ]. -Ltac nra_R := - 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). - -Ltac nra_Q := - xnqa ; - (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))). - Ltac nra := - first [ nra_R | nra_Q ]. + first [ Lra.nra | Lqa.nra ]. (* Local Variables: *) -- cgit v1.2.3 From 1ae74bfd16f00bea0de14299cace8b638f768a70 Mon Sep 17 00:00:00 2001 From: Frédéric Besson Date: Thu, 1 Sep 2016 16:21:11 +0200 Subject: Fixed Bug #5003 : more careful generalisation of dependent terms. --- plugins/micromega/coq_micromega.ml | 35 ++++++++++++++++++++++++++++++++--- 1 file changed, 32 insertions(+), 3 deletions(-) (limited to 'plugins') diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index edcb00b90b..42ea8c4592 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 } -- cgit v1.2.3