Library Coq.micromega.Lra
Here, lra stands for linear real arithmetic
Ltac lra :=
unfold Rdiv in * ;
lra_R rchecker.
Here, nra stands for non-linear real arithmetic
Ltac nra :=
unfold Rdiv in * ;
xnra rchecker.
Ltac xpsatz dom d :=
let tac :=
lazymatch dom with
|
R =>
(
sos_R rchecker) || (
psatz_R d rchecker)
|
_ =>
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).