summaryrefslogtreecommitdiff
path: root/theories/ZArith/Zorder.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-21 09:46:51 +0200
commit5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (patch)
tree631ad791a7685edafeb1fb2e8faeedc8379318ae /theories/ZArith/Zorder.v
parentda178a880e3ace820b41d38b191d3785b82991f5 (diff)
Imported Upstream snapshot 8.3~beta0+13298
Diffstat (limited to 'theories/ZArith/Zorder.v')
-rw-r--r--theories/ZArith/Zorder.v66
1 files changed, 38 insertions, 28 deletions
diff --git a/theories/ZArith/Zorder.v b/theories/ZArith/Zorder.v
index 73808f92..511c364b 100644
--- a/theories/ZArith/Zorder.v
+++ b/theories/ZArith/Zorder.v
@@ -1,3 +1,4 @@
+(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
@@ -5,9 +6,9 @@
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: Zorder.v 12888 2010-03-28 19:35:03Z herbelin $ i*)
+(*i $Id$ i*)
-(** Binary Integers (Pierre Crégut (CNET, Lannion, France) *)
+(** Binary Integers (Pierre Crégut, CNET, Lannion, France) *)
Require Import BinPos.
Require Import BinInt.
@@ -49,7 +50,7 @@ Proof.
[ tauto
| intros H3; right; unfold not in |- *; intros H4; elim H3; rewrite (H2 H4);
intros H5; discriminate H5 ].
-Qed.
+Qed.
Theorem dec_Zne : forall n m:Z, decidable (Zne n m).
Proof.
@@ -79,7 +80,7 @@ Proof.
intros x y; unfold decidable, Zge in |- *; elim (x ?= y);
[ left; discriminate
| right; unfold not in |- *; intros H; apply H; trivial with arith
- | left; discriminate ].
+ | left; discriminate ].
Qed.
Theorem dec_Zlt : forall n m:Z, decidable (n < m).
@@ -96,7 +97,7 @@ Proof.
| unfold Zlt in |- *; intros H; elim H; intros H1;
[ auto with arith
| right; elim (Zcompare_Gt_Lt_antisym x y); auto with arith ] ].
-Qed.
+Qed.
(** * Relating strict and large orders *)
@@ -180,7 +181,7 @@ Proof.
intros x y. split. intro. apply Zgt_lt. assumption.
intro. apply Zlt_gt. assumption.
Qed.
-
+
(** * Equivalence and order properties *)
(** Reflexivity *)
@@ -188,7 +189,7 @@ Qed.
Lemma Zle_refl : forall n:Z, n <= n.
Proof.
intros n; unfold Zle in |- *; rewrite (Zcompare_refl n); discriminate.
-Qed.
+Qed.
Lemma Zeq_le : forall n m:Z, n = m -> n <= m.
Proof.
@@ -201,7 +202,7 @@ Hint Resolve Zle_refl: zarith.
Lemma Zle_antisym : forall n m:Z, n <= m -> m <= n -> n = m.
Proof.
- intros n m H1 H2; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]].
+ intros n m H1 H2; destruct (Ztrichotomy n m) as [Hlt| [Heq| Hgt]].
absurd (m > n); [ apply Zle_not_gt | apply Zlt_gt ]; assumption.
assumption.
absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption.
@@ -256,6 +257,13 @@ Proof.
| absurd (n > m); [ apply Zle_not_gt | idtac ]; assumption ].
Qed.
+Lemma Zle_lt_or_eq_iff : forall n m, n <= m <-> n < m \/ n = m.
+Proof.
+ unfold Zle, Zlt. intros.
+ generalize (Zcompare_Eq_iff_eq n m).
+ destruct (n ?= m); intuition; discriminate.
+Qed.
+
(** Dichotomy *)
Lemma Zle_or_lt : forall n m:Z, n <= m \/ m < n.
@@ -276,8 +284,7 @@ Qed.
Lemma Zlt_trans : forall n m p:Z, n < m -> m < p -> n < p.
Proof.
- intros n m p H1 H2; apply Zgt_lt; apply Zgt_trans with (m := m); apply Zlt_gt;
- assumption.
+ exact Zcompare_Lt_trans.
Qed.
(** Mixed transitivity *)
@@ -400,13 +407,13 @@ Qed.
Lemma Zgt_le_succ : forall n m:Z, m > n -> Zsucc n <= m.
Proof.
unfold Zgt, Zle in |- *; intros n p H; elim (Zcompare_Gt_not_Lt p n);
- intros H1 H2; unfold not in |- *; intros H3; unfold not in H1;
+ intros H1 H2; unfold not in |- *; intros H3; unfold not in H1;
apply H1;
[ assumption
| elim (Zcompare_Gt_Lt_antisym (n + 1) p); intros H4 H5; apply H4; exact H3 ].
Qed.
-Lemma Zlt_gt_succ : forall n m:Z, n <= m -> Zsucc m > n.
+Lemma Zle_gt_succ : forall n m:Z, n <= m -> Zsucc m > n.
Proof.
intros n p H; apply Zgt_le_trans with p.
apply Zgt_succ.
@@ -415,7 +422,7 @@ Qed.
Lemma Zle_lt_succ : forall n m:Z, n <= m -> n < Zsucc m.
Proof.
- intros n m H; apply Zgt_lt; apply Zlt_gt_succ; assumption.
+ intros n m H; apply Zgt_lt; apply Zle_gt_succ; assumption.
Qed.
Lemma Zlt_le_succ : forall n m:Z, n < m -> Zsucc n <= m.
@@ -433,12 +440,17 @@ Proof.
intros n m H; apply Zgt_succ_le; apply Zlt_gt; assumption.
Qed.
-Lemma Zlt_succ_gt : forall n m:Z, Zsucc n <= m -> m > n.
+Lemma Zle_succ_gt : forall n m:Z, Zsucc n <= m -> m > n.
Proof.
intros n m H; apply Zle_gt_trans with (m := Zsucc n);
[ assumption | apply Zgt_succ ].
Qed.
+Lemma Zlt_succ_r : forall n m, n < Zsucc m <-> n <= m.
+Proof.
+ split; [apply Zlt_succ_le | apply Zle_lt_succ].
+Qed.
+
(** Weakening order *)
Lemma Zle_succ : forall n:Z, n <= Zsucc n.
@@ -478,9 +490,9 @@ Hint Resolve Zle_le_succ: zarith.
Lemma Zgt_succ_pred : forall n m:Z, m > Zsucc n -> Zpred m > n.
Proof.
unfold Zgt, Zsucc, Zpred in |- *; intros n p H;
- rewrite <- (fun x y => Zcompare_plus_compat x y 1);
+ rewrite <- (fun x y => Zcompare_plus_compat x y 1);
rewrite (Zplus_comm p); rewrite Zplus_assoc;
- rewrite (fun x => Zplus_comm x n); simpl in |- *;
+ rewrite (fun x => Zplus_comm x n); simpl in |- *;
assumption.
Qed.
@@ -563,7 +575,7 @@ Proof.
assert (Hle : m <= n).
apply Zgt_succ_le; assumption.
destruct (Zle_lt_or_eq _ _ Hle) as [Hlt| Heq].
- left; apply Zlt_gt; assumption.
+ left; apply Zlt_gt; assumption.
right; assumption.
Qed.
@@ -680,7 +692,7 @@ Proof.
rewrite (Zplus_comm p n); rewrite (Zplus_comm p m); trivial.
Qed.
-(** ** Multiplication *)
+(** ** Multiplication *)
(** Compatibility of multiplication by a positive wrt to order *)
Lemma Zmult_le_compat_r : forall n m p:Z, n <= m -> 0 <= p -> n * p <= m * p.
@@ -777,7 +789,7 @@ Proof.
intros a b c d H0 H1 H2 H3.
apply Zge_trans with (a * d).
apply Zmult_ge_compat_l; trivial.
- apply Zge_trans with c; trivial.
+ apply Zge_trans with c; trivial.
apply Zmult_ge_compat_r; trivial.
Qed.
@@ -965,17 +977,17 @@ Qed.
Lemma Zeq_plus_swap : forall n m p:Z, n + p = m <-> n = m - p.
Proof.
- intros x y z; intros. split. intro. apply Zplus_minus_eq. symmetry in |- *. rewrite Zplus_comm.
+ intros x y z; intros. split. intro. apply Zplus_minus_eq. symmetry in |- *. rewrite Zplus_comm.
assumption.
- intro. rewrite H. unfold Zminus in |- *. rewrite Zplus_assoc_reverse.
+ intro. rewrite H. unfold Zminus in |- *. rewrite Zplus_assoc_reverse.
rewrite Zplus_opp_l. apply Zplus_0_r.
Qed.
Lemma Zlt_minus_simpl_swap : forall n m:Z, 0 < m -> n - m < n.
Proof.
intros n m H; apply Zplus_lt_reg_l with (p := m); rewrite Zplus_minus;
- pattern n at 1 in |- *; rewrite <- (Zplus_0_r n);
- rewrite (Zplus_comm m n); apply Zplus_lt_compat_l;
+ pattern n at 1 in |- *; rewrite <- (Zplus_0_r n);
+ rewrite (Zplus_comm m n); apply Zplus_lt_compat_l;
assumption.
Qed.
@@ -993,8 +1005,8 @@ Qed.
Lemma Zle_minus_le_0 : forall n m:Z, m <= n -> 0 <= n - m.
Proof.
- intros n m H; unfold Zminus; apply Zplus_le_reg_r with (p := m);
- rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H.
+ intros n m H; unfold Zminus; apply Zplus_le_reg_r with (p := m);
+ rewrite <- Zplus_assoc; rewrite Zplus_opp_l; rewrite Zplus_0_r; exact H.
Qed.
Lemma Zmult_lt_compat:
@@ -1012,7 +1024,7 @@ Proof.
rewrite <- H5; simpl; apply Zmult_lt_0_compat; auto with zarith.
Qed.
-Lemma Zmult_lt_compat2:
+Lemma Zmult_lt_compat2:
forall n m p q : Z, 0 < n <= p -> 0 < m < q -> n * m < p * q.
Proof.
intros n m p q (H1, H2) (H3, H4).
@@ -1025,5 +1037,3 @@ Qed.
(** For compatibility *)
Notation Zlt_O_minus_lt := Zlt_0_minus_lt (only parsing).
-Notation Zle_gt_succ := Zlt_gt_succ (only parsing).
-Notation Zle_succ_gt := Zlt_succ_gt (only parsing).