diff options
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
| -rw-r--r-- | theories/ZArith/Zcomplements.v | 143 |
1 files changed, 41 insertions, 102 deletions
diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v index ca72f8a8..5a2c3cc3 100644 --- a/theories/ZArith/Zcomplements.v +++ b/theories/ZArith/Zcomplements.v @@ -1,13 +1,11 @@ (************************************************************************) (* 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: Zcomplements.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import ZArithRing. Require Import ZArith_base. Require Export Omega. @@ -18,29 +16,7 @@ Open Local Scope Z_scope. (**********************************************************************) (** About parity *) -Lemma two_or_two_plus_one : - forall n:Z, {y : Z | n = 2 * y} + {y : Z | n = 2 * y + 1}. -Proof. - intro x; destruct x. - left; split with 0; reflexivity. - - destruct p. - right; split with (Zpos p); reflexivity. - - left; split with (Zpos p); reflexivity. - - right; split with 0; reflexivity. - - destruct p. - right; split with (Zneg (1 + p)). - rewrite BinInt.Zneg_xI. - rewrite BinInt.Zneg_plus_distr. - omega. - - left; split with (Zneg p); reflexivity. - - right; split with (-1); reflexivity. -Qed. +Notation two_or_two_plus_one := Z_modulo_2 (only parsing). (**********************************************************************) (** The biggest power of 2 that is stricly less than [a] @@ -58,31 +34,14 @@ Fixpoint floor_pos (a:positive) : positive := Definition floor (a:positive) := Zpos (floor_pos a). Lemma floor_gt0 : forall p:positive, floor p > 0. -Proof. - intro. - compute in |- *. - trivial. -Qed. +Proof. reflexivity. Qed. Lemma floor_ok : forall p:positive, floor p <= Zpos p < 2 * floor p. Proof. - unfold floor in |- *. - intro a; induction a as [p| p| ]. - - simpl in |- *. - repeat rewrite BinInt.Zpos_xI. - rewrite (BinInt.Zpos_xO (xO (floor_pos p))). - rewrite (BinInt.Zpos_xO (floor_pos p)). - omega. - - simpl in |- *. - repeat rewrite BinInt.Zpos_xI. - rewrite (BinInt.Zpos_xO (xO (floor_pos p))). - rewrite (BinInt.Zpos_xO (floor_pos p)). - rewrite (BinInt.Zpos_xO p). - omega. - - simpl in |- *; omega. + unfold floor. induction p; simpl. + - rewrite !Z.pos_xI, (Z.pos_xO (xO _)), Z.pos_xO. omega. + - rewrite (Z.pos_xO (xO _)), (Z.pos_xO p), Z.pos_xO. omega. + - omega. Qed. (**********************************************************************) @@ -90,41 +49,39 @@ Qed. Theorem Z_lt_abs_rec : forall P:Z -> Set, - (forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) -> + (forall n:Z, (forall m:Z, Z.abs m < Z.abs n -> P m) -> P n) -> forall n:Z, P n. Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z * P (- z)) in *. - cut (Q (Zabs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ]. + cut (Q (Z.abs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ]. elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. unfold Q in |- *; clear Q; intros. - apply pair; apply HP. - rewrite Zabs_eq; auto; intros. - elim (H (Zabs m)); intros; auto with zarith. + split; apply HP. + rewrite Z.abs_eq; auto; intros. + elim (H (Z.abs m)); intros; auto with zarith. elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Zabs_non_eq; auto with zarith. - rewrite Zopp_involutive; intros. - elim (H (Zabs m)); intros; auto with zarith. + rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. + elim (H (Z.abs m)); intros; auto with zarith. elim (Zabs_dec m); intro eq; rewrite eq; trivial. Qed. Theorem Z_lt_abs_induction : forall P:Z -> Prop, - (forall n:Z, (forall m:Z, Zabs m < Zabs n -> P m) -> P n) -> + (forall n:Z, (forall m:Z, Z.abs m < Z.abs n -> P m) -> P n) -> forall n:Z, P n. Proof. intros P HP p. set (Q := fun z => 0 <= z -> P z /\ P (- z)) in *. - cut (Q (Zabs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ]. + cut (Q (Z.abs p)); [ intros | apply (Z_lt_induction Q); auto with zarith ]. elim (Zabs_dec p); intro eq; rewrite eq; elim H; auto with zarith. unfold Q in |- *; clear Q; intros. split; apply HP. - rewrite Zabs_eq; auto; intros. - elim (H (Zabs m)); intros; auto with zarith. + rewrite Z.abs_eq; auto; intros. + elim (H (Z.abs m)); intros; auto with zarith. elim (Zabs_dec m); intro eq; rewrite eq; trivial. - rewrite Zabs_non_eq; auto with zarith. - rewrite Zopp_involutive; intros. - elim (H (Zabs m)); intros; auto with zarith. + rewrite Z.abs_neq, Z.opp_involutive; auto with zarith; intros. + elim (H (Z.abs m)); intros; auto with zarith. elim (Zabs_dec m); intro eq; rewrite eq; trivial. Qed. @@ -134,25 +91,12 @@ Lemma Zcase_sign : forall (n:Z) (P:Prop), (n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P. Proof. intros x P Hzero Hpos Hneg. - induction x as [| p| p]. - apply Hzero; trivial. - apply Hpos; apply Zorder.Zgt_pos_0. - apply Hneg; apply Zorder.Zlt_neg_0. + destruct x; [apply Hzero|apply Hpos|apply Hneg]; easy. Qed. -Lemma sqr_pos : forall n:Z, n * n >= 0. +Lemma sqr_pos n : n * n >= 0. Proof. - intro x. - apply (Zcase_sign x (x * x >= 0)). - intros H; rewrite H; omega. - intros H; replace 0 with (0 * 0). - apply Zmult_ge_compat; omega. - omega. - intros H; replace 0 with (0 * 0). - replace (x * x) with (- x * - x). - apply Zmult_ge_compat; omega. - ring. - omega. + Z.swap_greater. apply Z.square_nonneg. Qed. (**********************************************************************) @@ -167,7 +111,7 @@ Fixpoint Zlength_aux (acc:Z) (A:Type) (l:list A) : Z := end. Definition Zlength := Zlength_aux 0. -Implicit Arguments Zlength [A]. +Arguments Zlength [A] l. Section Zlength_properties. @@ -175,38 +119,33 @@ Section Zlength_properties. Implicit Type l : list A. - Lemma Zlength_correct : forall l, Zlength l = Z_of_nat (length l). + Lemma Zlength_correct l : Zlength l = Z.of_nat (length l). Proof. - assert (forall l (acc:Z), Zlength_aux acc A l = acc + Z_of_nat (length l)). - simple induction l. - simpl in |- *; auto with zarith. - intros; simpl (length (a :: l0)) in |- *; rewrite Znat.inj_S. - simpl in |- *; rewrite H; auto with zarith. - unfold Zlength in |- *; intros; rewrite H; auto. + assert (H : forall l acc, Zlength_aux acc A l = acc + Z.of_nat (length l)). + clear l. induction l. + auto with zarith. + intros. simpl length; simpl Zlength_aux. + rewrite IHl, Nat2Z.inj_succ; auto with zarith. + unfold Zlength. now rewrite H. Qed. Lemma Zlength_nil : Zlength (A:=A) nil = 0. - Proof. - auto. - Qed. + Proof. reflexivity. Qed. - Lemma Zlength_cons : forall (x:A) l, Zlength (x :: l) = Zsucc (Zlength l). + Lemma Zlength_cons (x:A) l : Zlength (x :: l) = Z.succ (Zlength l). Proof. - intros; do 2 rewrite Zlength_correct. - simpl (length (x :: l)) in |- *; rewrite Znat.inj_S; auto. + intros. now rewrite !Zlength_correct, <- Nat2Z.inj_succ. Qed. - Lemma Zlength_nil_inv : forall l, Zlength l = 0 -> l = nil. + Lemma Zlength_nil_inv l : Zlength l = 0 -> l = nil. Proof. - intro l; rewrite Zlength_correct. - case l; auto. - intros x l'; simpl (length (x :: l')) in |- *. - rewrite Znat.inj_S. - intros; exfalso; generalize (Zle_0_nat (length l')); omega. + rewrite Zlength_correct. + destruct l as [|x l]; auto. + now rewrite <- Nat2Z.inj_0, Nat2Z.inj_iff. Qed. End Zlength_properties. -Implicit Arguments Zlength_correct [A]. -Implicit Arguments Zlength_cons [A]. -Implicit Arguments Zlength_nil_inv [A]. +Arguments Zlength_correct [A] l. +Arguments Zlength_cons [A] x l. +Arguments Zlength_nil_inv [A] l _. |