Added transitivity and irreflexivity of <, as well as < -elimination for binary positive numbers.

Added directory contribs/micromega with the generalization of Frédéric Besson's micromega tactic for an arbitrary ordered ring. So far no tactic has been defined. One has to apply the theorems and find the certificate, which is necessary to solve inequations, manually.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10226 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 36 insertions, 100 deletions

diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index f62b5ecb2..7c2610ccc 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -25,6 +25,9 @@ Proof NZlt_le_incl.
 Theorem lt_neq : forall n m : N, n < m -> n ~= m.
 Proof NZlt_neq.
 
+Theorem lt_le_neq : forall n m : N, n < m <-> n <= m /\ n ~= m.
+Proof NZlt_le_neq.
+
 Theorem le_refl : forall n : N, n <= n.
 Proof NZle_refl.
 
diff --git a/theories/Numbers/Natural/Abstract/NPlusOrder.v b/theories/Numbers/Natural/Abstract/NPlusOrder.v
deleted file mode 100644
index c4640858e..000000000
--- a/theories/Numbers/Natural/Abstract/NPlusOrder.v
+++ /dev/null
@@ -1,87 +0,0 @@
-Require Export NPlus.
-Require Export NOrder.
-Require Import NZPlusOrder.
-
-Module NPlusOrderPropFunct
-  (Import NPlusMod : NPlusSig)
-  (Import NOrderMod : NOrderSig with Module NAxiomsMod := NPlusMod.NAxiomsMod).
-Module Export NPlusPropMod := NPlusPropFunct NPlusMod.
-Module Export NOrderPropMod := NOrderPropFunct NOrderMod.
-Module Export NZPlusOrderPropMod := NZPlusOrderPropFunct NZPlusMod NZOrderMod.
-Open Local Scope NatScope.
-
-(* Print All locks up here !!! *)
-Theorem lt_plus_trans : forall n m p, n < m -> n < m + p.
-Proof.
-intros n m p; induct p.
-now rewrite plus_0_r.
-intros x IH H.
-rewrite plus_succ_r. apply lt_closed_succ. apply IH; apply H.
-Qed.
-
-Theorem plus_lt_compat_l : forall n m p, n < m -> p + n < p + m.
-Proof.
-intros n m p H; induct p.
-do 2 rewrite plus_0_l; assumption.
-intros x IH. do 2 rewrite plus_succ_l. now apply <- lt_resp_succ.
-Qed.
-
-Theorem plus_lt_compat_r : forall n m p, n < m -> n + p < m + p.
-Proof.
-intros n m p H; rewrite plus_comm.
-set (k := p + n); rewrite plus_comm; unfold k; clear k.
-now apply plus_lt_compat_l.
-Qed.
-
-Theorem plus_lt_compat : forall n m p q, n < m -> p < q -> n + p < m + q.
-Proof.
-intros n m p q H1 H2.
-apply lt_trans with (m := m + p);
-[now apply plus_lt_compat_r | now apply plus_lt_compat_l].
-Qed.
-
-Theorem plus_lt_cancel_l : forall p n m, p + n < p + m <-> n < m.
-Proof.
-intros p n m; induct p.
-now do 2 rewrite plus_0_l.
-intros p IH.
-do 2 rewrite plus_succ_l. now rewrite lt_resp_succ.
-Qed.
-
-Theorem plus_lt_cancel_r : forall p n m, n + p < m + p <-> n < m.
-Proof.
-intros p n m;
-setoid_replace (n + p) with (p + n) by apply plus_comm;
-setoid_replace (m + p) with (p + m) by apply plus_comm;
-apply plus_lt_cancel_l.
-Qed.
-
-(* The following property is similar to plus_repl_pair in NPlus.v
-and 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 + u < m + v -> n + m' == n' + m -> n' + u < m' + v.
-Proof.
-intros n m n' m' u v H1 H2.
-apply <- (plus_lt_cancel_r (n + m')) in H1.
-set (k := n + m') in H1 at 2; rewrite H2 in H1; unfold k in H1; clear k.
-rewrite <- plus_assoc in H1.
-setoid_replace (m + v + (n + m')) with (n + m' + (m + v)) in H1 by apply plus_comm.
-rewrite <- plus_assoc in H1. apply -> plus_lt_cancel_l in H1.
-rewrite plus_assoc in H1. setoid_replace (m + v) with (v + m) in H1 by apply plus_comm.
-rewrite plus_assoc in H1. apply -> plus_lt_cancel_r in H1.
-now rewrite plus_comm in H1.
-Qed.
-
-Theorem plus_gt_succ :
-  forall n m p, S p < n + m -> (exists n', n == S n') \/ (exists m', m == S m').
-Proof.
-intros n m p H.
-apply <- lt_le_succ in H.
-apply lt_exists_pred in H. destruct H as [q H].
-now apply plus_eq_succ in H.
-Qed.
-
-End NPlusOrderProperties.
-
diff --git a/theories/Numbers/Natural/Abstract/NTimesOrder.v b/theories/Numbers/Natural/Abstract/NTimesOrder.v
index 2dbfd8f97..dc1b977aa 100644
--- a/theories/Numbers/Natural/Abstract/NTimesOrder.v
+++ b/theories/Numbers/Natural/Abstract/NTimesOrder.v
@@ -28,22 +28,31 @@ 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_lt : forall n m p q : N, n <= m -> p + m <= q + n -> p <= q.
-Proof NZle_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 : NZ, n + m <= p + q -> n <= p \/ m <= q.
+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 : NZ, 0 < n + m -> 0 < n \/ 0 < m.
+Theorem plus_pos_cases : forall n m : N, 0 < n + m -> 0 < n \/ 0 < m.
 Proof NZplus_pos_cases.
 
 (** Theorems true for natural numbers *)
@@ -55,17 +64,25 @@ rewrite plus_0_r; le_equal.
 intros m IH. rewrite plus_succ_r; now apply le_le_succ.
 Qed.
 
-Theorem lt_plus_r : forall n m : N, m ~= 0 -> n < n + m.
+Theorem lt_lt_plus_r : forall n m p : N, n < m -> n < m + p.
 Proof.
-intros n m; cases m.
-intro H; elimtype False; now apply H.
-intros. rewrite plus_succ_r. apply <- lt_succ_le. apply le_plus_r.
+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 : forall n m p : N, n < m -> n < m + p.
+Theorem lt_lt_plus_l : forall n m p : N, n < m -> n < p + m.
 Proof.
-intros n m p H; rewrite <- (plus_0_r n).
-apply plus_lt_le_mono; [assumption | apply le_0_l].
+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 similar to plus_repl_pair in NPlus.v
@@ -123,7 +140,7 @@ Proof.
 intros; apply NZtimes_le_mono; try assumption; apply le_0_l.
 Qed.
 
-Theorem times_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
+Theorem Ztimes_pos_pos : forall n m : N, 0 < n -> 0 < m -> 0 < n * m.
 Proof NZtimes_pos_pos.
 
 Theorem times_eq_0 : forall n m : N, n * m == 0 -> n == 0 \/ m == 0.
@@ -132,11 +149,14 @@ Proof NZtimes_eq_0.
 Theorem times_neq_0 : forall n m : N, n ~= 0 /\ m ~= 0 <-> n * m ~= 0.
 Proof NZtimes_neq_0.
 
+Theorem times_2_mono_l : forall n m : N, n < m -> 1 + (1 + 1) * n < (1 + 1) * m.
+Proof NZtimes_2_mono_l.
+
 Theorem times_pos : forall n m : N, n * m > 0 <-> n > 0 /\ m > 0.
 Proof.
 intros n m; split; [intro H | intros [H1 H2]].
 apply -> NZtimes_pos in H. destruct H as [[H1 H2] | [H1 H2]]. now split. false_hyp H1 nlt_0_r.
-now apply times_pos_pos.
+now apply NZtimes_pos_pos.
 Qed.
 
 End NTimesOrderPropFunct.