Imported Upstream version 8.4~betaupstream/8.4_beta

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 _.