Library Coq.micromega.Lia

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

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

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

Ltac zchecker_no_abstract checker :=
  zchange checker ; vm_compute ; reflexivity.

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

Ltac zchecker := zchecker_no_abstract ZTautoChecker_sound.

Ltac zchecker_ext := zchecker_no_abstract ZTautoCheckerExt_sound.

Ltac lia := preprocess; xlia zchecker_ext.

Ltac nia := preprocess; xnlia zchecker.