Some cleanup of Zcomplements

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14254 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 36 insertions, 95 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 03f68c024..86e9eb8ca 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -16,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]
@@ -56,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.
 
 (**********************************************************************)
@@ -88,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.
 
@@ -132,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.
 
 (**********************************************************************)
@@ -173,34 +119,29 @@ 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.