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

6 files changed, 28 insertions, 28 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 96d60c997..fbe71a4c7 100644
--- a/theories/Numbers/Natural/Abstract/NAdd.v
+++ b/theories/Numbers/Natural/Abstract/NAdd.v
@@ -45,7 +45,7 @@ Qed.
 Theorem eq_add_1 : forall n m,
   n + m == 1 -> n == 1 /\ m == 0 \/ n == 0 /\ m == 1.
 Proof.
-intros n m H.
+intros n m. rewrite one_succ. intro H.
 assert (H1 : exists p, n + m == S p) by now exists 0.
 apply -> eq_add_succ in H1. destruct H1 as [[n' H1] | [m' H1]].
 left. rewrite H1 in H; rewrite add_succ_l in H; apply succ_inj in H.
diff --git a/theories/Numbers/Natural/Abstract/NBase.v b/theories/Numbers/Natural/Abstract/NBase.v
index e9ec6a823..7ed563be5 100644
--- a/theories/Numbers/Natural/Abstract/NBase.v
+++ b/theories/Numbers/Natural/Abstract/NBase.v
@@ -94,12 +94,11 @@ Qed.
 Theorem eq_pred_0 : forall n, P n == 0 <-> n == 0 \/ n == 1.
 Proof.
 cases n.
-rewrite pred_0. setoid_replace (0 == 1) with False using relation iff. tauto.
-split; intro H; [symmetry in H; false_hyp H neq_succ_0 | elim H].
+rewrite pred_0. now split; [left|].
 intro n. rewrite pred_succ.
-setoid_replace (S n == 0) with False using relation iff by
-  (apply -> neg_false; apply neq_succ_0).
-rewrite succ_inj_wd. tauto.
+split. intros H; right. now rewrite H, one_succ.
+intros [H|H]. elim (neq_succ_0 _ H).
+apply succ_inj_wd. now rewrite <- one_succ.
 Qed.
 
 Theorem succ_pred : forall n, n ~= 0 -> S (P n) == n.
@@ -130,6 +129,7 @@ Theorem pair_induction :
   A 0 -> A 1 ->
     (forall n, A n -> A (S n) -> A (S (S n))) -> forall n, A n.
 Proof.
+rewrite one_succ.
 intros until 3.
 assert (D : forall n, A n /\ A (S n)); [ |intro n; exact (proj1 (D n))].
 induct n; [ | intros n [IH1 IH2]]; auto.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index c1bac7165..8d11b5ce3 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -308,7 +308,7 @@ Qed.
 
 Theorem half_1 : half 1 == 0.
 Proof.
-unfold half. rewrite half_aux_succ, half_aux_0; simpl; auto with *.
+unfold half. rewrite one_succ, half_aux_succ, half_aux_0; simpl; auto with *.
 Qed.
 
 Theorem half_double : forall n,
@@ -346,9 +346,8 @@ assert (LE : 0 <= half n) by apply le_0_l.
 le_elim LE; auto.
 destruct (half_double n) as [E|E];
  rewrite <- LE, mul_0_r, ?add_0_r in E; rewrite E in LT.
-destruct (nlt_0_r _ LT).
-rewrite <- succ_lt_mono in LT.
-destruct (nlt_0_r _ LT).
+order'.
+order.
 Qed.
 
 Theorem half_decrease : forall n, 0 < n -> half n < n.
@@ -359,11 +358,11 @@ destruct (half_double n) as [E|E]; rewrite E at 2;
 rewrite <- add_0_l at 1.
 rewrite <- add_lt_mono_r.
 assert (LE : 0 <= half n) by apply le_0_l.
-le_elim LE; auto.
+nzsimpl. le_elim LE; auto.
 rewrite <- LE, mul_0_r in E. rewrite E in LT. destruct (nlt_0_r _ LT).
 rewrite <- add_0_l at 1.
 rewrite <- add_lt_mono_r.
-rewrite add_succ_l. apply lt_0_succ.
+nzsimpl. apply lt_0_succ.
 Qed.
 
 
@@ -437,7 +436,7 @@ destruct (n<<2) as [ ]_eqn:H.
 auto with *.
 apply succ_wd, E, half_decrease.
 rewrite <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
-apply lt_succ_l; auto.
+order'.
 Qed.
 Hint Resolve log_good_step.
 
@@ -468,7 +467,7 @@ intros n IH k Hk1 Hk2.
 destruct (lt_ge_cases k 2) as [LT|LE].
 (* base *)
 rewrite log_init, pow_0 by auto.
-rewrite <- le_succ_l in Hk2.
+rewrite <- le_succ_l, <- one_succ in Hk2.
 le_elim Hk2.
 rewrite <- nle_gt, le_succ_l in LT. destruct LT; auto.
 rewrite <- Hk2.
diff --git a/theories/Numbers/Natural/Abstract/NMulOrder.v b/theories/Numbers/Natural/Abstract/NMulOrder.v
index f6c6ad542..6ecdef9ef 100644
--- a/theories/Numbers/Natural/Abstract/NMulOrder.v
+++ b/theories/Numbers/Natural/Abstract/NMulOrder.v
@@ -65,10 +65,10 @@ Proof.
 intros n m.
 split; [| intros [H1 H2]; now rewrite H1, H2, mul_1_l].
 intro H; destruct (lt_trichotomy n 1) as [H1 | [H1 | H1]].
-apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. false_hyp H neq_0_succ.
+apply -> lt_1_r in H1. rewrite H1, mul_0_l in H. order'.
 rewrite H1, mul_1_l in H; now split.
 destruct (eq_0_gt_0_cases m) as [H2 | H2].
-rewrite H2, mul_0_r in H; false_hyp H neq_0_succ.
+rewrite H2, mul_0_r in H. order'.
 apply -> (mul_lt_mono_pos_r m) in H1; [| assumption]. rewrite mul_1_l in H1.
 assert (H3 : 1 < n * m) by now apply (lt_1_l m).
 rewrite H in H3; false_hyp H3 lt_irrefl.
diff --git a/theories/Numbers/Natural/Abstract/NOrder.v b/theories/Numbers/Natural/Abstract/NOrder.v
index fa855f210..2816af7c4 100644
--- a/theories/Numbers/Natural/Abstract/NOrder.v
+++ b/theories/Numbers/Natural/Abstract/NOrder.v
@@ -63,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]].
@@ -73,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.
@@ -81,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.
diff --git a/theories/Numbers/Natural/Abstract/NParity.v b/theories/Numbers/Natural/Abstract/NParity.v
index e815f9ee6..bd6588686 100644
--- a/theories/Numbers/Natural/Abstract/NParity.v
+++ b/theories/Numbers/Natural/Abstract/NParity.v
@@ -40,17 +40,17 @@ Proof.
  intros x.
  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'.
 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.
@@ -91,7 +91,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.
@@ -138,7 +138,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).
@@ -176,19 +176,17 @@ Proof.
  exists (n'-m'). now rewrite mul_sub_distr_l, Hn, Hm.
  exists (n'-m'-1).
   rewrite !mul_sub_distr_l, Hn, Hm, sub_add_distr, mul_1_r.
-  rewrite <- (add_1_l 1) at 5. rewrite sub_add_distr.
+  rewrite two_succ at 5. rewrite <- (add_1_l 1). rewrite sub_add_distr.
   symmetry. apply sub_add.
   apply le_add_le_sub_l.
-  rewrite add_1_l, <- (mul_1_r 2) at 1.
-  rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l.
-  rewrite le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r.
+  rewrite add_1_l, <- two_succ, <- (mul_1_r 2) at 1.
+  rewrite <- mul_sub_distr_l. rewrite <- mul_le_mono_pos_l by order'.
+  rewrite one_succ, le_succ_l. rewrite <- lt_add_lt_sub_l, add_0_r.
   destruct (le_gt_cases n' m') as [LE|GT]; trivial.
   generalize (double_below _ _ LE). order.
-  apply lt_succ_r, le_0_1.
  exists (n'-m'). rewrite mul_sub_distr_l, Hn, Hm.
   apply add_sub_swap.
-  apply mul_le_mono_pos_l.
-  apply lt_succ_r, le_0_1.
+  apply mul_le_mono_pos_l; try order'.
   destruct (le_gt_cases m' n') as [LE|GT]; trivial.
   generalize (double_above _ _ GT). order.
  exists (n'-m'). rewrite Hm,Hn, mul_sub_distr_l.