NB: This Coq documentation contains a revised version of the Coq implementation of these papers [1], [2], [3], [4], and is also the support for ongoing research. A partial archive (14/01/2001) is available at here. Drop us a line if you are interested in a complete, up-to-date archive.

Library omegaz

Require Import ZArith.
Require Import ZArith_ext.

OmegaZ : extension of omega to handle goals/hypos that contains Z_of_nat

Lemma Z0_mech: Z0 = Z_of_nat 0.

Lemma Z_of_nat_inj': forall x y, x = y -> Z_of_nat x = Z_of_nat y.

Lemma nat_of_Z: forall z, (z >= 0)%Z -> exists n, z = Z_of_nat n.

Ltac mult_dist :=
  (rewrite mult_plus_distr_l; (mult_dist || idtac)) ||
  (rewrite mult_plus_distr_r; (mult_dist || idtac)) ||
  (rewrite mult_minus_distr_r; [(mult_dist || idtac) | OmegaZ]) ||
  (rewrite mult_minus_distr_l; [(mult_dist || idtac) | OmegaZ]) ||
  idtac
with
  Z_to_nat x:=
  assert (Z_to_natA1 : Zpos x = Z_of_nat (nat_of_P x));
    [auto | rewrite Z_to_natA1; clear Z_to_natA1; unfold nat_of_P; simpl (Pmult_nat x 1); idtac]
with
  Supr_Z t :=
  match t with
    | Z0 => rewrite Z0_mech
    | Zpos ?x => Z_to_nat x
    | Zplus ?x1 ?x2 =>
      ((Supr_Z x1 || idtac); (Supr_Z x2 || idtac); rewrite <- inj_plus) ||
      idtac
    | Zminus ?x1 ?x2 =>
      ((Supr_Z x1 || idtac); (Supr_Z x2 || idtac); rewrite <- inj_minus1; [idtac | omega]) ||
      idtac
    | Zmult ?x1 ?x2 =>
      ((Supr_Z x1 || idtac); (Supr_Z x2 || idtac); rewrite <- inj_mult) ||
      idtac
    | Z_of_nat ?x => idtac
    | ?E =>
      assert (Supr_Z'A1: (E >= 0)%Z);
        [omega |
         generalize (nat_of_Z _ Supr_Z'A1); clear Supr_Z'A1; intro X;
         let x := fresh in (let y := fresh in (destruct X as [x y]; rewrite y))] ||
      idtac
    | _ => idtac
  end
with
  Supr_Z_eq_left :=
  match goal with
    | |- (?x1 = ?x2)%Z => Supr_Z x1
    | |- (?x1 <= ?x2)%Z => Supr_Z x1
    | |- (?x1 >= ?x2)%Z => Supr_Z x1
    | |- (?x1 > ?x2)%Z => Supr_Z x1
    | |- (?x1 < ?x2)%Z => Supr_Z x1
    | |- _ => idtac
  end
with
  Supr_Z_eq_right :=
  match goal with
    | |- (?x1 = ?x2)%Z => Supr_Z x2
    | |- (?x1 <= ?x2)%Z => Supr_Z x2
    | |- (?x1 >= ?x2)%Z => Supr_Z x2
    | |- (?x1 > ?x2)%Z => Supr_Z x2
    | |- (?x1 < ?x2)%Z => Supr_Z x2
    | |- _ => idtac
  end
with
  Supr_Z_eq :=
  match goal with
    | |- (Z_of_nat ?x1 = Z_of_nat ?x2)%Z => apply Z_of_nat_inj'
    | |- (Z_of_nat ?x1 <= Z_of_nat ?x2)%Z => apply inj_le
    | |- (Z_of_nat ?x1 < Z_of_nat ?x2)%Z => apply inj_lt
    | |- (Z_of_nat ?x1 >= Z_of_nat ?x2)%Z => apply inj_ge
    | |- (Z_of_nat ?x1 < Z_of_nat ?x2)%Z => apply inj_gt
    | |- _ => idtac
  end
with
  Z_to_nat_Hyp x id:=
  assert (Z_to_natA1 : Zpos x = Z_of_nat (nat_of_P x));
    [auto |
     rewrite Z_to_natA1 in id; clear Z_to_natA1; unfold nat_of_P in id; simpl (Pmult_nat x 1) in id; idtac ]
with
  Supr_Z_Hyp t id:=
  match t with
    | Z0 => rewrite Z0_mech in id
    | Zpos ?x => Z_to_nat_Hyp x id
    | Zplus ?x1 ?x2 => (Supr_Z_Hyp x1 id || idtac) ; (Supr_Z_Hyp x2 id || idtac); rewrite <- inj_plus in id
    | Zminus ?x1 ?x2 => (Supr_Z_Hyp x1 id || idtac) ; (Supr_Z_Hyp x2 id || idtac); rewrite <- inj_minus1 in id; [idtac | omega]
    | Zmult ?x1 ?x2 => (Supr_Z_Hyp x1 id || idtac) ; (Supr_Z_Hyp x2 id || idtac); rewrite <- inj_mult in id
    | Z_of_nat ?x => idtac
    | ?E =>
      assert (Supr_Z'A1: (E >= 0)%Z);
        [omega |
         generalize (nat_of_Z _ Supr_Z'A1); clear Supr_Z'A1; intro X;
         let x := fresh in (let y := fresh in (destruct X as [x y]; rewrite y in id))] ||
      idtac
    | _ => idtac
  end
  
with
  Supr_Z_eq_hyp_left :=
  match goal with
    | id: (?x1 = ?x2)%Z |- _ => Supr_Z_Hyp x1 id
    | id: (?x1 <= ?x2)%Z |- _ => Supr_Z_Hyp x1 id
    | id: (?x1 >= ?x2)%Z |- _ => Supr_Z_Hyp x1 id
    | id: (?x1 > ?x2)%Z |- _ => Supr_Z_Hyp x1 id
    | id: (?x1 < ?x2)%Z |- _ => Supr_Z_Hyp x1 id
    | |- _ => idtac
  end
with
  Supr_Z_eq_hyp_right :=
  match goal with
    | id: (?x1 = ?x2)%Z |- _ => Supr_Z_Hyp x2 id
    | id: (?x1 <= ?x2)%Z |- _ => Supr_Z_Hyp x2 id
    | id: (?x1 >= ?x2)%Z |- _ => Supr_Z_Hyp x2 id
    | id: (?x1 > ?x2)%Z |- _ => Supr_Z_Hyp x2 id
    | id: (?x1 < ?x2)%Z |- _ => Supr_Z_Hyp x2 id
    | |- _ => idtac
  end
with Supr_Z_eq_Hyp :=
  match goal with
    | id: (?x1 = ?x2)%Z |- _ => generalize (Z_of_nat_inj _ _ id); intros
    | id: (?x1 > ?x2)%Z |- _ => generalize (Z_of_nat_gt_inj _ _ id); intros
    | id: (?x1 < ?x2)%Z |- _ => generalize (Z_of_nat_lt_inj _ _ id); intros
    | id: (?x1 >= ?x2)%Z |- _ => generalize (Z_of_nat_ge_inj _ _ id); intros
    | id: (?x1 <= ?x2)%Z |- _ => generalize (Z_of_nat_le_inj _ _ id); intros
    | |- _ => idtac
  end
with
  OmegaZ :=
  ((Supr_Z_eq_hyp_left; Supr_Z_eq_hyp_right; Supr_Z_eq_Hyp); (Supr_Z_eq_left; Supr_Z_eq_right; Supr_Z_eq) || idtac);
  mult_dist; (omega || tauto).

Lemma test: forall x y,
  ((Z_of_nat x) + 4%Z - 2%Z > (Z_of_nat (y +4)))%Z ->
  ((Z_of_nat (x + 2)) + 2%Z >= (Z_of_nat y) + 6%Z)%Z.

Ltac omegaz_inj_plus_hyp :=
  match goal with
    | id : context [Z_of_nat (plus _ _)] |- _ => rewrite inj_plus in id

  end.

Ltac omegaz_inj_plus :=
  match goal with
    | |- context [Z_of_nat (plus _ _)] => rewrite inj_plus

  end.

Ltac omegaz_inj_minus_hyp :=
  match goal with
    | id : context [Z_of_nat (minus _ _)] |- _ => rewrite inj_minus1 in id

  end.

Ltac omegaz_inj_minus :=
  match goal with
    | |- context [Z_of_nat (minus _ _)] => rewrite inj_minus1

  end.

Ltac omegaz_inj_mult_hyp :=
  match goal with
    | id : context [Z_of_nat (mult _ _)] |- _ => rewrite inj_mult in id

  end.

Ltac omegaz_inj_mult :=
  match goal with
    | |- context [Z_of_nat (mult _ _)] => rewrite inj_mult

  end.

Ltac simpl_Z_of_nat_cst_hyp :=
  match goal with
    | id : context [Z_of_nat O] |- _ => simpl (Z_of_nat O) in id
    | id : context [Z_of_nat (S ?x)] |- _ => simpl (Z_of_nat (S x)) in id
  end.

Require Import ssreflect ssrbool.

Ltac simpl_Z_of_nat_cst :=
  match goal with
    | |- context [Z_of_nat O] => simpl (Z_of_nat O)
    | |- context [Z_of_nat 1] => rewrite [Z_of_nat 1]/=
    | |- context [Z_of_nat 2] => rewrite [Z_of_nat 2]/=
    | |- context [Z_of_nat 3] => rewrite [Z_of_nat 3]/=
    | |- context [Z_of_nat 4] => rewrite [Z_of_nat 4]/=
    | |- context [Z_of_nat (S ?x)] => rewrite (Z_S x)
  end.

Ltac Zabs_nat_tac_hyp :=
  match goal with
    | id : context [Zabs_nat (Z_of_nat ?n)] |- _ => rewrite (Zabs_nat_Z_of_nat n) in id
    | id : context [Zabs_nat 1%Z] |- _ => rewrite (_ : Zabs_nat 1%Z = 1%nat) in id; last by done
  end.

Ltac Zabs_nat_tac :=
  match goal with
    | |- context [Zabs_nat (Z_of_nat ?n)] => rewrite (Zabs_nat_Z_of_nat n)
    | |- context [Zabs_nat 1%Z] => rewrite (_ : Zabs_nat 1%Z = 1%nat); last by done
  end.

Ltac omegaz_hyp :=
  repeat omegaz_inj_plus_hyp ;
  repeat omegaz_inj_minus_hyp ;
  repeat omegaz_inj_mult_hyp ;
  repeat simpl_Z_of_nat_cst_hyp.

Ltac omegaz_goal :=
  repeat omegaz_inj_plus ;
  repeat omegaz_inj_minus ;
  repeat omegaz_inj_mult ;
  repeat simpl_Z_of_nat_cst.

Ltac omegaz :=
  repeat omegaz_hyp ;
  repeat omegaz_goal ;
  omega.