diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /plugins/micromega/Psatz.v | |
parent | 300293c119981054c95182a90c829058530a6b6f (diff) |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'plugins/micromega/Psatz.v')
-rw-r--r-- | plugins/micromega/Psatz.v | 20 |
1 files changed, 17 insertions, 3 deletions
diff --git a/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v index fde0f29a..7f6cf79b 100644 --- a/plugins/micromega/Psatz.v +++ b/plugins/micromega/Psatz.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -18,7 +18,7 @@ Require Import RMicromega. Require Import QArith. Require Export Ring_normalize. Require Import ZArith. -Require Import Raxioms. +Require Import Rdefinitions. Require Export RingMicromega. Require Import VarMap. Require Tauto. @@ -66,6 +66,7 @@ Ltac psatzl dom := change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity) | 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'. *) @@ -75,12 +76,25 @@ Ltac psatzl dom := | _ => fail "Unsupported domain" end in tac. + +Ltac lra := + first [ psatzl R | psatzl Q ]. + Ltac lia := - xlia ; + zify ; unfold Zsucc in * ; + (*cbv delta - [Zplus Zminus Zopp Zmult Zpower Zgt Zge Zle Zlt 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 Zsucc 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: *) (* coding: utf-8 *) (* End: *) |