summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zcomplements.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2012-01-12 16:02:20 +0100
commit97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch)
tree97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /theories/ZArith/Zcomplements.v
parent300293c119981054c95182a90c829058530a6b6f (diff)
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'theories/ZArith/Zcomplements.v')
-rw-r--r--theories/ZArith/Zcomplements.v143
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 _.