diff options
| author |  Frédéric Besson <frederic.besson@inria.fr> | 2014-07-31 19:18:15 +0200 |
|---|---|---|
| committer | Frédéric Besson <frederic.besson@inria.fr> | 2014-07-31 19:18:15 +0200 |
| commit | 5b4aa0c12c605aa28af81ac8183c6c27ef1af8e9 (patch) | |
| tree | 0eb2859ad7f80ed5518a52e10815a02493a4e7c2 /plugins/micromega/Psatz.v | |
| parent | cfadaae9e459af6a441e7c744970657bb1601ba0 (diff) | |
micromega : refification recognises @eq T for T convertible with Z or R
Diffstat (limited to 'plugins/micromega/Psatz.v')
| -rw-r--r-- | plugins/micromega/Psatz.v | 34 |
1 files changed, 16 insertions, 18 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index 804a16b79..69b0046b9 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -23,6 +23,21 @@ Require Import VarMap. Require Tauto. Declare ML Module "micromega_plugin". +Ltac lia := + zify ; unfold Z.succ in * ; + (*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. + +Ltac nia := + zify ; unfold Z.succ in * ; + xnlia ; + intros __wit __varmap __ff ; + change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; + apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. + + Ltac xpsatz dom d := let tac := lazymatch dom with | Z => @@ -52,11 +67,7 @@ Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1. Ltac psatzl dom := let tac := lazymatch dom with - | Z => - psatzl_Z ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity + | Z => lia | Q => psatzl_Q ; (* If csdp is not installed, the previous step might not produce any @@ -79,19 +90,6 @@ Ltac psatzl dom := Ltac lra := first [ psatzl R | psatzl Q ]. -Ltac lia := - zify ; unfold Z.succ in * ; - (*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. - -Ltac nia := - zify ; unfold Z.succ in * ; - xnlia ; - intros __wit __varmap __ff ; - change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; - apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity. (* Local Variables: *) |