diff options
Diffstat (limited to 'theories/Arith/Lt.v')
| -rw-r--r-- | theories/Arith/Lt.v | 77 |
1 files changed, 42 insertions, 35 deletions
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v index eeb4e35e..94cf3793 100644 --- a/theories/Arith/Lt.v +++ b/theories/Arith/Lt.v @@ -6,86 +6,93 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Lt.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Lt.v 9245 2006-10-17 12:53:34Z notin $ i*) + +(** Theorems about [lt] in nat. [lt] is defined in library [Init/Peano.v] as: +<< +Definition lt (n m:nat) := S n <= m. +Infix "<" := lt : nat_scope. +>> +*) Require Import Le. Open Local Scope nat_scope. Implicit Types m n p : nat. -(** Irreflexivity *) +(** * Irreflexivity *) Theorem lt_irrefl : forall n, ~ n < n. Proof le_Sn_n. Hint Resolve lt_irrefl: arith v62. -(** Relationship between [le] and [lt] *) +(** * Relationship between [le] and [lt] *) Theorem lt_le_S : forall n m, n < m -> S n <= m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate lt_le_S: arith v62. Theorem lt_n_Sm_le : forall n m, n < S m -> n <= m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate lt_n_Sm_le: arith v62. Theorem le_lt_n_Sm : forall n m, n <= m -> n < S m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate le_lt_n_Sm: arith v62. Theorem le_not_lt : forall n m, n <= m -> ~ m < n. Proof. -induction 1; auto with arith. + induction 1; auto with arith. Qed. Theorem lt_not_le : forall n m, n < m -> ~ m <= n. Proof. -red in |- *; intros n m Lt Le; exact (le_not_lt m n Le Lt). + red in |- *; intros n m Lt Le; exact (le_not_lt m n Le Lt). Qed. Hint Immediate le_not_lt lt_not_le: arith v62. -(** Asymmetry *) +(** * Asymmetry *) Theorem lt_asym : forall n m, n < m -> ~ m < n. Proof. -induction 1; auto with arith. + induction 1; auto with arith. Qed. -(** Order and successor *) +(** * Order and successor *) Theorem lt_n_Sn : forall n, n < S n. Proof. -auto with arith. + auto with arith. Qed. Hint Resolve lt_n_Sn: arith v62. Theorem lt_S : forall n m, n < m -> n < S m. Proof. -auto with arith. + auto with arith. Qed. Hint Resolve lt_S: arith v62. Theorem lt_n_S : forall n m, n < m -> S n < S m. Proof. -auto with arith. + auto with arith. Qed. Hint Resolve lt_n_S: arith v62. Theorem lt_S_n : forall n m, S n < S m -> n < m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate lt_S_n: arith v62. Theorem lt_O_Sn : forall n, 0 < S n. Proof. -auto with arith. + auto with arith. Qed. Hint Resolve lt_O_Sn: arith v62. @@ -93,7 +100,7 @@ Theorem lt_n_O : forall n, ~ n < 0. Proof le_Sn_O. Hint Resolve lt_n_O: arith v62. -(** Predecessor *) +(** * Predecessor *) Lemma S_pred : forall n m, m < n -> n = S (pred n). Proof. @@ -111,65 +118,65 @@ destruct 1; simpl in |- *; auto with arith. Qed. Hint Resolve lt_pred_n_n: arith v62. -(** Transitivity properties *) +(** * Transitivity properties *) Theorem lt_trans : forall n m p, n < m -> m < p -> n < p. Proof. -induction 2; auto with arith. + induction 2; auto with arith. Qed. Theorem lt_le_trans : forall n m p, n < m -> m <= p -> n < p. Proof. -induction 2; auto with arith. + induction 2; auto with arith. Qed. Theorem le_lt_trans : forall n m p, n <= m -> m < p -> n < p. Proof. -induction 2; auto with arith. + induction 2; auto with arith. Qed. Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62. -(** Large = strict or equal *) +(** * Large = strict or equal *) Theorem le_lt_or_eq : forall n m, n <= m -> n < m \/ n = m. Proof. -induction 1; auto with arith. + induction 1; auto with arith. Qed. Theorem lt_le_weak : forall n m, n < m -> n <= m. Proof. -auto with arith. + auto with arith. Qed. Hint Immediate lt_le_weak: arith v62. -(** Dichotomy *) +(** * Dichotomy *) Theorem le_or_lt : forall n m, n <= m \/ m < n. Proof. -intros n m; pattern n, m in |- *; apply nat_double_ind; auto with arith. -induction 1; auto with arith. + intros n m; pattern n, m in |- *; apply nat_double_ind; auto with arith. + induction 1; auto with arith. Qed. Theorem nat_total_order : forall n m, n <> m -> n < m \/ m < n. Proof. -intros m n diff. -elim (le_or_lt n m); [ intro H'0 | auto with arith ]. -elim (le_lt_or_eq n m); auto with arith. -intro H'; elim diff; auto with arith. + intros m n diff. + elim (le_or_lt n m); [ intro H'0 | auto with arith ]. + elim (le_lt_or_eq n m); auto with arith. + intro H'; elim diff; auto with arith. Qed. -(** Comparison to 0 *) +(** * Comparison to 0 *) Theorem neq_O_lt : forall n, 0 <> n -> 0 < n. Proof. -induction n; auto with arith. -intros; absurd (0 = 0); trivial with arith. + induction n; auto with arith. + intros; absurd (0 = 0); trivial with arith. Qed. Hint Immediate neq_O_lt: arith v62. Theorem lt_O_neq : forall n, 0 < n -> 0 <> n. Proof. -induction 1; auto with arith. + induction 1; auto with arith. Qed. Hint Immediate lt_O_neq: arith v62.
\ No newline at end of file |