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

12 files changed, 83 insertions, 35 deletions

diff --git a/theories/Numbers/Natural/Abstract/NAdd.v b/theories/Numbers/Natural/Abstract/NAdd.v
index 96d60c9979..fbe71a4c70 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 e9ec6a823e..7ed563be5e 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 c1bac7165a..8d11b5ce33 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 f6c6ad5428..6ecdef9ef0 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 fa855f2105..2816af7c47 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 e815f9ee6a..bd65886867 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.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index ef4ac7c457..0f04869c09 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -68,6 +68,7 @@ Arguments Scope BigN.gcd [bigN_scope bigN_scope].
 
 Local Notation "0" := BigN.zero : bigN_scope. (* temporary notation *)
 Local Notation "1" := BigN.one : bigN_scope. (* temporary notation *)
+Local Notation "2" := BigN.two : bigN_scope. (* temporary notation *)
 Infix "+" := BigN.add : bigN_scope.
 Infix "-" := BigN.sub : bigN_scope.
 Infix "*" := BigN.mul : bigN_scope.
@@ -164,6 +165,7 @@ Ltac isBigNcst t :=
    end
  | BigN.zero => constr:true
  | BigN.one => constr:true
+ | BigN.two => constr:true
  | _ => constr:false
  end.
 
@@ -194,7 +196,6 @@ Add Ring BigNr : BigNring
   div BigNdiv).
 
 Section TestRing.
-Local Notation "2" := (BigN.N0 2%int31) : bigN_scope. (* temporary notation *)
 Let test : forall x y, 1 + x*y^1 + x^2 + 1 == 1*1 + 1 + y*x + 1*x*x.
 intros. ring_simplify. reflexivity.
 Qed.
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 6697d59c3b..9e6e4b6092 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -71,7 +71,7 @@ Module Make (W0:CyclicType) <: NType.
 
  Definition to_N (x : t) := Zabs_N (to_Z x).
 
- (** * Zero and One *)
+ (** * Zero, One *)
 
  Definition zero := mk_t O ZnZ.zero.
  Definition one := mk_t O ZnZ.one.
@@ -115,6 +115,18 @@ Module Make (W0:CyclicType) <: NType.
   rewrite spec_mk_t_S. simpl. rewrite ZnZ.spec_1. assumption.
  Qed.
 
+ (** Two *)
+
+ (** Not really pretty, but since W0 might be Z/2Z, we're not sure
+     there's a proper 2 there. *)
+
+ Definition two := succ one.
+
+ Lemma spec_2 : [two] = 2.
+ Proof.
+  unfold two. now rewrite spec_succ, spec_1.
+ Qed.
+
  (** * Addition *)
 
  Local Notation addn := (fun n =>
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 65b166df60..d1217d407e 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -46,6 +46,16 @@ Definition sub_succ_r := Nminus_succ_r.
 Definition mul_0_l := Nmult_0_l.
 Definition mul_succ_l n m := eq_trans (Nmult_Sn_m n m) (Nplus_comm _ _).
 
+Lemma one_succ : 1 = Nsucc 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma two_succ : 2 = Nsucc 1.
+Proof.
+reflexivity.
+Qed.
+
 (** Order *)
 
 Program Instance lt_wd : Proper (eq==>eq==>iff) Nlt.
@@ -165,7 +175,9 @@ Definition eq := @eq N.
 Definition eqb := Neqb.
 Definition compare := Ncompare.
 Definition eq_dec := N_eq_dec.
-Definition zero := N0.
+Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
 Definition succ := Nsucc.
 Definition pred := Npred.
 Definition add := Nplus.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 5bb26d04f2..bbf4f5cd7b 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -163,6 +163,16 @@ Proof.
 reflexivity.
 Qed.
 
+Theorem one_succ : 1 = S 0.
+Proof.
+reflexivity.
+Qed.
+
+Theorem two_succ : 2 = S 1.
+Proof.
+reflexivity.
+Qed.
+
 Theorem add_0_l : forall n : nat, 0 + n = n.
 Proof.
 reflexivity.
@@ -259,6 +269,8 @@ Definition eq := @eq nat.
 Definition eqb := beq_nat.
 Definition compare := nat_compare.
 Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
 Definition succ := S.
 Definition pred := pred.
 Definition add := plus.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 3ff2ded62d..7cf3e7046b 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSig.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSig.v
@@ -40,6 +40,7 @@ Module Type NType.
  Parameter min : t -> t -> t.
  Parameter zero : t.
  Parameter one : t.
+ Parameter two : t.
  Parameter succ : t -> t.
  Parameter pred : t -> t.
  Parameter add  : t -> t -> t.
@@ -66,6 +67,7 @@ Module Type NType.
  Parameter spec_min : forall x y, [min x y] = Zmin [x] [y].
  Parameter spec_0: [zero] = 0.
  Parameter spec_1: [one] = 1.
+ Parameter spec_2: [two] = 2.
  Parameter spec_succ: forall n, [succ n] = [n] + 1.
  Parameter spec_add: forall x y, [add x y] = [x] + [y].
  Parameter spec_pred: forall x, [pred x] = Zmax 0 ([x] - 1).
@@ -94,6 +96,8 @@ Module Type NType_Notation (Import N:NType).
  Notation "[ x ]" := (to_Z x).
  Infix "==" := eq (at level 70).
  Notation "0" := zero.
+ Notation "1" := one.
+ Notation "2" := two.
  Infix "+" := add.
  Infix "-" := sub.
  Infix "*" := mul.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 568ebeae86..e1dc5349bc 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -13,7 +13,7 @@ Require Import ZArith Nnat NAxioms NDiv NSig.
 Module NTypeIsNAxioms (Import N : NType').
 
 Hint Rewrite
- spec_0 spec_1 spec_succ spec_add spec_mul spec_pred spec_sub
+ spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub
  spec_div spec_modulo spec_gcd spec_compare spec_eq_bool
  spec_max spec_min spec_pow_pos spec_pow_N spec_pow spec_even spec_odd
  : nsimpl.
@@ -37,6 +37,16 @@ Proof.
 intros. zify. generalize (spec_pos n); omega with *.
 Qed.
 
+Theorem one_succ : 1 == succ 0.
+Proof.
+now zify.
+Qed.
+
+Theorem two_succ : 2 == succ 1.
+Proof.
+now zify.
+Qed.
+
 Definition N_of_Z z := of_N (Zabs_N z).
 
 Section Induction.
@@ -181,9 +191,6 @@ Qed.
 
 Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
 
-Local Notation "1" := (succ 0).
-Local Notation "2" := (succ 1).
-
 Lemma pow_0_r : forall a, a^0 == 1.
 Proof.
  intros. now zify.