Numbers : also axiomatize constants 1 and 2.

 Initially, I was using notation 1 := (S 0) and so on. But then, when
 implementing by NArith or ZArith, some lemmas statements were filled
 with Nsucc's and Zsucc's instead of 1 and 2's.

 Concerning BigN, things are rather complicated: zero, one, two
 aren't inlined during the functor application creating BigN.
 This is deliberate, at least for the other operations like BigN.add.
 And anyway, since zero, one, two are defined too early in NMake,
 we don't have 0%bigN in the body of BigN.zero but something complex that
 reduce to 0%bigN, same for one and two. Fortunately, apply or
 rewrite of generic lemmas seem to work, even if there's BigZ.zero
 on one side and 0 on the other...

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

5 files changed, 25 insertions, 30 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v
index eb27e63782..b5ca908b40 100644
--- a/theories/Numbers/Integer/Abstract/ZAddOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v
@@ -102,6 +102,11 @@ Proof.
 intro n. rewrite (opp_le_mono 0 n). now rewrite opp_0.
 Qed.
 
+Theorem lt_m1_0 : -(1) < 0.
+Proof.
+apply opp_neg_pos, lt_0_1.
+Qed.
+
 Theorem sub_lt_mono_l : forall n m p, n < m <-> p - m < p - n.
 Proof.
 intros n m p. do 2 rewrite <- add_opp_r. rewrite <- add_lt_mono_l.
diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v
index 540e17cb40..23eac0e699 100644
--- a/theories/Numbers/Integer/Abstract/ZLt.v
+++ b/theories/Numbers/Integer/Abstract/ZLt.v
@@ -125,7 +125,7 @@ Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -(1).
 Proof.
 intros n m H1 H2. apply -> lt_le_pred in H2.
 setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m.
-apply <- eq_opp_r. now rewrite opp_pred, opp_0.
+apply <- eq_opp_r. now rewrite one_succ, opp_pred, opp_0.
 Qed.
 
 End ZOrderProp.
diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v
index 76428584d7..25989b2d40 100644
--- a/theories/Numbers/Integer/Abstract/ZMulOrder.v
+++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v
@@ -177,22 +177,16 @@ Qed.
 
 Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1.
 Proof.
-assert (F : ~ 1 < -1).
-intro H.
-assert (H1 : -1 < 0). apply <- opp_neg_pos. apply lt_succ_diag_r.
-assert (H2 : 1 < 0) by now apply lt_trans with (-1).
-false_hyp H2 nlt_succ_diag_l.
+assert (F := lt_m1_0).
 zero_pos_neg n.
-intros m H; rewrite mul_0_l in H; false_hyp H neq_succ_diag_r.
-intros n H; split; apply <- le_succ_l in H; le_elim H.
-intros m H1; apply (lt_1_mul_l n m) in H.
-rewrite H1 in H; destruct H as [H | [H | H]].
-false_hyp H F. false_hyp H neq_succ_diag_l. false_hyp H lt_irrefl.
-intros; now left.
-intros m H1; apply (lt_1_mul_l n m) in H. rewrite mul_opp_l in H1;
-apply -> eq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]].
-false_hyp H lt_irrefl. apply -> eq_opp_l in H. rewrite opp_0 in H.
-false_hyp H neq_succ_diag_l. false_hyp H F.
+(* n = 0 *)
+intros m. nzsimpl. now left.
+(* 0 < n, proving P n /\ P (-n) *)
+intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn.
+le_elim Hn; split; intros m H.
+destruct (lt_1_mul_l n m) as [|[|]]; order'.
+rewrite mul_opp_l, eq_opp_l in H. destruct (lt_1_mul_l n m) as [|[|]]; order'.
+now left.
 intros; right; symmetry; now apply opp_wd.
 Qed.
 
diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v
index 1ababfe5c8..4c752043c7 100644
--- a/theories/Numbers/Integer/Abstract/ZParity.v
+++ b/theories/Numbers/Integer/Abstract/ZParity.v
@@ -41,20 +41,20 @@ Proof.
  intros x.
  split; intros [(y,H)|(y,H)].
  right. exists y. rewrite H. now nzsimpl.
- left. exists (S y). rewrite H. now nzsimpl.
+ left. exists (S y). rewrite H. now nzsimpl'.
  right. exists (P y). rewrite <- succ_inj_wd. rewrite H.
-  nzsimpl. now rewrite <- add_succ_l, <- add_succ_r, succ_pred.
+  nzsimpl'. now rewrite <- add_succ_l, <- add_succ_r, succ_pred.
  left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl.
 Qed.
 
 Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1.
 Proof.
- intros. nzsimpl. apply lt_succ_r. now apply add_le_mono.
+ intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono.
 Qed.
 
 Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m.
 Proof.
- intros. nzsimpl.
+ intros. nzsimpl'.
  rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r.
  apply add_le_mono; now apply le_succ_l.
 Qed.
@@ -95,7 +95,7 @@ Qed.
 
 Lemma odd_1 : odd 1 = true.
 Proof.
- rewrite odd_spec. exists 0. now nzsimpl.
+ rewrite odd_spec. exists 0. now nzsimpl'.
 Qed.
 
 Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n.
@@ -140,7 +140,7 @@ Proof.
  exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm.
  exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc.
  exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0.
- exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1.
+ exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1.
 Qed.
 
 Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m).
diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v
index 9de681375d..782a110240 100644
--- a/theories/Numbers/Integer/Abstract/ZPow.v
+++ b/theories/Numbers/Integer/Abstract/ZPow.v
@@ -78,12 +78,10 @@ Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b.
 Proof.
  intros a b (c,H). rewrite H.
  destruct (le_gt_cases 0 c).
- assert (0 <= 2) by (apply le_le_succ_r, le_0_1).
- rewrite 2 pow_mul_r; trivial.
+ rewrite 2 pow_mul_r by order'.
  rewrite 2 pow_2_r.
  now rewrite mul_opp_opp.
- assert (2*c < 0).
-  apply mul_pos_neg; trivial. rewrite lt_succ_r. apply le_0_1.
+ assert (2*c < 0) by (apply mul_pos_neg; order').
  now rewrite !pow_neg.
 Qed.
 
@@ -91,10 +89,8 @@ Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b).
 Proof.
  intros a b (c,H). rewrite H.
  destruct (le_gt_cases 0 c) as [LE|GT].
- assert (0 <= 2*c).
-  apply mul_nonneg_nonneg; trivial.
-  apply le_le_succ_r, le_0_1.
- rewrite add_succ_r, add_0_r, !pow_succ_r; trivial.
+ assert (0 <= 2*c) by (apply mul_nonneg_nonneg; order').
+ rewrite add_1_r, !pow_succ_r; trivial.
  rewrite pow_opp_even by (now exists c).
  apply mul_opp_l.
  apply double_above in GT. rewrite mul_0_r in GT.