diff options
Diffstat (limited to 'theories/Arith/Gt.v')
| -rw-r--r-- | theories/Arith/Gt.v | 133 |
1 files changed, 62 insertions, 71 deletions
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v index afd146e7..e406ff0d 100644 --- a/theories/Arith/Gt.v +++ b/theories/Arith/Gt.v @@ -1,154 +1,145 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(** Theorems about [gt] in [nat]. [gt] is defined in [Init/Peano.v] as: +(** Theorems about [gt] in [nat]. + + This file is DEPRECATED now, see module [PeanoNat.Nat] instead, + which favor [lt] over [gt]. + + [gt] is defined in [Init/Peano.v] as: << Definition gt (n m:nat) := m < n. >> *) -Require Import Le. -Require Import Lt. -Require Import Plus. +Require Import PeanoNat Le Lt Plus. Local Open Scope nat_scope. -Implicit Types m n p : nat. - (** * Order and successor *) -Theorem gt_Sn_O : forall n, S n > 0. -Proof. - auto with arith. -Qed. -Hint Resolve gt_Sn_O: arith v62. +Theorem gt_Sn_O n : S n > 0. +Proof Nat.lt_0_succ _. -Theorem gt_Sn_n : forall n, S n > n. -Proof. - auto with arith. -Qed. -Hint Resolve gt_Sn_n: arith v62. +Theorem gt_Sn_n n : S n > n. +Proof Nat.lt_succ_diag_r _. -Theorem gt_n_S : forall n m, n > m -> S n > S m. +Theorem gt_n_S n m : n > m -> S n > S m. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Resolve gt_n_S: arith v62. -Lemma gt_S_n : forall n m, S m > S n -> m > n. +Lemma gt_S_n n m : S m > S n -> m > n. Proof. - auto with arith. + apply Nat.succ_lt_mono. Qed. -Hint Immediate gt_S_n: arith v62. -Theorem gt_S : forall n m, S n > m -> n > m \/ m = n. +Theorem gt_S n m : S n > m -> n > m \/ m = n. Proof. - intros n m H; unfold gt; apply le_lt_or_eq; auto with arith. + intro. now apply Nat.lt_eq_cases, Nat.succ_le_mono. Qed. -Lemma gt_pred : forall n m, m > S n -> pred m > n. +Lemma gt_pred n m : m > S n -> pred m > n. Proof. - auto with arith. + apply Nat.lt_succ_lt_pred. Qed. -Hint Immediate gt_pred: arith v62. (** * Irreflexivity *) -Lemma gt_irrefl : forall n, ~ n > n. -Proof lt_irrefl. -Hint Resolve gt_irrefl: arith v62. +Lemma gt_irrefl n : ~ n > n. +Proof Nat.lt_irrefl _. (** * Asymmetry *) -Lemma gt_asym : forall n m, n > m -> ~ m > n. -Proof fun n m => lt_asym m n. - -Hint Resolve gt_asym: arith v62. +Lemma gt_asym n m : n > m -> ~ m > n. +Proof Nat.lt_asymm _ _. (** * Relating strict and large orders *) -Lemma le_not_gt : forall n m, n <= m -> ~ n > m. -Proof le_not_lt. -Hint Resolve le_not_gt: arith v62. - -Lemma gt_not_le : forall n m, n > m -> ~ n <= m. +Lemma le_not_gt n m : n <= m -> ~ n > m. Proof. -auto with arith. + apply Nat.le_ngt. Qed. -Hint Resolve gt_not_le: arith v62. +Lemma gt_not_le n m : n > m -> ~ n <= m. +Proof. + apply Nat.lt_nge. +Qed. -Theorem le_S_gt : forall n m, S n <= m -> m > n. +Theorem le_S_gt n m : S n <= m -> m > n. Proof. - auto with arith. + apply Nat.le_succ_l. Qed. -Hint Immediate le_S_gt: arith v62. -Lemma gt_S_le : forall n m, S m > n -> n <= m. +Lemma gt_S_le n m : S m > n -> n <= m. Proof. - intros n p; exact (lt_n_Sm_le n p). + apply Nat.succ_le_mono. Qed. -Hint Immediate gt_S_le: arith v62. -Lemma gt_le_S : forall n m, m > n -> S n <= m. +Lemma gt_le_S n m : m > n -> S n <= m. Proof. - auto with arith. + apply Nat.le_succ_l. Qed. -Hint Resolve gt_le_S: arith v62. -Lemma le_gt_S : forall n m, n <= m -> S m > n. +Lemma le_gt_S n m : n <= m -> S m > n. Proof. - auto with arith. + apply Nat.succ_le_mono. Qed. -Hint Resolve le_gt_S: arith v62. (** * Transitivity *) -Theorem le_gt_trans : forall n m p, m <= n -> m > p -> n > p. +Theorem le_gt_trans n m p : m <= n -> m > p -> n > p. Proof. - red; intros; apply lt_le_trans with m; auto with arith. + intros. now apply Nat.lt_le_trans with m. Qed. -Theorem gt_le_trans : forall n m p, n > m -> p <= m -> n > p. +Theorem gt_le_trans n m p : n > m -> p <= m -> n > p. Proof. - red; intros; apply le_lt_trans with m; auto with arith. + intros. now apply Nat.le_lt_trans with m. Qed. -Lemma gt_trans : forall n m p, n > m -> m > p -> n > p. +Lemma gt_trans n m p : n > m -> m > p -> n > p. Proof. - red; intros n m p H1 H2. - apply lt_trans with m; auto with arith. + intros. now apply Nat.lt_trans with m. Qed. -Theorem gt_trans_S : forall n m p, S n > m -> m > p -> n > p. +Theorem gt_trans_S n m p : S n > m -> m > p -> n > p. Proof. - red; intros; apply lt_le_trans with m; auto with arith. + intros. apply Nat.lt_le_trans with m; trivial. now apply Nat.succ_le_mono. Qed. -Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. - (** * Comparison to 0 *) -Theorem gt_0_eq : forall n, n > 0 \/ 0 = n. +Theorem gt_0_eq n : n > 0 \/ 0 = n. Proof. - intro n; apply gt_S; auto with arith. + destruct n; [now right | left; apply Nat.lt_0_succ]. Qed. (** * Simplification and compatibility *) -Lemma plus_gt_reg_l : forall n m p, p + n > p + m -> n > m. +Lemma plus_gt_reg_l n m p : p + n > p + m -> n > m. Proof. - red; intros n m p H; apply plus_lt_reg_l with p; auto with arith. + apply Nat.add_lt_mono_l. Qed. -Lemma plus_gt_compat_l : forall n m p, n > m -> p + n > p + m. +Lemma plus_gt_compat_l n m p : n > m -> p + n > p + m. Proof. - auto with arith. + apply Nat.add_lt_mono_l. Qed. + +(** * Hints *) + +Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith v62. +Hint Immediate gt_S_n gt_pred : arith v62. +Hint Resolve gt_irrefl gt_asym : arith v62. +Hint Resolve le_not_gt gt_not_le : arith v62. +Hint Immediate le_S_gt gt_S_le : arith v62. +Hint Resolve gt_le_S le_gt_S : arith v62. +Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62. Hint Resolve plus_gt_compat_l: arith v62. (* begin hide *) |