diff options
Diffstat (limited to 'theories/Arith/Le.v')
| -rw-r--r-- | theories/Arith/Le.v | 110 |
1 files changed, 63 insertions, 47 deletions
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v index e95ef408..e8b9e6be 100644 --- a/theories/Arith/Le.v +++ b/theories/Arith/Le.v @@ -6,108 +6,124 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Le.v 8642 2006-03-17 10:09:02Z notin $ i*) +(*i $Id: Le.v 9245 2006-10-17 12:53:34Z notin $ i*) + +(** Order on natural numbers. [le] is defined in [Init/Peano.v] as: +<< +Inductive le (n:nat) : nat -> Prop := + | le_n : n <= n + | le_S : forall m:nat, n <= m -> n <= S m + +where "n <= m" := (le n m) : nat_scope. +>> + *) -(** Order on natural numbers *) Open Local Scope nat_scope. Implicit Types m n p : nat. -(** Reflexivity *) +(** * [le] is a pre-order *) +(** Reflexivity *) Theorem le_refl : forall n, n <= n. Proof. -exact le_n. + exact le_n. Qed. (** Transitivity *) - Theorem le_trans : forall n m p, n <= m -> m <= p -> n <= p. Proof. induction 2; auto. Qed. Hint Resolve le_trans: arith v62. -(** Order, successor and predecessor *) +(** * Properties of [le] w.r.t. successor, predecessor and 0 *) -Theorem le_n_S : forall n m, n <= m -> S n <= S m. +(** Comparison to 0 *) + +Theorem le_O_n : forall n, 0 <= n. Proof. - induction 1; auto. + induction n; auto. Qed. -Theorem le_n_Sn : forall n, n <= S n. +Theorem le_Sn_O : forall n, ~ S n <= 0. Proof. - auto. + red in |- *; intros n H. + change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith. Qed. -Theorem le_O_n : forall n, 0 <= n. +Hint Resolve le_O_n le_Sn_O: arith v62. + +Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n. Proof. - induction n; auto. + induction n; auto with arith. + intro; contradiction le_Sn_O with n. Qed. +Hint Immediate le_n_O_eq: arith v62. -Hint Resolve le_n_S le_n_Sn le_O_n le_n_S: arith v62. -Theorem le_pred_n : forall n, pred n <= n. +(** [le] and successor *) + +Theorem le_n_S : forall n m, n <= m -> S n <= S m. Proof. -induction n; auto with arith. + induction 1; auto. Qed. -Hint Resolve le_pred_n: arith v62. + +Theorem le_n_Sn : forall n, n <= S n. +Proof. + auto. +Qed. + +Hint Resolve le_n_S le_n_Sn : arith v62. Theorem le_Sn_le : forall n m, S n <= m -> n <= m. Proof. -intros n m H; apply le_trans with (S n); auto with arith. + intros n m H; apply le_trans with (S n); auto with arith. Qed. Hint Immediate le_Sn_le: arith v62. Theorem le_S_n : forall n m, S n <= S m -> n <= m. Proof. -intros n m H; change (pred (S n) <= pred (S m)) in |- *. -destruct H; simpl; auto with arith. + intros n m H; change (pred (S n) <= pred (S m)) in |- *. + destruct H; simpl; auto with arith. Qed. Hint Immediate le_S_n: arith v62. -Theorem le_pred : forall n m, n <= m -> pred n <= pred m. +Theorem le_Sn_n : forall n, ~ S n <= n. Proof. -destruct n; simpl; auto with arith. -destruct m; simpl; auto with arith. + induction n; auto with arith. Qed. +Hint Resolve le_Sn_n: arith v62. -(** Comparison to 0 *) +(** [le] and predecessor *) -Theorem le_Sn_O : forall n, ~ S n <= 0. +Theorem le_pred_n : forall n, pred n <= n. Proof. -red in |- *; intros n H. -change (IsSucc 0) in |- *; elim H; simpl in |- *; auto with arith. + induction n; auto with arith. Qed. -Hint Resolve le_Sn_O: arith v62. +Hint Resolve le_pred_n: arith v62. -Theorem le_n_O_eq : forall n, n <= 0 -> 0 = n. +Theorem le_pred : forall n m, n <= m -> pred n <= pred m. Proof. -induction n; auto with arith. -intro; contradiction le_Sn_O with n. + destruct n; simpl; auto with arith. + destruct m; simpl; auto with arith. Qed. -Hint Immediate le_n_O_eq: arith v62. -(** Negative properties *) - -Theorem le_Sn_n : forall n, ~ S n <= n. -Proof. -induction n; auto with arith. -Qed. -Hint Resolve le_Sn_n: arith v62. +(** * [le] is a order on [nat] *) (** Antisymmetry *) Theorem le_antisym : forall n m, n <= m -> m <= n -> n = m. Proof. -intros n m h; destruct h as [| m0 H]; auto with arith. -intros H1. -absurd (S m0 <= m0); auto with arith. -apply le_trans with n; auto with arith. + intros n m H; destruct H as [|m' H]; auto with arith. + intros H1. + absurd (S m' <= m'); auto with arith. + apply le_trans with n; auto with arith. Qed. Hint Immediate le_antisym: arith v62. -(** A different elimination principle for the order on natural numbers *) + +(** * A different elimination principle for the order on natural numbers *) Lemma le_elim_rel : forall P:nat -> nat -> Prop, @@ -115,7 +131,7 @@ Lemma le_elim_rel : (forall p (q:nat), p <= q -> P p q -> P (S p) (S q)) -> forall n m, n <= m -> P n m. Proof. -induction n; auto with arith. -intros m Le. -elim Le; auto with arith. -Qed.
\ No newline at end of file + induction n; auto with arith. + intros m Le. + elim Le; auto with arith. +Qed. |