diff options
Diffstat (limited to 'theories/ZArith/Zorder.v')
| -rw-r--r-- | theories/ZArith/Zorder.v | 66 |
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). |