From d3cf0e074d4b4a3ddc1de4c91a235474eead80aa Mon Sep 17 00:00:00 2001 From: emakarov Date: Thu, 15 Nov 2007 13:30:39 +0000 Subject: Split NTimesOrder into properly NTimesOrder and NPlusOrder. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10324 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Numbers/Natural/Abstract/NPlusOrder.v | 114 +++++++++++++++++++++++++ 1 file changed, 114 insertions(+) create mode 100644 theories/Numbers/Natural/Abstract/NPlusOrder.v (limited to 'theories/Numbers/Natural') diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v new file mode 100644 index 000000000..f459e8dd6 --- /dev/null +++ b/theories/Numbers/Natural/Abstract/NPlusOrder.v @@ -0,0 +1,114 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* p + n < p + m. +Proof NZplus_lt_mono_l. + +Theorem plus_lt_mono_r : forall n m p : N, n < m <-> n + p < m + p. +Proof NZplus_lt_mono_r. + +Theorem plus_lt_mono : forall n m p q : N, n < m -> p < q -> n + p < m + q. +Proof NZplus_lt_mono. + +Theorem plus_le_mono_l : forall n m p : N, n <= m <-> p + n <= p + m. +Proof NZplus_le_mono_l. + +Theorem plus_le_mono_r : forall n m p : N, n <= m <-> n + p <= m + p. +Proof NZplus_le_mono_r. + +Theorem plus_le_mono : forall n m p q : N, n <= m -> p <= q -> n + p <= m + q. +Proof NZplus_le_mono. + +Theorem plus_lt_le_mono : forall n m p q : N, n < m -> p <= q -> n + p < m + q. +Proof NZplus_lt_le_mono. + +Theorem plus_le_lt_mono : forall n m p q : N, n <= m -> p < q -> n + p < m + q. +Proof NZplus_le_lt_mono. + +Theorem plus_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n + m. +Proof NZplus_pos_pos. + +Theorem lt_plus_pos_l : forall n m : N, 0 < n -> m < n + m. +Proof NZlt_plus_pos_l. + +Theorem lt_plus_pos_r : forall n m : N, 0 < n -> m < m + n. +Proof NZlt_plus_pos_r. + +Theorem le_lt_plus_lt : forall n m p q : N, n <= m -> p + m < q + n -> p < q. +Proof NZle_lt_plus_lt. + +Theorem lt_le_plus_lt : forall n m p q : N, n < m -> p + m <= q + n -> p < q. +Proof NZlt_le_plus_lt. + +Theorem le_le_plus_le : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q. +Proof NZle_le_plus_le. + +Theorem plus_lt_cases : forall n m p q : N, n + m < p + q -> n < p \/ m < q. +Proof NZplus_lt_cases. + +Theorem plus_le_cases : forall n m p q : N, n + m <= p + q -> n <= p \/ m <= q. +Proof NZplus_le_cases. + +Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m. +Proof NZplus_pos_cases. + +(** Theorems true for natural numbers *) + +Theorem le_plus_r : forall n m : N, n <= n + m. +Proof. +intro n; induct m. +rewrite plus_0_r; now apply eq_le_incl. +intros m IH. rewrite plus_succ_r; now apply le_le_succ_r. +Qed. + +Theorem lt_lt_plus_r : forall n m p : N, n < m -> n < m + p. +Proof. +intros n m p H; rewrite <- (plus_0_r n). +apply plus_lt_le_mono; [assumption | apply le_0_l]. +Qed. + +Theorem lt_lt_plus_l : forall n m p : N, n < m -> n < p + m. +Proof. +intros n m p; rewrite plus_comm; apply lt_lt_plus_r. +Qed. + +Theorem plus_pos_l : forall n m : N, 0 < n -> 0 < n + m. +Proof. +intros; apply NZplus_pos_nonneg. assumption. apply le_0_l. +Qed. + +Theorem plus_pos_r : forall n m : N, 0 < m -> 0 < n + m. +Proof. +intros; apply NZplus_nonneg_pos. apply le_0_l. assumption. +Qed. + +(* The following property is used to prove the correctness of the +definition of order on integers constructed from pairs of natural numbers *) + +Theorem plus_lt_repl_pair : forall n m n' m' u v : N, + n + u < m + v -> n + m' == n' + m -> n' + u < m' + v. +Proof. +intros n m n' m' u v H1 H2. +symmetry in H2. assert (H3 : n' + m <= n + m') by now apply eq_le_incl. +pose proof (plus_lt_le_mono _ _ _ _ H1 H3) as H4. +rewrite (plus_shuffle2 n u), (plus_shuffle1 m v), (plus_comm m n) in H4. +do 2 rewrite <- plus_assoc in H4. do 2 apply <- plus_lt_mono_l in H4. +now rewrite (plus_comm n' u), (plus_comm m' v). +Qed. + +End NPlusOrderPropFunct. \ No newline at end of file -- cgit v1.2.3