Some lemmas about dependent choice + extensions of Compare_dec +

synonyms in Le.v, Lt.v, Gt.v.

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

4 files changed, 55 insertions, 19 deletions

diff --git a/theories/Arith/Compare_dec.v b/theories/Arith/Compare_dec.v
index 1dc74af73..deb6f229b 100644
--- a/theories/Arith/Compare_dec.v
+++ b/theories/Arith/Compare_dec.v
@@ -56,27 +56,47 @@ Definition le_lt_eq_dec n m : n <= m -> {n < m} + {n = m}.
   intros; absurd (m < n); auto with arith.
 Defined.
 
+Theorem le_dec : forall n m, {n <= m} + {~ n <= m}.
+Proof.
+  intros x y; elim (le_gt_dec x y);
+    [ auto with arith | intro; right; apply gt_not_le; assumption ].
+Qed.
+
+Theorem lt_dec : forall n m, {n < m} + {~ n < m}.
+Proof.
+  intros; apply le_dec.
+Qed.
+
+Theorem gt_dec : forall n m, {n > m} + {~ n > m}.
+Proof.
+  intros; apply lt_dec.
+Qed.
+
+Theorem ge_dec : forall n m, {n >= m} + {~ n >= m}.
+Proof.
+  intros; apply le_dec.
+Qed.
+
 (** Proofs of decidability *)
 
 Theorem dec_le : forall n m, decidable (n <= m).
 Proof.
-  intros x y; unfold decidable in |- *; elim (le_gt_dec x y);
-    [ auto with arith | intro; right; apply gt_not_le; assumption ].
+  intros x y; destruct (le_dec x y); unfold decidable; auto.
 Qed.
 
 Theorem dec_lt : forall n m, decidable (n < m).
 Proof.
-  intros x y; unfold lt in |- *; apply dec_le.
+  intros; apply dec_le.
 Qed.
 
 Theorem dec_gt : forall n m, decidable (n > m).
 Proof.
-  intros x y; unfold gt in |- *; apply dec_lt.
+  intros; apply dec_lt.
 Qed.
 
 Theorem dec_ge : forall n m, decidable (n >= m).
 Proof.
-  intros x y; unfold ge in |- *; apply dec_le.
+  intros; apply dec_le.
 Qed.
 
 Theorem not_eq : forall n m, n <> m -> n < m \/ m < n.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index c2ed678cb..70169f52a 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -135,7 +135,7 @@ Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
 
 (** * Comparison to 0 *)
 
-Theorem gt_O_eq : forall n, n > 0 \/ 0 = n.
+Theorem gt_0_eq : forall n, n > 0 \/ 0 = n.
 Proof.
   intro n; apply gt_S; auto with arith.
 Qed.
@@ -151,4 +151,8 @@ Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m.
 Proof.
   auto with arith.
 Qed.
-Hint Resolve plus_gt_compat_l: arith v62.
\ No newline at end of file
+Hint Resolve plus_gt_compat_l: arith v62.
+
+(* begin hide *)
+Notation gt_O_eq := gt_0_eq (only parsing).
+(* end hide *)
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index 1c00d7ec9..d85178dea 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -41,25 +41,25 @@ Hint Resolve le_trans: arith v62.
 
 (** Comparison to 0 *)
 
-Theorem le_O_n : forall n, 0 <= n.
+Theorem le_0_n : forall n, 0 <= n.
 Proof.
   induction n; auto.
 Qed.
 
-Theorem le_Sn_O : forall n, ~ S n <= 0.
+Theorem le_Sn_0 : forall n, ~ S n <= 0.
 Proof.
   red in |- *; intros n H.
   change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith.
 Qed.
 
-Hint Resolve le_O_n le_Sn_O: arith v62.
+Hint Resolve le_0_n le_Sn_0: arith v62.
 
-Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n.
+Theorem le_n_0_eq : forall n, n <= 0 -> 0 = n.
 Proof.
   induction n; auto with arith.
-  intro; contradiction le_Sn_O with n.
+  intro; contradiction le_Sn_0 with n.
 Qed.
-Hint Immediate le_n_O_eq: arith v62.
+Hint Immediate le_n_0_eq: arith v62.
 
 
 (** [le] and successor *)
@@ -135,3 +135,9 @@ Proof.
   intros m Le.
   elim Le; auto with arith.
 Qed.
+
+(* begin hide *)
+Notation le_O_n := le_0_n (only parsing).
+Notation le_Sn_O := le_Sn_0 (only parsing).
+Notation le_n_O_eq := le_n_0_eq (only parsing).
+(* end hide *)
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index bdd7ce092..af435e54b 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -90,11 +90,11 @@ Proof.
 Qed.
 Hint Immediate lt_S_n: arith v62.
 
-Theorem lt_O_Sn : forall n, 0 < S n.
+Theorem lt_0_Sn : forall n, 0 < S n.
 Proof.
   auto with arith.
 Qed.
-Hint Resolve lt_O_Sn: arith v62.
+Hint Resolve lt_0_Sn: arith v62.
 
 Theorem lt_n_O : forall n, ~ n < 0.
 Proof le_Sn_O.
@@ -175,15 +175,21 @@ Qed.
 
 (** * Comparison to 0 *)
 
-Theorem neq_O_lt : forall n, 0 <> n -> 0 < n.
+Theorem neq_0_lt : forall n, 0 <> n -> 0 < n.
 Proof.
   induction n; auto with arith.
   intros; absurd (0 = 0); trivial with arith.
 Qed.
-Hint Immediate neq_O_lt: arith v62.
+Hint Immediate neq_0_lt: arith v62.
 
-Theorem lt_O_neq : forall n, 0 < n -> 0 <> n.
+Theorem lt_0_neq : forall n, 0 < n -> 0 <> n.
 Proof.
   induction 1; auto with arith.
 Qed.
-Hint Immediate lt_O_neq: arith v62.
\ No newline at end of file
+Hint Immediate lt_0_neq: arith v62.
+
+(* begin hide *)
+Notation lt_O_Sn := lt_0_Sn (only parsing).
+Notation neq_O_lt := neq_0_lt (only parsing).
+Notation lt_O_neq := lt_0_neq (only parsing).
+(* end hide *)