diff options
Diffstat (limited to 'theories/ZArith/Zabs.v')
| -rw-r--r-- | theories/ZArith/Zabs.v | 224 |
1 files changed, 52 insertions, 172 deletions
diff --git a/theories/ZArith/Zabs.v b/theories/ZArith/Zabs.v index 0f6e62b7..23473e93 100644 --- a/theories/ZArith/Zabs.v +++ b/theories/ZArith/Zabs.v @@ -1,226 +1,106 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Zabs.v 14641 2011-11-06 11:59:10Z herbelin $ i*) -(** 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. Require Import BinInt. +Require Import Zcompare. Require Import Zorder. -Require Import Zmax. Require Import Znat. Require Import ZArith_dec. -Open Local Scope Z_scope. +Local Open Scope Z_scope. (**********************************************************************) (** * Properties of absolute value *) -Lemma Zabs_eq : forall n:Z, 0 <= n -> Zabs n = n. -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. -Qed. - -Theorem Zabs_Zopp : forall n:Z, Zabs (- n) = Zabs n. -Proof. - intros z; case z; simpl in |- *; 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. -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. +Lemma Zabs_spec x : + 0 <= x /\ Z.abs x = x \/ + 0 > x /\ Z.abs x = -x. Proof. - destruct a; simpl; auto. -Qed. - -(** * Results about absolute value in nat. *) - -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. - -Theorem Zabs_nat_Z_of_nat: forall n, Zabs_nat (Z_of_nat n) = n. -Proof. - destruct n; simpl; auto. - apply nat_of_P_o_P_of_succ_nat_eq_succ. -Qed. - -Lemma Zabs_nat_mult: forall n m:Z, Zabs_nat (n*m) = (Zabs_nat n * Zabs_nat m)%nat. -Proof. - intros; apply inj_eq_rev. - rewrite inj_mult; repeat rewrite inj_Zabs_nat; apply Zabs_Zmult. -Qed. - -Lemma Zabs_nat_Zsucc: - forall p, 0 <= p -> Zabs_nat (Zsucc p) = S (Zabs_nat p). -Proof. - intros; apply inj_eq_rev. - rewrite inj_S; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith. -Qed. - -Lemma Zabs_nat_Zplus: - forall x y, 0<=x -> 0<=y -> Zabs_nat (x+y) = (Zabs_nat x + Zabs_nat y)%nat. -Proof. - intros; apply inj_eq_rev. - rewrite inj_plus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto with zarith. - apply Zplus_le_0_compat; auto. -Qed. - -Lemma Zabs_nat_Zminus: - forall x y, 0 <= x <= y -> Zabs_nat (y - x) = (Zabs_nat y - Zabs_nat x)%nat. -Proof. - intros x y (H,H'). - assert (0 <= y) by (apply Zle_trans with x; auto). - assert (0 <= y-x) by (apply Zle_minus_le_0; auto). - apply inj_eq_rev. - rewrite inj_minus; repeat rewrite inj_Zabs_nat, Zabs_eq; auto. - rewrite Zmax_right; auto. -Qed. - -Lemma Zabs_nat_le : - forall n m:Z, 0 <= n <= m -> (Zabs_nat n <= Zabs_nat m)%nat. -Proof. - intros n m (H,H'); apply inj_le_rev. - repeat rewrite inj_Zabs_nat, Zabs_eq; auto. - apply Zle_trans with n; auto. -Qed. - -Lemma Zabs_nat_lt : - forall n m:Z, 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat. -Proof. - intros n m (H,H'); apply inj_lt_rev. - repeat rewrite inj_Zabs_nat, Zabs_eq; auto. - apply Zlt_le_weak; apply Zle_lt_trans with n; 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. + intros. Z.swap_greater. apply Z.sgn_spec. Qed. -Lemma Zsgn_pos : forall x:Z, Zsgn x = 1 <-> 0 < x. -Proof. - destruct x; now intuition. -Qed. +(** Compatibility *) -Lemma Zsgn_neg : forall x:Z, Zsgn x = -1 <-> x < 0. +Notation inj_Zabs_nat := Zabs2Nat.id_abs (only parsing). +Notation Zabs_nat_Z_of_nat := Zabs2Nat.id (only parsing). +Notation Zabs_nat_mult := Zabs2Nat.inj_mul (only parsing). +Notation Zabs_nat_Zsucc := Zabs2Nat.inj_succ (only parsing). +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 n m : 0 <= n <= m -> (Z.abs_nat n <= Z.abs_nat m)%nat. Proof. - destruct x; now intuition. + intros (H,H'). apply Zabs2Nat.inj_le; trivial. now transitivity n. Qed. -Lemma Zsgn_null : forall x:Z, Zsgn x = 0 <-> x = 0. +Lemma Zabs_nat_lt n m : 0 <= n < m -> (Zabs_nat n < Zabs_nat m)%nat. Proof. - destruct x; now intuition. + intros (H,H'). apply Zabs2Nat.inj_lt; trivial. + transitivity n; trivial. now apply Z.lt_le_incl. Qed. - |