diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NOrder.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NOrder.v | 43 |
1 files changed, 22 insertions, 21 deletions
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v index 17dd3466..8bba7d72 100644 --- a/theories/Numbers/Natural/Abstract/NOrder.v +++ b/theories/Numbers/Natural/Abstract/NOrder.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,18 +8,16 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Export NAdd. -Module NOrderPropFunct (Import N : NAxiomsSig'). -Include NAddPropFunct N. +Module NOrderProp (Import N : NAxiomsMiniSig'). +Include NAddProp N. (* Theorems that are true for natural numbers but not for integers *) Theorem lt_wf_0 : well_founded lt. Proof. -setoid_replace lt with (fun n m => 0 <= n /\ n < m). +setoid_replace lt with (fun n m => 0 <= n < m). apply lt_wf. intros x y; split. intro H; split; [apply le_0_l | assumption]. now intros [_ H]. @@ -29,12 +27,12 @@ Defined. Theorem nlt_0_r : forall n, ~ n < 0. Proof. -intro n; apply -> le_ngt. apply le_0_l. +intro n; apply le_ngt. apply le_0_l. Qed. Theorem nle_succ_0 : forall n, ~ (S n <= 0). Proof. -intros n H; apply -> le_succ_l in H; false_hyp H nlt_0_r. +intros n H; apply le_succ_l in H; false_hyp H nlt_0_r. Qed. Theorem le_0_r : forall n, n <= 0 <-> n == 0. @@ -65,6 +63,7 @@ Qed. Theorem zero_one : forall n, n == 0 \/ n == 1 \/ 1 < n. Proof. +setoid_rewrite one_succ. induct n. now left. cases n. intros; right; now left. intros n IH. destruct IH as [H | [H | H]]. @@ -75,6 +74,7 @@ Qed. Theorem lt_1_r : forall n, n < 1 <-> n == 0. Proof. +setoid_rewrite one_succ. cases n. split; intro; [reflexivity | apply lt_succ_diag_r]. intros n. rewrite <- succ_lt_mono. @@ -83,6 +83,7 @@ Qed. Theorem le_1_r : forall n, n <= 1 <-> n == 0 \/ n == 1. Proof. +setoid_rewrite one_succ. cases n. split; intro; [now left | apply le_succ_diag_r]. intro n. rewrite <- succ_le_mono, le_0_r, succ_inj_wd. @@ -117,9 +118,9 @@ Proof. intros Base Step; induct n. intros; apply Base. intros n IH m H. elim H using le_ind. -solve_predicate_wd. +solve_proper. apply Step; [| apply IH]; now apply eq_le_incl. -intros k H1 H2. apply -> le_succ_l in H1. apply lt_le_incl in H1. auto. +intros k H1 H2. apply le_succ_l in H1. apply lt_le_incl in H1. auto. Qed. Theorem lt_ind_rel : @@ -131,7 +132,7 @@ intros Base Step; induct n. intros m H. apply lt_exists_pred in H; destruct H as [m' [H _]]. rewrite H; apply Base. intros n IH m H. elim H using lt_ind. -solve_predicate_wd. +solve_proper. apply Step; [| apply IH]; now apply lt_succ_diag_r. intros k H1 H2. apply lt_succ_l in H1. auto. Qed. @@ -175,7 +176,7 @@ Theorem lt_le_pred : forall n m, n < m -> n <= P m. Proof. intro n; cases m. intro H; false_hyp H nlt_0_r. -intros m IH. rewrite pred_succ; now apply -> lt_succ_r. +intros m IH. rewrite pred_succ; now apply lt_succ_r. Qed. Theorem lt_pred_le : forall n m, P n < m -> n <= m. @@ -183,7 +184,7 @@ Theorem lt_pred_le : forall n m, P n < m -> n <= m. Proof. intros n m; cases n. rewrite pred_0; intro H; now apply lt_le_incl. -intros n IH. rewrite pred_succ in IH. now apply <- le_succ_l. +intros n IH. rewrite pred_succ in IH. now apply le_succ_l. Qed. Theorem lt_pred_lt : forall n m, n < P m -> n < m. @@ -200,7 +201,7 @@ Theorem pred_le_mono : forall n m, n <= m -> P n <= P m. (* Converse is false for n == 1, m == 0 *) Proof. intros n m H; elim H using le_ind_rel. -solve_relation_wd. +solve_proper. intro; rewrite pred_0; apply le_0_l. intros p q H1 _; now do 2 rewrite pred_succ. Qed. @@ -208,12 +209,12 @@ Qed. Theorem pred_lt_mono : forall n m, n ~= 0 -> (n < m <-> P n < P m). Proof. intros n m H1; split; intro H2. -assert (m ~= 0). apply <- neq_0_lt_0. now apply lt_lt_0 with n. +assert (m ~= 0). apply neq_0_lt_0. now apply lt_lt_0 with n. now rewrite <- (succ_pred n) in H2; rewrite <- (succ_pred m) in H2 ; -[apply <- succ_lt_mono | | |]. -assert (m ~= 0). apply <- neq_0_lt_0. apply lt_lt_0 with (P n). +[apply succ_lt_mono | | |]. +assert (m ~= 0). apply neq_0_lt_0. apply lt_lt_0 with (P n). apply lt_le_trans with (P m). assumption. apply le_pred_l. -apply -> succ_lt_mono in H2. now do 2 rewrite succ_pred in H2. +apply succ_lt_mono in H2. now do 2 rewrite succ_pred in H2. Qed. Theorem lt_succ_lt_pred : forall n m, S n < m <-> n < P m. @@ -224,13 +225,13 @@ Qed. Theorem le_succ_le_pred : forall n m, S n <= m -> n <= P m. (* Converse is false for n == m == 0 *) Proof. -intros n m H. apply lt_le_pred. now apply -> le_succ_l. +intros n m H. apply lt_le_pred. now apply le_succ_l. Qed. Theorem lt_pred_lt_succ : forall n m, P n < m -> n < S m. (* Converse is false for n == m == 0 *) Proof. -intros n m H. apply <- lt_succ_r. now apply lt_pred_le. +intros n m H. apply lt_succ_r. now apply lt_pred_le. Qed. Theorem le_pred_le_succ : forall n m, P n <= m <-> n <= S m. @@ -240,5 +241,5 @@ rewrite pred_0. split; intro H; apply le_0_l. intro n. rewrite pred_succ. apply succ_le_mono. Qed. -End NOrderPropFunct. +End NOrderProp. |