Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 129 insertions, 129 deletions

diff --git a/theories/ZArith/Zcomplements.v b/theories/ZArith/Zcomplements.v
index 817fbc1b..78c8a976 100644
--- a/theories/ZArith/Zcomplements.v
+++ b/theories/ZArith/Zcomplements.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Zcomplements.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: Zcomplements.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import ZArithRing.
 Require Import ZArith_base.
@@ -19,27 +19,27 @@ 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}. 
+  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.
+  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.
 
 (**********************************************************************)
@@ -50,109 +50,109 @@ Qed.
 
 Fixpoint floor_pos (a:positive) : positive :=
   match a with
-  | xH => 1%positive
-  | xO a' => xO (floor_pos a')
-  | xI b' => xO (floor_pos b')
+    | xH => 1%positive
+    | xO a' => xO (floor_pos a')
+    | xI b' => xO (floor_pos b')
   end.
 
 Definition floor (a:positive) := Zpos (floor_pos a).
 
 Lemma floor_gt0 : forall p:positive, floor p > 0.
 Proof.
-intro.
-compute in |- *.
-trivial.
+  intro.
+  compute in |- *.
+  trivial.
 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 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.
 Qed.
 
 (**********************************************************************)
 (** Two more induction principles over [Z]. *)
 
 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, P n.
+  forall P:Z -> Set,
+    (forall n:Z, (forall m:Z, Zabs m < Zabs 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 ].
-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.
-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.
-elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+  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 ].
+  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.
+  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.
+  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, P n.
+  forall P:Z -> Prop,
+    (forall n:Z, (forall m:Z, Zabs m < Zabs 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 ].
-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.
-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.
-elim (Zabs_dec m); intro eq; rewrite eq; trivial.
+  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 ].
+  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.
+  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.
+  elim (Zabs_dec m); intro eq; rewrite eq; trivial.
 Qed.
 
 (** To do case analysis over the sign of [z] *) 
 
 Lemma Zcase_sign :
- forall (n:Z) (P:Prop), (n = 0 -> P) -> (n > 0 -> P) -> (n < 0 -> P) -> P.
+  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.
+  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.
 Qed.
 
 Lemma sqr_pos : forall n:Z, 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.
+  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.
 Qed.
 
 (**********************************************************************)
@@ -162,8 +162,8 @@ Require Import List.
 
 Fixpoint Zlength_aux (acc:Z) (A:Set) (l:list A) {struct l} : Z :=
   match l with
-  | nil => acc
-  | _ :: l => Zlength_aux (Zsucc acc) A l
+    | nil => acc
+    | _ :: l => Zlength_aux (Zsucc acc) A l
   end. 
 
 Definition Zlength := Zlength_aux 0.
@@ -171,42 +171,42 @@ Implicit Arguments Zlength [A].
 
 Section Zlength_properties.
 
-Variable A : Set.
-
-Implicit Type l : list A.
-
-Lemma Zlength_correct : forall 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.
-Qed.
-
-Lemma Zlength_nil : Zlength (A:=A) nil = 0.
-Proof.
-auto.
-Qed.
-
-Lemma Zlength_cons : forall (x:A) l, Zlength (x :: l) = Zsucc (Zlength l).
-Proof.
-intros; do 2 rewrite Zlength_correct.
-simpl (length (x :: l)) in |- *; rewrite Znat.inj_S; auto.
-Qed.
-
-Lemma Zlength_nil_inv : forall 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; elimtype False; generalize (Zle_0_nat (length l')); omega.
-Qed.
+  Variable A : Set.
+
+  Implicit Type l : list A.
+
+  Lemma Zlength_correct : forall 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.
+  Qed.
+
+  Lemma Zlength_nil : Zlength (A:=A) nil = 0.
+  Proof.
+    auto.
+  Qed.
+
+  Lemma Zlength_cons : forall (x:A) l, Zlength (x :: l) = Zsucc (Zlength l).
+  Proof.
+    intros; do 2 rewrite Zlength_correct.
+    simpl (length (x :: l)) in |- *; rewrite Znat.inj_S; auto.
+  Qed.
+
+  Lemma Zlength_nil_inv : forall 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; elimtype False; generalize (Zle_0_nat (length l')); omega.
+  Qed.
 
 End Zlength_properties.
 
 Implicit Arguments Zlength_correct [A].
 Implicit Arguments Zlength_cons [A].
-Implicit Arguments Zlength_nil_inv [A].
\ No newline at end of file
+Implicit Arguments Zlength_nil_inv [A].