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

12 files changed, 493 insertions, 76 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index cc2d04e58..6e4c4b26f 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -416,7 +416,7 @@ Ltac bal_tac :=
 
 Ltac bal_tac_imp := match goal with 
   | |- context [ assert_false ] => 
-      inv avl; avl_nns; simpl in *; false_omega
+      inv avl; avl_nns; simpl in *; omega_max
   | _ => idtac
 end.
 
@@ -703,7 +703,7 @@ Proof.
  rewrite e3; simpl;destruct 1.
  split.
  apply bal_avl; auto.
- simpl; omega_max.
+ omega_max.
  omega_bal.
 Qed.
 
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index 23d42fda8..fa10809cc 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -461,7 +461,7 @@ Lemma bal_in : forall l x r y, avl l -> avl r ->
 Proof.
  bal_tac; 
  solve [repeat rewrite create_in; intuition_in
-       |inv avl; avl_nns; simpl in *; false_omega].
+       |inv avl; avl_nns; simpl in *; omega_max].
 Qed.
 
 Ltac omega_bal := match goal with 
@@ -1856,7 +1856,7 @@ Qed.
 Lemma height_0 : forall s, avl s -> height s = 0 -> s = Leaf.
 Proof.
  destruct 1; intuition; simpl in *.
- avl_nns; simpl in *; false_omega_max.
+ avl_nns; simpl in *; elimtype False; omega_max.
 Qed.   
 
 (** * Union
diff --git a/theories/Ints/Z/IntsZmisc.v b/theories/Ints/Z/IntsZmisc.v
index 6fcaaa6e9..e4dee2d4f 100644
--- a/theories/Ints/Z/IntsZmisc.v
+++ b/theories/Ints/Z/IntsZmisc.v
@@ -100,7 +100,7 @@ Definition is_lt (n m : positive) :=
   end.
 Infix "?<" := is_lt (at level 70, no associativity) : P_scope.
 
-Lemma is_lt_spec : forall n m, if n ?< m then n < m else m <= n. 
+Lemma is_lt_spec : forall n m, if n ?< m then (n < m)%Z else (m <= n)%Z. 
 Proof.
  intros n m; unfold is_lt, Zlt, Zle, Zcompare.
  rewrite (ZC4 m n);destruct ((n ?= m) Eq);trivial;try (intro;discriminate).
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v
index 2e3c6a3a5..28c6fdb6d 100644
--- a/theories/NArith/BinPos.v
+++ b/theories/NArith/BinPos.v
@@ -220,6 +220,22 @@ Fixpoint Pcompare (x y:positive) (r:comparison) {struct y} : comparison :=
 
 Infix "?=" := Pcompare (at level 70, no associativity) : positive_scope.
 
+Definition Plt (x y:positive) := (Pcompare x y Eq) = Lt.
+Definition Pgt (x y:positive) := (Pcompare x y Eq) = Gt.
+Definition Ple (x y:positive) := (Pcompare x y Eq) <> Gt.
+Definition Pge (x y:positive) := (Pcompare x y Eq) <> Lt.
+
+Infix "<=" := Ple : positive_scope.
+Infix "<" := Plt : positive_scope.
+Infix ">=" := Pge : positive_scope.
+Infix ">" := Pgt : positive_scope.
+
+Notation "x <= y <= z" := (x <= y /\ y <= z) : positive_scope.
+Notation "x <= y < z" := (x <= y /\ y < z) : positive_scope.
+Notation "x < y < z" := (x < y /\ y < z) : positive_scope.
+Notation "x < y <= z" := (x < y /\ y <= z) : positive_scope.
+
+
 Definition Pmin (p p' : positive) := match Pcompare p p' Eq with 
  | Lt | Eq => p 
  | Gt => p'
@@ -959,6 +975,11 @@ Qed.
 (**********************************************************************)
 (** Properties of subtraction on binary positive numbers *)
 
+Lemma Ppred_minus : forall p, Ppred p = Pminus p xH.
+Proof.
+  destruct p; compute; auto.
+Qed.
+
 Lemma double_eq_zero_inversion :
   forall p:positive_mask, Pdouble_mask p = IsNul -> p = IsNul.
 Proof.
@@ -991,6 +1012,33 @@ Proof.
       | auto ].
 Qed.
 
+Lemma Pminus_mask_carry_diag : forall p, Pminus_mask_carry p p = IsNeg.
+Proof.
+  induction p; simpl; auto; rewrite IHp; auto.
+Qed.
+
+Lemma Pminus_mask_IsNeg : forall p q:positive, 
+ Pminus_mask p q = IsNeg -> Pminus_mask_carry p q = IsNeg.
+Proof.
+  induction p; destruct q; simpl; intros; auto; try discriminate.
+
+  unfold Pdouble_mask in H.
+  generalize (IHp q).
+  destruct (Pminus_mask p q); try discriminate.
+  intro H'; rewrite H'; auto.
+
+  unfold Pdouble_plus_one_mask in H.
+  destruct (Pminus_mask p q); simpl; auto; try discriminate.
+
+  unfold Pdouble_plus_one_mask in H.
+  destruct (Pminus_mask_carry p q); simpl; auto; try discriminate.
+
+  unfold Pdouble_mask in H.
+  generalize (IHp q).
+  destruct (Pminus_mask p q); try discriminate.
+  intro H'; rewrite H'; auto.
+Qed.
+
 Lemma ZL10 :
   forall p q:positive,
     Pminus_mask p q = IsPos xH -> Pminus_mask_carry p q = IsNul.
@@ -1099,3 +1147,26 @@ Proof.
     intros H2 H3; elim H3; intros H4 H5; unfold Pminus in |- *; 
       rewrite H2; exact H4.
 Qed.
+
+(* When x<y, the substraction of x by y returns 1 *)
+
+Lemma Pminus_mask_Lt : forall p q:positive, p<q -> Pminus_mask p q = IsNeg.
+Proof.
+  unfold Plt; induction p; destruct q; simpl; intros; auto; try discriminate.
+  rewrite IHp; simpl; auto.
+  rewrite IHp; simpl; auto.
+  apply Pcompare_Gt_Lt; auto.
+  destruct (Pcompare_Lt_Lt _ _ H).
+  rewrite Pminus_mask_IsNeg; simpl; auto.
+  subst q; rewrite Pminus_mask_carry_diag; auto.
+  rewrite IHp; simpl; auto.
+Qed. 
+
+Lemma Pminus_Lt : forall p q:positive, p<q -> p-q = xH.
+Proof.
+  intros; unfold Plt, Pminus; rewrite Pminus_mask_Lt; auto.
+Qed.
+
+
+
+
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.
+
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index d5cd17a0c..5bc81f955 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -9,7 +9,7 @@
 (*i $Id$ i*)
 
 (***********************************************************)
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 (***********************************************************)
 
 Require Export BinPos.
@@ -967,6 +967,21 @@ Qed.
 (**********************************************************************)
 (** * Relating binary positive numbers and binary integers *)
 
+Lemma Zpos_eq : forall p q, p = q -> Zpos p = Zpos q.
+Proof.
+  intros; f_equal; auto.
+Qed.
+
+Lemma Zpos_eq_rev : forall p q, Zpos p = Zpos q -> p = q.
+Proof.
+  inversion 1; auto.
+Qed.
+
+Lemma Zpos_eq_iff : forall p q, p = q <-> Zpos p = Zpos q.
+Proof.
+  split; [apply Zpos_eq|apply Zpos_eq_rev].
+Qed.
+
 Lemma Zpos_xI : forall p:positive, Zpos (xI p) = Zpos 2 * Zpos p + Zpos 1.
 Proof.
   intro; apply refl_equal.
@@ -1061,3 +1076,4 @@ Definition Z_of_N (x:N) := match x with
                              | N0 => Z0
                              | Npos p => Zpos p
                            end.
+
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index 4c9470b36..562000d8f 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -7,8 +7,8 @@
 (***********************************************************************)
 
 (* Finite sets library.  
- * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
- * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
+ * Authors: Pierre Letouzey and Jean-Christophe Filliâtre 
+ * Institution: LRI, CNRS UMR 8623 - Université Paris Sud
  *              91405 Orsay, France *)
 
 (* $Id$ *)
@@ -352,46 +352,15 @@ Module MoreInt (I:Int).
   Ltac i2z_refl := 
     i2z_gen;
     match goal with |- ?t => 
-      let e := p2ep t 
-	in 
-	(change (ep2p e); 
-	  apply norm_ep_correct2; 
-	    simpl)
+      let e := p2ep t in 
+      change (ep2p e); apply norm_ep_correct2; simpl
     end.
 
-  Ltac iauto := i2z_refl; auto.
-  Ltac iomega := i2z_refl; intros; romega.
-
-  Open Scope Z_scope.
-
-  Lemma max_spec : forall (x y:Z), 
-    x >= y /\ Zmax x y = x  \/
-    x < y /\ Zmax x y = y.
-  Proof.
-    intros; unfold Zmax, Zlt, Zge.
-    destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
-  Qed.
-
-  Ltac omega_max_genspec x y := 
-    generalize (max_spec x y); 
-    (let z := fresh "z" in let Hz := fresh "Hz" in 
-     set (z:=Zmax x y); clearbody z).
-
-  Ltac omega_max_loop := 
-    match goal with 
-      (* hack: we don't want [i2z (height ...)] to be reduced by romega later... *)
-      | |- context [ i2z (?f ?x) ] => 
-          let i := fresh "i2z" in (set (i:=i2z (f x)); clearbody i); omega_max_loop
-      | |- context [ Zmax ?x ?y ] => omega_max_genspec x y; omega_max_loop
-      | _ => intros
-    end.
-
-  Ltac omega_max := i2z_refl; omega_max_loop; try romega.
+  (* i2z_refl can be replaced below by (simpl in *; i2z). 
+     The reflexive version improves compilation of AVL files by about 15%  *)
   
-  Ltac false_omega := i2z_refl; intros; romega.
-  Ltac false_omega_max := elimtype False; omega_max.
+  Ltac omega_max := i2z_refl; romega with Z.
 
-  Open Scope Int_scope.
 End MoreInt.
 
 
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index c7f0bb723..e43d68bfa 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
 
 Require Import Arith_base.
 Require Import BinPos.
@@ -70,6 +70,13 @@ Proof.
       (intros H2; rewrite H2); auto.
 Qed.
 
+Lemma Zabs_spec : forall x:Z, 
+  0 <= x /\ Zabs x = x \/ 
+  0 > x /\ Zabs x = -x. 
+Proof.
+ intros; unfold Zabs, Zle, Zgt; destruct x; simpl; intuition discriminate.
+Qed.
+
 (** * Triangular inequality *)
 
 Hint Local Resolve Zle_neg_pos: zarith.
@@ -89,6 +96,16 @@ Proof.
   apply Zplus_le_compat; simpl in |- *; auto with zarith.
 Qed.
 
+(** * A characterization of the sign function: *)
+
+Lemma Zsgn_spec : forall x:Z, 
+  0 < x /\ Zsgn x = 1 \/ 
+  0 = x /\ Zsgn x = 0 \/ 
+  0 > x /\ Zsgn x = -1.
+Proof. 
+ intros; unfold Zsgn, Zle, Zgt; destruct x; compute; intuition.
+Qed.
+
 (** * Absolute value and multiplication *)
 
 Lemma Zsgn_Zabs : forall n:Z, n * Zsgn n = Zabs n.
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index b7121fa19..33f50fc9b 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -10,7 +10,7 @@
 
 Require Import ZArithRing.
 Require Import ZArith_base.
-Require Import Omega.
+Require Export Omega.
 Require Import Wf_nat.
 Open Local Scope Z_scope.
 
diff --git a/theories/ZArith/Zmax.v b/theories/ZArith/Zmax.v
index b2c068564..fbc7bfafc 100644
--- a/theories/ZArith/Zmax.v
+++ b/theories/ZArith/Zmax.v
@@ -38,6 +38,14 @@ Proof.
   destruct (n ?= m); (apply H1|| apply H2); discriminate. 
 Qed.
 
+Lemma Zmax_spec : forall x y:Z, 
+  x >= y /\ Zmax x y = x  \/
+  x < y /\ Zmax x y = y.
+Proof.
+ intros; unfold Zmax, Zlt, Zge.
+ destruct (Zcompare x y); [ left | right | left ]; split; auto; discriminate.
+Qed.
+
 (** * Least upper bound properties of max *)
 
 Lemma Zle_max_l : forall n m:Z, n <= Zmax n m.
@@ -106,3 +114,39 @@ Proof.
     rewrite (Zcompare_plus_compat x y n).
   case (x ?= y); apply Zplus_comm.
 Qed.
+
+(** * Maximum and Zpos *)
+
+Lemma Zpos_max : forall p q, Zpos (Pmax p q) = Zmax (Zpos p) (Zpos q).
+Proof.
+  intros; unfold Zmax, Pmax; simpl; generalize (Pcompare_Eq_eq p q).
+  destruct Pcompare; auto.
+  intro H; rewrite H; auto.
+Qed.
+
+Lemma Zpos_max_1 : forall p, Zmax 1 (Zpos p) = Zpos p.
+Proof.
+  intros; unfold Zmax; simpl; destruct p; simpl; auto.
+Qed.
+
+(** * Characterization of Pminus in term of Zminus and Zmax *)
+
+Lemma Zpos_minus : forall p q, Zpos (Pminus p q) = Zmax 1 (Zpos p - Zpos q).
+Proof.
+  intros.
+  case_eq (Pcompare p q Eq).
+  intros H; rewrite (Pcompare_Eq_eq _ _ H).
+  rewrite Zminus_diag.
+  unfold Zmax; simpl.
+  unfold Pminus; rewrite Pminus_mask_diag; auto.
+  intros; rewrite Pminus_Lt; auto.
+  destruct (Zmax_spec 1 (Zpos p - Zpos q)) as [(H1,H2)|(H1,H2)]; auto.
+  elimtype False; clear H2.
+  assert (H1':=Zlt_trans 0 1 _ Zlt_0_1 H1).
+  generalize (Zlt_0_minus_lt _ _ H1').
+  unfold Zlt; simpl.
+  rewrite (ZC2 _ _ H); intro; discriminate.
+  intros; simpl; rewrite H.
+  symmetry; apply Zpos_max_1.
+Qed.
+
diff --git a/theories/ZArith/Zmin.v b/theories/ZArith/Zmin.v
index 0e0caa1bd..beb91a738 100644
--- a/theories/ZArith/Zmin.v
+++ b/theories/ZArith/Zmin.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 (*i $Id$ i*)
 
-(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
+(** Initial version from Pierre Crégut (CNET, Lannion, France), 1996.
     Further extensions by the Coq development team, with suggestions
     from Russell O'Connor (Radbout U., Nijmegen, The Netherlands).
  *)
@@ -43,6 +43,14 @@ Proof.
   intros n m P H1 H2; unfold Zmin in |- *; case (n ?= m); auto with arith.
 Qed.
 
+Lemma Zmin_spec : forall x y:Z, 
+  x <= y /\ Zmin x y = x  \/
+  x > y /\ Zmin x y = y.
+Proof.
+ intros; unfold Zmin, Zle, Zgt.
+ destruct (Zcompare x y); [ left | left | right ]; split; auto; discriminate.
+Qed.
+
 (** * Greatest lower bound properties of min *)
 
 Lemma Zle_min_l : forall n m:Z, Zmin n m <= n.
@@ -128,3 +136,11 @@ Proof.
 Qed.
 
 Notation Zmin_plus := Zplus_min_distr_r (only parsing).
+
+(** * Minimum and Zpos *)
+
+Lemma Zpos_min : forall p q, Zpos (Pmin p q) = Zmin (Zpos p) (Zpos q).
+Proof.
+  intros; unfold Zmin, Pmin; simpl; destruct Pcompare; auto.
+Qed.
+
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index 27f31bf83..d9fb4e97c 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -8,7 +8,7 @@
 
 (*i $Id$ i*)
 
-(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
 
 Require Export Arith_base.
 Require Import BinPos.
@@ -17,6 +17,7 @@ Require Import Zcompare.
 Require Import Zorder.
 Require Import Decidable.
 Require Import Peano_dec.
+Require Import Min Max Zmin Zmax.
 Require Export Compare_dec.
 
 Open Local Scope Z_scope.
@@ -26,6 +27,8 @@ Definition neq (x y:nat) := x <> y.
 (************************************************)
 (** Properties of the injection from nat into Z *)
 
+(** Injection and successor *)
+
 Theorem inj_S : forall n:nat, Z_of_nat (S n) = Zsucc (Z_of_nat n).
 Proof.
   intro y; induction y as [| n H];
@@ -33,25 +36,12 @@ Proof.
       | change (Zpos (Psucc (P_of_succ_nat n)) = Zsucc (Z_of_nat (S n))) in |- *;
 	rewrite Zpos_succ_morphism; trivial with arith ].
 Qed.
- 
-Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
-Proof.
-  intro x; induction x as [| n H]; intro y; destruct y as [| m];
-    [ simpl in |- *; trivial with arith
-      | simpl in |- *; trivial with arith
-      | simpl in |- *; rewrite <- plus_n_O; trivial with arith
-      | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
-	rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
-	  trivial with arith ].
-Qed.
 
-Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
+(** Injection and equality. *)
+
+Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
 Proof.
-  intro x; induction x as [| n H];
-    [ simpl in |- *; trivial with arith
-      | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
-	rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; 
-	  trivial with arith ].
+  intros x y H; rewrite H; trivial with arith.
 Qed.
 
 Theorem inj_neq : forall n m:nat, neq n m -> Zne (Z_of_nat n) (Z_of_nat m).
@@ -66,6 +56,24 @@ Proof.
 	    intros E; rewrite E; auto with arith ].
 Qed. 
 
+Theorem inj_eq_rev : forall n m:nat, Z_of_nat n = Z_of_nat m -> n = m.
+Proof.
+  intros x y H.
+  destruct (eq_nat_dec x y) as [H'|H']; auto.
+  elimtype False.
+  exact (inj_neq _ _ H' H).
+Qed.
+
+Theorem inj_eq_iff : forall n m:nat, n=m <-> Z_of_nat n = Z_of_nat m.
+Proof.
+ split; [apply inj_eq | apply inj_eq_rev].
+Qed.
+
+
+(** Injection and order relations: *)
+
+(** One way ... *)
+
 Theorem inj_le : forall n m:nat, (n <= m)%nat -> Z_of_nat n <= Z_of_nat m.
 Proof.
   intros x y; intros H; elim H;
@@ -81,29 +89,100 @@ Proof.
     exact H.
 Qed.
 
+Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+Proof.
+  intros x y H; apply Zle_ge; apply inj_le; apply H.
+Qed.
+
 Theorem inj_gt : forall n m:nat, (n > m)%nat -> Z_of_nat n > Z_of_nat m.
 Proof.
   intros x y H; apply Zlt_gt; apply inj_lt; exact H.
 Qed.
 
-Theorem inj_ge : forall n m:nat, (n >= m)%nat -> Z_of_nat n >= Z_of_nat m.
+(** The other way ... *)
+
+Theorem inj_le_rev : forall n m:nat, Z_of_nat n <= Z_of_nat m -> (n <= m)%nat.
 Proof.
-  intros x y H; apply Zle_ge; apply inj_le; apply H.
+  intros x y H.
+  destruct (le_lt_dec x y) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_lt _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
 Qed.
 
-Theorem inj_eq : forall n m:nat, n = m -> Z_of_nat n = Z_of_nat m.
+Theorem inj_lt_rev : forall n m:nat, Z_of_nat n < Z_of_nat m -> (n < m)%nat.
 Proof.
-  intros x y H; rewrite H; trivial with arith.
+  intros x y H.
+  destruct (le_lt_dec y x) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_le _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
 Qed.
 
-Theorem intro_Z :
-  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Theorem inj_ge_rev : forall n m:nat, Z_of_nat n >= Z_of_nat m -> (n >= m)%nat.
 Proof.
-  intros x; exists (Z_of_nat x); split;
-    [ trivial with arith
-      | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
-	unfold Zle in |- *; elim x; intros; simpl in |- *; 
-          discriminate ].
+  intros x y H.
+  destruct (le_lt_dec y x) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_gt _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H; rewrite H1 in H; auto.
+Qed.
+
+Theorem inj_gt_rev : forall n m:nat, Z_of_nat n > Z_of_nat m -> (n > m)%nat.
+Proof.
+  intros x y H.
+  destruct (le_lt_dec x y) as [H0|H0]; auto.
+  elimtype False.
+  assert (H1:=inj_ge _ _ H0).
+  red in H; red in H1.
+  rewrite <- Zcompare_antisym in H1; rewrite H in H1; auto.
+Qed.
+
+(* Both ways ... *)
+
+Theorem inj_le_iff : forall n m:nat, (n<=m)%nat <-> Z_of_nat n <= Z_of_nat m.
+Proof.
+ split; [apply inj_le | apply inj_le_rev].
+Qed.
+
+Theorem inj_lt_iff : forall n m:nat, (n<m)%nat <-> Z_of_nat n < Z_of_nat m.
+Proof.
+ split; [apply inj_lt | apply inj_lt_rev].
+Qed.
+
+Theorem inj_ge_iff : forall n m:nat, (n>=m)%nat <-> Z_of_nat n >= Z_of_nat m.
+Proof.
+ split; [apply inj_ge | apply inj_ge_rev].
+Qed.
+
+Theorem inj_gt_iff : forall n m:nat, (n>m)%nat <-> Z_of_nat n > Z_of_nat m.
+Proof.
+ split; [apply inj_gt | apply inj_gt_rev].
+Qed.
+
+(** Injection and usual operations *)
+ 
+Theorem inj_plus : forall n m:nat, Z_of_nat (n + m) = Z_of_nat n + Z_of_nat m.
+Proof.
+  intro x; induction x as [| n H]; intro y; destruct y as [| m];
+    [ simpl in |- *; trivial with arith
+      | simpl in |- *; trivial with arith
+      | simpl in |- *; rewrite <- plus_n_O; trivial with arith
+      | change (Z_of_nat (S (n + S m)) = Z_of_nat (S n) + Z_of_nat (S m)) in |- *;
+	rewrite inj_S; rewrite H; do 2 rewrite inj_S; rewrite Zplus_succ_l;
+	  trivial with arith ].
+Qed.
+
+Theorem inj_mult : forall n m:nat, Z_of_nat (n * m) = Z_of_nat n * Z_of_nat m.
+Proof.
+  intro x; induction x as [| n H];
+    [ simpl in |- *; trivial with arith
+      | intro y; rewrite inj_S; rewrite <- Zmult_succ_l_reverse; rewrite <- H;
+	rewrite <- inj_plus; simpl in |- *; rewrite plus_comm; 
+	  trivial with arith ].
 Qed.
 
 Theorem inj_minus1 :
@@ -121,6 +200,46 @@ Proof.
     [ trivial with arith | apply gt_not_le; assumption ].
 Qed.
 
+Theorem inj_minus : forall n m:nat, 
+ Z_of_nat (minus n m) = Zmax 0 (Z_of_nat n - Z_of_nat m).
+Proof.
+ intros.
+ rewrite Zmax_comm.
+ unfold Zmax.
+ destruct (le_lt_dec m n) as [H|H].
+
+ rewrite (inj_minus1 _ _ H).
+ assert (H':=Zle_minus_le_0 _ _ (inj_le _ _ H)).
+ unfold Zle in H'.
+ rewrite <- Zcompare_antisym in H'.
+ destruct Zcompare; simpl in *; intuition.
+
+ rewrite (inj_minus2 _ _ H).
+ assert (H':=Zplus_lt_compat_r _ _ (- Z_of_nat m) (inj_lt _ _ H)).
+ rewrite Zplus_opp_r in H'.
+ unfold Zminus; rewrite H'; auto.
+Qed.
+
+Theorem inj_min : forall n m:nat, 
+  Z_of_nat (min n m) = Zmin (Z_of_nat n) (Z_of_nat m).
+Proof.
+ induction n; destruct m; try (compute; auto; fail).
+ simpl min.
+ do 3 rewrite inj_S.
+ rewrite <- Zsucc_min_distr; f_equal; auto.
+Qed.
+
+Theorem inj_max : forall n m:nat, 
+  Z_of_nat (max n m) = Zmax (Z_of_nat n) (Z_of_nat m).
+Proof.
+ induction n; destruct m; try (compute; auto; fail).
+ simpl max.
+ do 3 rewrite inj_S.
+ rewrite <- Zsucc_max_distr; f_equal; auto.
+Qed.
+
+(** Composition of injections **)
+
 Theorem Zpos_eq_Z_of_nat_o_nat_of_P :
   forall p:positive, Zpos p = Z_of_nat (nat_of_P p).
 Proof.
@@ -136,3 +255,31 @@ Proof.
   rewrite inj_plus; repeat rewrite <- H.
   rewrite Zpos_xO; simpl in |- *; rewrite Pplus_diag; reflexivity.
 Qed.
+
+Theorem inj_Zabs_nat : forall z:Z, Z_of_nat (Zabs_nat z) = Zabs z.
+Proof.
+destruct z; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
+Qed.
+
+(** Misc *)
+
+Theorem intro_Z :
+  forall n:nat,  exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0.
+Proof.
+  intros x; exists (Z_of_nat x); split;
+    [ trivial with arith
+      | rewrite Zmult_comm; rewrite Zmult_1_l; rewrite Zplus_0_r;
+	unfold Zle in |- *; elim x; intros; simpl in |- *; 
+          discriminate ].
+Qed.
+
+Lemma Zpos_P_of_succ_nat : forall n:nat, 
+ Zpos (P_of_succ_nat n) = Zsucc (Z_of_nat n).
+Proof.
+  intros.
+  unfold Z_of_nat.
+  destruct n.
+  simpl; auto.
+  simpl (P_of_succ_nat (S n)).
+  apply Zpos_succ_morphism.
+Qed.