diff options
Diffstat (limited to 'theories/ZArith/Zabs.v')
| -rw-r--r-- | theories/ZArith/Zabs.v | 114 |
1 files changed, 58 insertions, 56 deletions
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index fed6ad76..ed641358 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -5,11 +5,11 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zabs.v 5920 2004-07-16 20:01:26Z herbelin $ i*) +(*i $Id: Zabs.v 9302 2006-10-27 21:21:17Z barras $ i*) (** Binary Integers (Pierre Crégut (CNET, Lannion, France) *) -Require Import Arith. +Require Import Arith_base. Require Import BinPos. Require Import BinInt. Require Import Zorder. @@ -18,111 +18,113 @@ Require Import ZArith_dec. Open Local Scope Z_scope. (**********************************************************************) -(** Properties of absolute value *) +(** * Properties of absolute value *) Lemma Zabs_eq : forall n:Z, 0 <= n -> Zabs n = n. -intro x; destruct x; auto with arith. -compute in |- *; intros; absurd (Gt = Gt); trivial with arith. +Proof. + intro x; destruct x; auto with arith. + compute in |- *; intros; absurd (Gt = Gt); trivial with arith. Qed. Lemma Zabs_non_eq : forall n:Z, n <= 0 -> Zabs n = - n. Proof. -intro x; destruct x; auto with arith. -compute in |- *; intros; absurd (Gt = Gt); trivial with arith. + intro x; destruct x; auto with arith. + compute in |- *; intros; absurd (Gt = Gt); trivial with arith. Qed. Theorem Zabs_Zopp : forall n:Z, Zabs (- n) = Zabs n. Proof. -intros z; case z; simpl in |- *; auto. + intros z; case z; simpl in |- *; auto. Qed. -(** Proving a property of the absolute value by cases *) +(** * 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). + forall (P:Z -> Prop) (n:Z), + (n >= 0 -> P n) -> (n <= 0 -> P (- n)) -> P (Zabs 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 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. Qed. Theorem Zabs_intro : forall P (n:Z), P (- n) -> P n -> P (Zabs n). -intros P z; case z; simpl in |- *; auto. +Proof. + intros P z; case z; simpl in |- *; auto. Qed. Definition Zabs_dec : forall x:Z, {x = Zabs x} + {x = - Zabs x}. Proof. -intro x; destruct x; auto with arith. + intro x; destruct x; auto with arith. Defined. Lemma Zabs_pos : forall n:Z, 0 <= Zabs n. -intro x; destruct x; auto with arith; compute in |- *; intros H; inversion H. + intro x; destruct x; auto with arith; compute in |- *; intros H; inversion H. Qed. Theorem Zabs_eq_case : forall n m:Z, Zabs n = Zabs m -> n = m \/ n = - m. 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. + 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. -(** Triangular inequality *) +(** * 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. + 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 *) +(** * 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. + 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. + 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. + intros z1 z2; case z1; case z2; simpl in |- *; auto. Qed. -(** absolute value in nat is compatible with order *) +(** * Absolute value in nat is compatible with order *) Lemma Zabs_nat_lt : - forall n m:Z, 0 <= n /\ n < m -> (Zabs_nat n < Zabs_nat m)%nat. + forall n m:Z, 0 <= n /\ n < m -> (Zabs_nat n < Zabs_nat m)%nat. Proof. -intros x y. case x; simpl in |- *. case y; simpl in |- *. - -intro. absurd (0 < 0). compute in |- *. intro H0. discriminate H0. intuition. -intros. elim (ZL4 p). intros. rewrite H0. auto with arith. -intros. elim (ZL4 p). intros. rewrite H0. auto with arith. - -case y; simpl in |- *. -intros. absurd (Zpos p < 0). compute in |- *. intro H0. discriminate H0. intuition. -intros. change (nat_of_P p > nat_of_P p0)%nat in |- *. -apply nat_of_P_gt_Gt_compare_morphism. -elim H; auto with arith. intro. exact (ZC2 p0 p). - -intros. absurd (Zpos p0 < Zneg p). -compute in |- *. intro H0. discriminate H0. intuition. - -intros. absurd (0 <= Zneg p). compute in |- *. auto with arith. intuition. -Qed.
\ No newline at end of file + intros x y. case x; simpl in |- *. case y; simpl in |- *. + + intro. absurd (0 < 0). compute in |- *. intro H0. discriminate H0. intuition. + intros. elim (ZL4 p). intros. rewrite H0. auto with arith. + intros. elim (ZL4 p). intros. rewrite H0. auto with arith. + + case y; simpl in |- *. + intros. absurd (Zpos p < 0). compute in |- *. intro H0. discriminate H0. intuition. + intros. change (nat_of_P p > nat_of_P p0)%nat in |- *. + apply nat_of_P_gt_Gt_compare_morphism. + elim H; auto with arith. intro. exact (ZC2 p0 p). + + intros. absurd (Zpos p0 < Zneg p). + compute in |- *. intro H0. discriminate H0. intuition. + + intros. absurd (0 <= Zneg p). compute in |- *. auto with arith. intuition. +Qed. |