A generic preprocessing tactic zify for (r)omega

------------------------------------------------ 

See file PreOmega for more details and/or test-suite/succes/*Omega*.v

The zify tactic performs a Z-ification of your current goal,
transforming parts of type nat, N, positive, taking advantage of many
equivalences of operations, and of the positivity implied by these
types.

Integration with omega and romega:
 (r)omega : the earlier tactics, 100% compatible 
 (r)omega with * : full zify applied before the (r)omega run
 (r)omega with <types>, where <types> is a sub-list of {nat,N,positive,Z}, 
   applies only specific parts of zify (btw "with Z" means take advantage 
   of Zmax, Zmin, Zabs and Zsgn). 

As a particular consequence, "romega with nat" should now be a
close-to-perfect replacement for omega. Slightly more powerful, since
(forall x:nat, x*x>=0) is provable and also slightly less powerful: if
False is somewhere in the hypothesis, it doesn't use it. 

For the moment zify is done in a direct way in Ltac, using rewrite
when necessary, but crucial chains of rewrite may be made reflexive
some day.

Even though zify is designed to help (r)omega, I think it might be 
of interest for other tactics (micromega ?). Feel free to complete
zify if your favorite operation / type isn't handled yet. 


Side-effects: 

- additional results for ZArith, NArith, etc...
- definition of Ple, Plt, Pgt, Pge and notations for them in positive_scope
- romega now start by doing "intros". Since the conclusion will be negated, 
  and this operation will be justified by means of decidability, it helps
  to have as little as possible in the conclusion. 






git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10028 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 137 insertions, 0 deletions

diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index e19989aed..76a3d616c 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -16,7 +16,11 @@ Require Import Min.
 Require Import Max.
 Require Import BinPos.
 Require Import BinNat.
+Require Import BinInt.
 Require Import Pnat.
+Require Import Zmax.
+Require Import Zmin.
+Require Import Znat.
 
 (** Translation from [N] to [nat] and back. *)
 
@@ -238,3 +242,136 @@ Proof.
   rewrite <- nat_of_Nmax.
   apply N_of_nat_of_N.
 Qed.
+
+(** Properties concerning Z_of_N *)
+
+Lemma Z_of_nat_of_N : forall n:N, Z_of_nat (nat_of_N n) = Z_of_N n.
+Proof.
+  destruct n; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
+Qed.
+
+Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m.
+Proof.
+ intros; f_equal; assumption.
+Qed.
+
+Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m.
+Proof.
+ intros [|n] [|m]; simpl; intros; try discriminate; congruence.
+Qed.
+
+Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m.
+Proof.
+ split; [apply Z_of_N_eq | apply Z_of_N_eq_rev].
+Qed.
+
+Lemma Z_of_N_le : forall n m, (n<=m)%N -> (Z_of_N n <= Z_of_N m)%Z.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_le_rev : forall n m, (Z_of_N n <= Z_of_N m)%Z -> (n<=m)%N.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> (Z_of_N n <= Z_of_N m)%Z.
+Proof.
+ split; [apply Z_of_N_le | apply Z_of_N_le_rev].
+Qed.
+
+Lemma Z_of_N_lt : forall n m, (n<m)%N -> (Z_of_N n < Z_of_N m)%Z.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_lt_rev : forall n m, (Z_of_N n < Z_of_N m)%Z -> (n<m)%N.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> (Z_of_N n < Z_of_N m)%Z.
+Proof.
+ split; [apply Z_of_N_lt | apply Z_of_N_lt_rev].
+Qed.
+
+Lemma Z_of_N_ge : forall n m, (n>=m)%N -> (Z_of_N n >= Z_of_N m)%Z.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_ge_rev : forall n m, (Z_of_N n >= Z_of_N m)%Z -> (n>=m)%N.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> (Z_of_N n >= Z_of_N m)%Z.
+Proof.
+ split; [apply Z_of_N_ge | apply Z_of_N_ge_rev].
+Qed.
+
+Lemma Z_of_N_gt : forall n m, (n>m)%N -> (Z_of_N n > Z_of_N m)%Z.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_gt_rev : forall n m, (Z_of_N n > Z_of_N m)%Z -> (n>m)%N.
+Proof.
+ intros [|n] [|m]; simpl; auto.
+Qed.
+
+Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> (Z_of_N n > Z_of_N m)%Z.
+Proof.
+ split; [apply Z_of_N_gt | apply Z_of_N_gt_rev].
+Qed.
+
+Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n.
+Proof.
+ destruct n; simpl; auto.
+Qed. 
+
+Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p.
+Proof.
+ destruct p; simpl; auto.
+Qed. 
+
+Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z.
+Proof.
+ destruct z; simpl; auto.
+Qed. 
+
+Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z.
+Proof.
+ destruct n; intro; discriminate.
+Qed.
+
+Lemma Z_of_N_plus : forall n m:N, Z_of_N (n+m) = (Z_of_N n + Z_of_N m)%Z.
+Proof.
+intros; repeat rewrite <- Z_of_nat_of_N; rewrite nat_of_Nplus; apply inj_plus.
+Qed.
+
+Lemma Z_of_N_mult : forall n m:N, Z_of_N (n*m) = (Z_of_N n * Z_of_N m)%Z.
+Proof.
+intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmult; apply inj_mult.
+Qed.
+
+Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m). 
+Proof.
+intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus.
+Qed.
+
+Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n). 
+Proof.
+intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S.
+Qed.
+
+Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m). 
+Proof.
+intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min.
+Qed.
+
+Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m). 
+Proof.
+intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max.
+Qed.
+