diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2016-08-31 19:12:15 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2016-08-31 19:12:15 +0200 |
| commit | 7d4b8108bc8fa6951e605cb9b42580ff6f8e583f (patch) | |
| tree | 38851b455ef429d861f46ef7fc4639233254bd1a /plugins/micromega/Lia.v | |
| parent | 985e83e60b6665d17b81830aea4fce3384fe2b5a (diff) | |
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.
Diffstat (limited to 'plugins/micromega/Lia.v')
| -rw-r--r-- | plugins/micromega/Lia.v | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/plugins/micromega/Lia.v b/plugins/micromega/Lia.v index 52bf5ed3d..6974f8d99 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: *) |