aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-05 15:13:09 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-05-05 15:13:09 +0000
commitf440fd9b2d0f3e1bb5cd0b86df4676a46be781db (patch)
tree3a189286d98b225d68fa06b7b60306ba863e5946
parentae700f63dfade2676e68944aa5076400883ec96c (diff)
Minimal lemmas about Z.gt, N.gt and co
The use of these predicate isn't recommended, but let's at least allow converting > >= and < <= git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14109 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--theories/NArith/BinNat.v44
-rw-r--r--theories/ZArith/BinInt.v35
2 files changed, 74 insertions, 5 deletions
diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 2e3b7c49d..779391ed1 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -922,6 +922,44 @@ Set Inline Level 30. (* For inlining only t eq zero one two *)
Include NProp
<+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+(** Otherwise N stays associated with abstract_scope : (TODO FIX) *)
+Bind Scope N_scope with N.
+
+(** In generic statements, the predicates [lt] and [le] have been
+ favored, whereas [gt] and [ge] don't even exist in the abstract
+ layers. The use of [gt] and [ge] is hence not recommended. We provide
+ here the bare minimal results to related them with [lt] and [le]. *)
+
+Lemma gt_lt n m : n > m -> m < n.
+Proof.
+ unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+Qed.
+
+Lemma lt_gt n m : n < m -> m > n.
+Proof.
+ unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+Qed.
+
+Lemma gt_lt_iff n m : n > m <-> m < n.
+Proof.
+ split. apply gt_lt. apply lt_gt.
+Qed.
+
+Lemma ge_le n m : n >= m -> m <= n.
+Proof.
+ unfold le, ge. intros H. contradict H. now apply gt_lt.
+Qed.
+
+Lemma le_ge n m : n <= m -> m >= n.
+Proof.
+ unfold le, ge. intros H. contradict H. now apply lt_gt.
+Qed.
+
+Lemma ge_le_iff n m : n >= m <-> m <= n.
+Proof.
+ split. apply ge_le. apply le_ge.
+Qed.
+
(** Auxiliary results about right shift on positive numbers,
used in BinInt *)
@@ -1092,6 +1130,7 @@ Notation Nlog2_nonpos := N.log2_nonpos (only parsing).
Notation Neven_spec := N.even_spec (only parsing).
Notation Nodd_spec := N.odd_spec (only parsing).
Notation Nlt_not_eq := N.lt_neq (only parsing).
+Notation Ngt_Nlt := N.gt_lt (only parsing).
(** More complex compatibility facts, expressed as lemmas
(to preserve scopes for instance) *)
@@ -1105,9 +1144,4 @@ Proof (N.mul_add_distr_l p n m).
Lemma Nmult_reg_r n m p : p <> 0 -> n * p = m * p -> n = m.
Proof (fun H => proj1 (N.mul_cancel_r n m p H)).
-Lemma Ngt_Nlt n m : n > m -> m < n.
-Proof.
-unfold Ngt, Nlt; intro H. now rewrite <- N.compare_antisym, H.
-Qed.
-
(** Not kept : Ncompare_n_Sm Nplus_lt_cancel_l *)
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v
index 62f5a0f78..04bb8d881 100644
--- a/theories/ZArith/BinInt.v
+++ b/theories/ZArith/BinInt.v
@@ -1286,6 +1286,41 @@ Include ZProp
(** Otherwise Z stays associated with abstract_scope : (TODO FIX) *)
Bind Scope Z_scope with Z.
+(** In generic statements, the predicates [lt] and [le] have been
+ favored, whereas [gt] and [ge] don't even exist in the abstract
+ layers. The use of [gt] and [ge] is hence not recommended. We provide
+ here the bare minimal results to related them with [lt] and [le]. *)
+
+Lemma gt_lt n m : n > m -> m < n.
+Proof.
+ unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+Qed.
+
+Lemma lt_gt n m : n < m -> m > n.
+Proof.
+ unfold lt, gt. intros H. now rewrite <- compare_antisym, H.
+Qed.
+
+Lemma gt_lt_iff n m : n > m <-> m < n.
+Proof.
+ split. apply gt_lt. apply lt_gt.
+Qed.
+
+Lemma ge_le n m : n >= m -> m <= n.
+Proof.
+ unfold le, ge. intros H. contradict H. now apply gt_lt.
+Qed.
+
+Lemma le_ge n m : n <= m -> m >= n.
+Proof.
+ unfold le, ge. intros H. contradict H. now apply lt_gt.
+Qed.
+
+Lemma ge_le_iff n m : n >= m <-> m <= n.
+Proof.
+ split. apply ge_le. apply le_ge.
+Qed.
+
(** TODO : to add in Numbers *)
Lemma add_shuffle3 n m p : n + (m + p) = m + (n + p).