Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 163 insertions, 163 deletions

diff --git a/theories/ZArith/ZArith_dec.v b/theories/ZArith/ZArith_dec.v
index 40c5860c..84249955 100644
--- a/theories/ZArith/ZArith_dec.v
+++ b/theories/ZArith/ZArith_dec.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: ZArith_dec.v 5920 2004-07-16 20:01:26Z herbelin $ i*)
+(*i $Id: ZArith_dec.v 9245 2006-10-17 12:53:34Z notin $ i*)
 
 Require Import Sumbool.
 
@@ -17,210 +17,210 @@ Open Local Scope Z_scope.
 
 Lemma Dcompare_inf : forall r:comparison, {r = Eq} + {r = Lt} + {r = Gt}.
 Proof.
-simple induction r; auto with arith. 
+  simple induction r; auto with arith. 
 Defined.
 
 Lemma Zcompare_rec :
- forall (P:Set) (n m:Z),
-   ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
+  forall (P:Set) (n m:Z),
+    ((n ?= m) = Eq -> P) -> ((n ?= m) = Lt -> P) -> ((n ?= m) = Gt -> P) -> P.
 Proof.
-intros P x y H1 H2 H3.
-elim (Dcompare_inf (x ?= y)).
-intro H. elim H; auto with arith. auto with arith.
+  intros P x y H1 H2 H3.
+  elim (Dcompare_inf (x ?= y)).
+  intro H. elim H; auto with arith. auto with arith.
 Defined.
 
 Section decidability.
 
-Variables x y : Z.
-
-(** Decidability of equality on binary integers *)
-
-Definition Z_eq_dec : {x = y} + {x <> y}.
-Proof.
-apply Zcompare_rec with (n := x) (m := y).
-intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
-intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4.
-  rewrite (H2 H4) in H3. discriminate H3.
-intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4.
-  rewrite (H2 H4) in H3. discriminate H3.
-Defined. 
-
-(** Decidability of order on binary integers *)
-
-Definition Z_lt_dec : {x < y} + {~ x < y}.
-Proof.
-unfold Zlt in |- *.
-apply Zcompare_rec with (n := x) (m := y); intro H.
-right. rewrite H. discriminate.
-left; assumption.
-right. rewrite H. discriminate.
-Defined.
-
-Definition Z_le_dec : {x <= y} + {~ x <= y}.
-Proof.
-unfold Zle in |- *.
-apply Zcompare_rec with (n := x) (m := y); intro H.
-left. rewrite H. discriminate.
-left. rewrite H. discriminate.
-right. tauto.
-Defined.
-
-Definition Z_gt_dec : {x > y} + {~ x > y}.
-Proof.
-unfold Zgt in |- *.
-apply Zcompare_rec with (n := x) (m := y); intro H.
-right. rewrite H. discriminate.
-right. rewrite H. discriminate.
-left; assumption.
-Defined.
-
-Definition Z_ge_dec : {x >= y} + {~ x >= y}.
-Proof.
-unfold Zge in |- *.
-apply Zcompare_rec with (n := x) (m := y); intro H.
-left. rewrite H. discriminate.
-right. tauto.
-left. rewrite H. discriminate.
-Defined.
-
-Definition Z_lt_ge_dec : {x < y} + {x >= y}.
-Proof.
-exact Z_lt_dec.
-Defined.
-
-Lemma Z_lt_le_dec : {x < y} + {y <= x}.
-Proof.
-intros.
-elim Z_lt_ge_dec.
-intros; left; assumption.
-intros; right; apply Zge_le; assumption.
-Qed.
-
-Definition Z_le_gt_dec : {x <= y} + {x > y}.
-Proof.
-elim Z_le_dec; auto with arith.
-intro. right. apply Znot_le_gt; auto with arith.
-Defined.
-
-Definition Z_gt_le_dec : {x > y} + {x <= y}.
-Proof.
-exact Z_gt_dec.
-Defined.
-
-Definition Z_ge_lt_dec : {x >= y} + {x < y}.
-Proof.
-elim Z_ge_dec; auto with arith.
-intro. right. apply Znot_ge_lt; auto with arith.
-Defined.
-
-Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}.
-Proof.
-intro H.
-apply Zcompare_rec with (n := x) (m := y).
-intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith.
-intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
-intro H1. absurd (x > y); auto with arith.
-Defined.
+  Variables x y : Z.
+  
+  (** * Decidability of equality on binary integers *)
+
+  Definition Z_eq_dec : {x = y} + {x <> y}.
+  Proof.
+    apply Zcompare_rec with (n := x) (m := y).
+    intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
+    intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4.
+    rewrite (H2 H4) in H3. discriminate H3.
+    intro H3. right. elim (Zcompare_Eq_iff_eq x y). intros H1 H2. unfold not in |- *. intro H4.
+    rewrite (H2 H4) in H3. discriminate H3.
+  Defined. 
+
+  (** * Decidability of order on binary integers *)
+
+  Definition Z_lt_dec : {x < y} + {~ x < y}.
+  Proof.
+    unfold Zlt in |- *.
+    apply Zcompare_rec with (n := x) (m := y); intro H.
+    right. rewrite H. discriminate.
+    left; assumption.
+    right. rewrite H. discriminate.
+  Defined.
+
+  Definition Z_le_dec : {x <= y} + {~ x <= y}.
+  Proof.
+    unfold Zle in |- *.
+    apply Zcompare_rec with (n := x) (m := y); intro H.
+    left. rewrite H. discriminate.
+    left. rewrite H. discriminate.
+    right. tauto.
+  Defined.
+  
+  Definition Z_gt_dec : {x > y} + {~ x > y}.
+  Proof.
+    unfold Zgt in |- *.
+    apply Zcompare_rec with (n := x) (m := y); intro H.
+    right. rewrite H. discriminate.
+    right. rewrite H. discriminate.
+    left; assumption.
+  Defined.
+
+  Definition Z_ge_dec : {x >= y} + {~ x >= y}.
+  Proof.
+    unfold Zge in |- *.
+    apply Zcompare_rec with (n := x) (m := y); intro H.
+    left. rewrite H. discriminate.
+    right. tauto.
+    left. rewrite H. discriminate.
+  Defined.
+
+  Definition Z_lt_ge_dec : {x < y} + {x >= y}.
+  Proof.
+    exact Z_lt_dec.
+  Defined.
+
+  Lemma Z_lt_le_dec : {x < y} + {y <= x}.
+  Proof.
+    intros.
+    elim Z_lt_ge_dec.
+    intros; left; assumption.
+    intros; right; apply Zge_le; assumption.
+  Qed.
+
+  Definition Z_le_gt_dec : {x <= y} + {x > y}.
+  Proof.
+    elim Z_le_dec; auto with arith.
+    intro. right. apply Znot_le_gt; auto with arith.
+  Defined.
+
+  Definition Z_gt_le_dec : {x > y} + {x <= y}.
+  Proof.
+    exact Z_gt_dec.
+  Defined.
+
+  Definition Z_ge_lt_dec : {x >= y} + {x < y}.
+  Proof.
+    elim Z_ge_dec; auto with arith.
+    intro. right. apply Znot_ge_lt; auto with arith.
+  Defined.
+
+  Definition Z_le_lt_eq_dec : x <= y -> {x < y} + {x = y}.
+  Proof.
+    intro H.
+    apply Zcompare_rec with (n := x) (m := y).
+    intro. right. elim (Zcompare_Eq_iff_eq x y); auto with arith.
+    intro. left. elim (Zcompare_Eq_iff_eq x y); auto with arith.
+    intro H1. absurd (x > y); auto with arith.
+  Defined.
 
 End decidability.
 
-(** Cotransitivity of order on binary integers *)
+(** * Cotransitivity of order on binary integers *)
 
 Lemma Zlt_cotrans : forall n m:Z, n < m -> forall p:Z, {n < p} + {p < m}.
 Proof.
- intros x y H z.
- case (Z_lt_ge_dec x z).
- intro.
- left.
- assumption.
- intro.
- right.
- apply Zle_lt_trans with (m := x).
- apply Zge_le.
- assumption.
- assumption.
+  intros x y H z.
+  case (Z_lt_ge_dec x z).
+  intro.
+  left.
+  assumption.
+  intro.
+  right.
+  apply Zle_lt_trans with (m := x).
+  apply Zge_le.
+  assumption.
+  assumption.
 Defined.
 
 Lemma Zlt_cotrans_pos : forall n m:Z, 0 < n + m -> {0 < n} + {0 < m}.
 Proof.
- intros x y H.
- case (Zlt_cotrans 0 (x + y) H x).
- intro.
- left.
- assumption.
- intro.
- right.
- apply Zplus_lt_reg_l with (p := x).
- rewrite Zplus_0_r.
- assumption.
+  intros x y H.
+  case (Zlt_cotrans 0 (x + y) H x).
+  intro.
+  left.
+  assumption.
+  intro.
+  right.
+  apply Zplus_lt_reg_l with (p := x).
+  rewrite Zplus_0_r.
+  assumption.
 Defined.
 
 Lemma Zlt_cotrans_neg : forall n m:Z, n + m < 0 -> {n < 0} + {m < 0}.
 Proof.
- intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy;
-  [ right; apply Zplus_lt_reg_l with (p := x); rewrite Zplus_0_r | left ];
-  assumption.
+  intros x y H; case (Zlt_cotrans (x + y) 0 H x); intro Hxy;
+    [ right; apply Zplus_lt_reg_l with (p := x); rewrite Zplus_0_r | left ];
+    assumption.
 Defined.
 
 Lemma not_Zeq_inf : forall n m:Z, n <> m -> {n < m} + {m < n}.
 Proof.
- intros x y H.
- case Z_lt_ge_dec with x y.
- intro.
- left.
- assumption.
- intro H0.
- generalize (Zge_le _ _ H0).
- intro.
- case (Z_le_lt_eq_dec _ _ H1).
- intro.
- right.
- assumption.
- intro.
- apply False_rec.
- apply H.
- symmetry  in |- *.
- assumption.
+  intros x y H.
+  case Z_lt_ge_dec with x y.
+  intro.
+  left.
+  assumption.
+  intro H0.
+  generalize (Zge_le _ _ H0).
+  intro.
+  case (Z_le_lt_eq_dec _ _ H1).
+  intro.
+  right.
+  assumption.
+  intro.
+  apply False_rec.
+  apply H.
+  symmetry  in |- *.
+  assumption.
 Defined.
 
 Lemma Z_dec : forall n m:Z, {n < m} + {n > m} + {n = m}.
 Proof.
- intros x y.
- case (Z_lt_ge_dec x y).
- intro H.
- left.
- left.
- assumption.
- intro H.
- generalize (Zge_le _ _ H).
- intro H0.
- case (Z_le_lt_eq_dec y x H0).
- intro H1.
- left.
- right.
- apply Zlt_gt.
- assumption.
- intro.
- right.
- symmetry  in |- *.
- assumption.
+  intros x y.
+  case (Z_lt_ge_dec x y).
+  intro H.
+  left.
+  left.
+  assumption.
+  intro H.
+  generalize (Zge_le _ _ H).
+  intro H0.
+  case (Z_le_lt_eq_dec y x H0).
+  intro H1.
+  left.
+  right.
+  apply Zlt_gt.
+  assumption.
+  intro.
+  right.
+  symmetry  in |- *.
+  assumption.
 Defined.
 
 
 Lemma Z_dec' : forall n m:Z, {n < m} + {m < n} + {n = m}.
 Proof.
- intros x y.
- case (Z_eq_dec x y); intro H;
-  [ right; assumption | left; apply (not_Zeq_inf _ _ H) ].
+  intros x y.
+  case (Z_eq_dec x y); intro H;
+    [ right; assumption | left; apply (not_Zeq_inf _ _ H) ].
 Defined.
 
 
 
 Definition Z_zerop : forall x:Z, {x = 0} + {x <> 0}.
 Proof.
-exact (fun x:Z => Z_eq_dec x 0).
+  exact (fun x:Z => Z_eq_dec x 0).
 Defined.
 
 Definition Z_notzerop (x:Z) := sumbool_not _ _ (Z_zerop x).
 
-Definition Z_noteq_dec (x y:Z) := sumbool_not _ _ (Z_eq_dec x y).
\ No newline at end of file
+Definition Z_noteq_dec (x y:Z) := sumbool_not _ _ (Z_eq_dec x y).