diff options
| -rw-r--r-- | theories/ZArith/Zabs.v | 153 | ||||
| -rw-r--r-- | theories/ZArith/Znat.v | 40 |
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. |