Library Coq.micromega.Lia

Require Import ZMicromega.
Require Import ZArith.
Require Import RingMicromega.
Require Import VarMap.
Require Coq.micromega.Tauto.

Ltac preprocess :=
  zify ; unfold Z.succ in * ; unfold Z.pred in *.

Ltac zchange :=
  intros __wit __varmap __ff ;
  change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ;
  apply (ZTautoChecker_sound __ff __wit).

Ltac zchecker_no_abstract := zchange ; vm_compute ; reflexivity.

Ltac zchecker_abstract := zchange ; vm_cast_no_check (eq_refl true).

Ltac zchecker := zchecker_no_abstract.

Ltac lia := preprocess; xlia zchecker.

Ltac nia := preprocess; xnlia zchecker.