Library Coq.micromega.Psatz

Require Import ZMicromega.
Require Import QMicromega.
Require Import RMicromega.
Require Import QArith.
Require Import ZArith.
Require Import Rdefinitions.
Require Import RingMicromega.
Require Import VarMap.
Require Coq.micromega.Tauto.
Require Lia.
Require Lra.
Require Lqa.


Ltac lia := Lia.lia.

Ltac nia := Lia.nia.

Ltac xpsatz dom d :=
  let tac := lazymatch dom with
  | Z =>
    (sos_Z Lia.zchecker) || (psatz_Z d Lia.zchecker)
  | R =>
    (sos_R Lra.rchecker) || (psatz_R d Lra.rchecker)
  | Q => (sos_Q Lqa.rchecker) || (psatz_Q d Lqa.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).

Ltac psatzl dom :=
  let tac := lazymatch dom with
  | Z => Lia.lia
  | Q => Lqa.lra
  | R => Lra.lra
  | _ => fail "Unsupported domain"
  end in tac.

Ltac lra :=
  first [ psatzl R | psatzl Q ].

Ltac nra :=
  first [ Lra.nra | Lqa.nra ].