diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2014-08-01 15:23:24 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2014-08-01 15:23:24 +0200 |
| commit | bbf3682aa80bb86502e29018465e3602f0d9bb3e (patch) | |
| tree | 030cea0b019df4903664fe77d96297c40381762a /plugins/micromega/Psatz.v | |
| parent | 7e67bba64e1b59be2acf5997157bff10581d28f2 (diff) | |
micromega : improve efficiency/termination of type-checking
* unused terms are generalised
* proof is abstract
Diffstat (limited to 'plugins/micromega/Psatz.v')
| -rw-r--r-- | plugins/micromega/Psatz.v | 13 |
1 files changed, 9 insertions, 4 deletions
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 := |