cleanup of Zsgn

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

2 files changed, 81 insertions, 112 deletions

diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v
index 4941dedb2..23473e932 100644
--- a/theories/ZArith/Zabs.v
+++ b/theories/ZArith/Zabs.v
@@ -6,7 +6,13 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+
+(** Binary Integers : properties of absolute value *)
+(** Initial author : Pierre Crégut (CNET, Lannion, France) *)
+
+(** THIS FILE IS DEPRECATED.
+    It is now almost entirely made of compatibility formulations
+    for results already present in BinInt.Z. *)
 
 Require Import Arith_base.
 Require Import BinPos.
@@ -21,135 +27,61 @@ Local Open Scope Z_scope.
 (**********************************************************************)
 (** * Properties of absolute value *)
 
-Notation Zabs_eq := Z.abs_eq (only parsing). (* 0 <= n -> Zabs n = n *)
-Notation Zabs_non_eq := Z.abs_neq (only parsing). (* n <= 0 -> Zabs n = -n *)
-
-Theorem Zabs_Zopp : forall n:Z, Zabs (- n) = Zabs n.
-Proof.
-  intros z; case z; simpl; auto.
-Qed.
+Notation Zabs_eq := Z.abs_eq (only parsing).
+Notation Zabs_non_eq := Z.abs_neq (only parsing).
+Notation Zabs_Zopp := Z.abs_opp (only parsing).
+Notation Zabs_pos := Z.abs_nonneg (only parsing).
+Notation Zabs_involutive := Z.abs_involutive (only parsing).
+Notation Zabs_eq_case := Z.abs_eq_cases (only parsing).
+Notation Zabs_triangle := Z.abs_triangle (only parsing).
+Notation Zsgn_Zabs := Z.sgn_abs (only parsing).
+Notation Zabs_Zsgn := Z.abs_sgn (only parsing).
+Notation Zabs_Zmult := Z.abs_mul (only parsing).
+Notation Zabs_square := Z.abs_square (only parsing).
 
 (** * Proving a property of the absolute value by cases *)
 
 Lemma Zabs_ind :
   forall (P:Z -> Prop) (n:Z),
-    (n >= 0 -> P n) -> (n <= 0 -> P (- n)) -> P (Zabs n).
+    (n >= 0 -> P n) -> (n <= 0 -> P (- n)) -> P (Z.abs n).
 Proof.
-  intros P x H H0; elim (Z_lt_ge_dec x 0); intro.
-  assert (x <= 0). apply Zlt_le_weak; assumption.
-  rewrite Zabs_non_eq. apply H0. assumption. assumption.
-  rewrite Zabs_eq. apply H; assumption. apply Zge_le. assumption.
+ intros. apply Z.abs_case_strong; Z.swap_greater; trivial.
+ intros x y Hx; now subst.
 Qed.
 
-Theorem Zabs_intro : forall P (n:Z), P (- n) -> P n -> P (Zabs n).
+Theorem Zabs_intro : forall P (n:Z), P (- n) -> P n -> P (Z.abs n).
 Proof.
-  intros P z; case z; simpl in |- *; auto.
+ now destruct n.
 Qed.
 
-Definition Zabs_dec : forall x:Z, {x = Zabs x} + {x = - Zabs x}.
+Definition Zabs_dec : forall x:Z, {x = Z.abs x} + {x = - Z.abs x}.
 Proof.
-  intro x; destruct x; auto with arith.
+ destruct x; auto.
 Defined.
 
-Lemma Zabs_pos : forall n:Z, 0 <= Zabs n.
-  intro x; destruct x; auto with arith; compute in |- *; intros H; inversion H.
-Qed.
-
-Lemma Zabs_involutive : forall x:Z, Zabs (Zabs x) = Zabs x.
-Proof.
-  intros; apply Zabs_eq; apply Zabs_pos.
-Qed.
-
-Theorem Zabs_eq_case : forall n m:Z, Zabs n = Zabs m -> n = m \/ n = - m.
+Lemma Zabs_spec x :
+  0 <= x /\ Z.abs x = x \/
+  0 > x /\ Z.abs x = -x.
 Proof.
-  intros z1 z2; case z1; case z2; simpl in |- *; auto;
-    try (intros; discriminate); intros p1 p2 H1; injection H1;
-      (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.
-
-Theorem Zabs_triangle : forall n m:Z, Zabs (n + m) <= Zabs n + Zabs m.
-Proof.
-  intros z1 z2; case z1; case z2; try (simpl in |- *; auto with zarith; fail).
-  intros p1 p2;
-    apply Zabs_intro with (P := fun x => x <= Zabs (Zpos p2) + Zabs (Zneg p1));
-      try rewrite Zopp_plus_distr; auto with zarith.
-  apply Zplus_le_compat; simpl in |- *; auto with zarith.
-  apply Zplus_le_compat; simpl in |- *; auto with zarith.
-  intros p1 p2;
-    apply Zabs_intro with (P := fun x => x <= Zabs (Zpos p2) + Zabs (Zneg p1));
-      try rewrite Zopp_plus_distr; auto with zarith.
-  apply Zplus_le_compat; simpl in |- *; auto with zarith.
-  apply Zplus_le_compat; simpl in |- *; auto with zarith.
-Qed.
-
-(** * Absolute value and multiplication *)
-
-Lemma Zsgn_Zabs : forall n:Z, n * Zsgn n = Zabs n.
-Proof.
-  intro x; destruct x; rewrite Zmult_comm; auto with arith.
-Qed.
-
-Lemma Zabs_Zsgn : forall n:Z, Zabs n * Zsgn n = n.
-Proof.
-  intro x; destruct x; rewrite Zmult_comm; auto with arith.
-Qed.
-
-Theorem Zabs_Zmult : forall n m:Z, Zabs (n * m) = Zabs n * Zabs m.
-Proof.
-  intros z1 z2; case z1; case z2; simpl in |- *; auto.
-Qed.
-
-Theorem Zabs_square : forall a, Zabs a * Zabs a = a * a.
-Proof.
-  destruct a; simpl; auto.
+ Z.swap_greater. apply Z.abs_spec.
 Qed.
 
 (** * Some results about the sign function. *)
 
-Lemma Zsgn_Zmult : forall a b, Zsgn (a*b) = Zsgn a * Zsgn b.
-Proof.
-  destruct a; destruct b; simpl; auto.
-Qed.
-
-Lemma Zsgn_Zopp : forall a, Zsgn (-a) = - Zsgn a.
-Proof.
-  destruct a; simpl; auto.
-Qed.
+Notation Zsgn_Zmult := Z.sgn_mul (only parsing).
+Notation Zsgn_Zopp := Z.sgn_opp (only parsing).
+Notation Zsgn_pos := Z.sgn_pos_iff (only parsing).
+Notation Zsgn_neg := Z.sgn_neg_iff (only parsing).
+Notation Zsgn_null := Z.sgn_null_iff (only parsing).
 
 (** A characterization of the sign function: *)
 
-Lemma Zsgn_spec : forall x:Z,
+Lemma Zsgn_spec x :
   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.
-
-Lemma Zsgn_pos : forall x:Z, Zsgn x = 1 <-> 0 < x.
-Proof.
- destruct x; now intuition.
-Qed.
-
-Lemma Zsgn_neg : forall x:Z, Zsgn x = -1 <-> x < 0.
-Proof.
- destruct x; now intuition.
-Qed.
-
-Lemma Zsgn_null : forall x:Z, Zsgn x = 0 <-> x = 0.
-Proof.
- destruct x; now intuition.
+ intros. Z.swap_greater. apply Z.sgn_spec.
 Qed.
 
 (** Compatibility *)
@@ -162,16 +94,13 @@ Notation Zabs_nat_Zplus := Zabs2Nat.inj_add (only parsing).
 Notation Zabs_nat_Zminus := (fun n m => Zabs2Nat.inj_sub m n) (only parsing).
 Notation Zabs_nat_compare := Zabs2Nat.inj_compare (only parsing).
 
-Lemma Zabs_nat_le :
-  forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat.
+Lemma Zabs_nat_le n m : 0 <= n <= m -> (Z.abs_nat n <= Z.abs_nat m)%nat.
 Proof.
- intros n m (H,H'). apply nat_compare_le. rewrite Zabs_nat_compare; trivial.
- apply Zle_trans with n; auto.
+ intros (H,H'). apply Zabs2Nat.inj_le; trivial. now transitivity n.
 Qed.
 
-Lemma Zabs_nat_lt :
-  forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat.
+Lemma Zabs_nat_lt n m : 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat.
 Proof.
-  intros n m (H,H'). apply nat_compare_lt. rewrite Zabs_nat_compare; trivial.
-  apply Zlt_le_weak; apply Zle_lt_trans with n; auto.
+ intros (H,H'). apply Zabs2Nat.inj_lt; trivial.
+  transitivity n; trivial. now apply Z.lt_le_incl.
 Qed.
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v
index bc3d73484..84262469b 100644
--- a/theories/ZArith/Znat.v
+++ b/theories/ZArith/Znat.v
@@ -290,6 +290,16 @@ Proof.
  intros Hn Hm. now rewrite <- N2Z.inj_compare, !id.
 Qed.
 
+Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.to_N n <= Z.to_N m)%N).
+Proof.
+ intros Hn Hm. unfold Z.le, N.le. now rewrite inj_compare.
+Qed.
+
+Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.to_N n < Z.to_N m)%N).
+Proof.
+ intros Hn Hm. unfold Z.lt, N.lt. now rewrite inj_compare.
+Qed.
+
 Lemma inj_min n m : Z.to_N (Z.min n m) = N.min (Z.to_N n) (Z.to_N m).
 Proof.
  destruct n, m; simpl; trivial; unfold Z.min, N.min; simpl;
@@ -386,6 +396,16 @@ Proof.
  intros. rewrite !abs_N_nonneg by trivial. now apply Z2N.inj_compare.
 Qed.
 
+Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.abs_N n <= Z.abs_N m)%N).
+Proof.
+ intros Hn Hm. unfold Z.le, N.le. now rewrite inj_compare.
+Qed.
+
+Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.abs_N n < Z.abs_N m)%N).
+Proof.
+ intros Hn Hm. unfold Z.lt, N.lt. now rewrite inj_compare.
+Qed.
+
 Lemma inj_min n m : 0<=n -> 0<=m ->
  Z.abs_N (Z.min n m) = N.min (Z.abs_N n) (Z.abs_N m).
 Proof.
@@ -619,6 +639,16 @@ Proof.
  intros Hn Hm. now rewrite <- Nat2Z.inj_compare, !id.
 Qed.
 
+Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.to_nat n <= Z.to_nat m)%nat).
+Proof.
+ intros Hn Hm. unfold Z.le. now rewrite nat_compare_le, inj_compare.
+Qed.
+
+Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.to_nat n < Z.to_nat m)%nat).
+Proof.
+ intros Hn Hm. unfold Z.lt. now rewrite nat_compare_lt, inj_compare.
+Qed.
+
 Lemma inj_min n m : Z.to_nat (Z.min n m) = min (Z.to_nat n) (Z.to_nat m).
 Proof.
  now rewrite <- !Z_N_nat, Z2N.inj_min, N2Nat.inj_min.
@@ -708,6 +738,16 @@ Proof.
  intros. now rewrite <- !Zabs_N_nat, <- N2Nat.inj_compare, Zabs2N.inj_compare.
 Qed.
 
+Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.abs_nat n <= Z.abs_nat m)%nat).
+Proof.
+ intros Hn Hm. unfold Z.le. now rewrite nat_compare_le, inj_compare.
+Qed.
+
+Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.abs_nat n < Z.abs_nat m)%nat).
+Proof.
+ intros Hn Hm. unfold Z.lt. now rewrite nat_compare_lt, inj_compare.
+Qed.
+
 Lemma inj_min n m : 0<=n -> 0<=m ->
  Z.abs_nat (Z.min n m) = min (Z.abs_nat n) (Z.abs_nat m).
 Proof.