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

11 files changed, 90 insertions, 47 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.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index 6c9dc77c10..92be49bdaf 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -70,6 +70,7 @@ Arguments Scope BigZ.gcd [bigZ_scope bigZ_scope].
 
 Local Notation "0" := BigZ.zero : bigZ_scope.
 Local Notation "1" := BigZ.one : bigZ_scope.
+Local Notation "2" := BigZ.two : bigZ_scope.
 Infix "+" := BigZ.add : bigZ_scope.
 Infix "-" := BigZ.sub : bigZ_scope.
 Notation "- x" := (BigZ.opp x) : bigZ_scope.
@@ -171,6 +172,7 @@ Ltac isBigZcst t :=
  | BigZ.Neg ?t => isBigNcst t
  | BigZ.zero => constr:true
  | BigZ.one => constr:true
+ | BigZ.two => constr:true
  | BigZ.minus_one => constr:true
  | _ => constr:false
  end.
@@ -186,6 +188,7 @@ Ltac BigZ_to_N t :=
  | BigZ.Pos ?t => BigN_to_N t
  | BigZ.zero => constr:0%N
  | BigZ.one => constr:1%N
+ | BigZ.two => constr:2%N
  | _ => constr:NotConstant
  end.
 
@@ -198,7 +201,6 @@ Add Ring BigZr : BigZring
   div BigZdiv).
 
 Section TestRing.
-Local Notation "2" := (BigZ.Pos (BigN.N0 2%int31)) : bigZ_scope.
 Let test : forall x y, 1 + x*y + x^2 + 1 == 1*1 + 1 + (y + 1*x)*x.
 Proof.
 intros. ring_simplify. reflexivity.
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index fb760bdf57..f9490cc9c7 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -31,6 +31,7 @@ Module Make (N:NType) <: ZType.
 
  Definition zero := Pos N.zero.
  Definition one  := Pos N.one.
+ Definition two := Pos N.two.
  Definition minus_one := Neg N.one.
 
  Definition of_Z x :=
@@ -64,6 +65,10 @@ Module Make (N:NType) <: ZType.
  exact N.spec_1.
  Qed.
 
+ Theorem spec_2: to_Z two = 2.
+ exact N.spec_2.
+ Qed.
+
  Theorem spec_m1: to_Z minus_one = -1.
  simpl; rewrite N.spec_1; auto.
  Qed.
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index 28a37abf85..5f87283940 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -63,6 +63,8 @@ Module Z
 Definition t := Z.
 Definition eqb := Zeq_bool.
 Definition zero := 0.
+Definition one := 1.
+Definition two := 2.
 Definition succ := Zsucc.
 Definition pred := Zpred.
 Definition add := Zplus.
@@ -99,6 +101,16 @@ Definition sub_succ_r := Zminus_succ_r.
 Definition mul_0_l := Zmult_0_l.
 Definition mul_succ_l := Zmult_succ_l.
 
+Lemma one_succ : 1 = Zsucc 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma two_succ : 2 = Zsucc 1.
+Proof.
+reflexivity.
+Qed.
+
 (** Boolean Equality *)
 
 Definition eqb_eq x y := iff_sym (Zeq_is_eq_bool x y).
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index 7df1871e11..ab555ca321 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -25,7 +25,8 @@ Bind Scope NScope with N.t.
 Infix "=="  := N.eq (at level 70) : NScope.
 Notation "x ~= y" := (~ N.eq x y) (at level 70) : NScope.
 Notation "0" := N.zero : NScope.
-Notation "1" := (N.succ N.zero) : NScope.
+Notation "1" := N.one : NScope.
+Notation "2" := N.two : NScope.
 Infix "+" := N.add : NScope.
 Infix "-" := N.sub : NScope.
 Infix "*" := N.mul : NScope.
@@ -43,6 +44,8 @@ Module Z.
 
 Definition t := (N.t * N.t)%type.
 Definition zero : t := (0, 0).
+Definition one : t := (1,0).
+Definition two : t := (2,0).
 Definition eq (p q : t) := (p#1 + q#2 == q#1 + p#2).
 Definition succ (n : t) : t := (N.succ n#1, n#2).
 Definition pred (n : t) : t := (n#1, N.succ n#2).
@@ -73,7 +76,8 @@ Bind Scope ZScope with Z.t.
 Infix "=="  := Z.eq (at level 70) : ZScope.
 Notation "x ~= y" := (~ Z.eq x y) (at level 70) : ZScope.
 Notation "0" := Z.zero : ZScope.
-Notation "1" := (Z.succ Z.zero) : ZScope.
+Notation "1" := Z.one : ZScope.
+Notation "2" := Z.two : ZScope.
 Infix "+" := Z.add : ZScope.
 Infix "-" := Z.sub : ZScope.
 Infix "*" := Z.mul : ZScope.
@@ -159,20 +163,22 @@ Hypothesis A_wd : Proper (Z.eq==>iff) A.
 Theorem bi_induction :
   A 0 -> (forall n, A n <-> A (Z.succ n)) -> forall n, A n.
 Proof.
+Open Scope NScope.
 intros A0 AS n; unfold Z.zero, Z.succ, Z.eq in *.
 destruct n as [n m].
-cut (forall p, A (p, 0%N)); [intro H1 |].
-cut (forall p, A (0%N, p)); [intro H2 |].
+cut (forall p, A (p, 0)); [intro H1 |].
+cut (forall p, A (0, p)); [intro H2 |].
 destruct (add_dichotomy n m) as [[p H] | [p H]].
-rewrite (A_wd (n, m) (0%N, p)) by (rewrite add_0_l; now rewrite add_comm).
+rewrite (A_wd (n, m) (0, p)) by (rewrite add_0_l; now rewrite add_comm).
 apply H2.
-rewrite (A_wd (n, m) (p, 0%N)) by now rewrite add_0_r. apply H1.
+rewrite (A_wd (n, m) (p, 0)) by now rewrite add_0_r. apply H1.
 induct p. assumption. intros p IH.
-apply -> (A_wd (0%N, p) (1%N, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].
-now apply <- AS.
+apply -> (A_wd (0, p) (1, N.succ p)) in IH; [| now rewrite add_0_l, add_1_l].
+rewrite one_succ in IH. now apply <- AS.
 induct p. assumption. intros p IH.
-replace 0%N with (snd (p, 0%N)); [| reflexivity].
-replace (N.succ p) with (N.succ (fst (p, 0%N))); [| reflexivity]. now apply -> AS.
+replace 0 with (snd (p, 0)); [| reflexivity].
+replace (N.succ p) with (N.succ (fst (p, 0))); [| reflexivity]. now apply -> AS.
+Close Scope NScope.
 Qed.
 
 End Induction.
@@ -189,6 +195,16 @@ Proof.
 intro n; unfold Z.succ, Z.pred, Z.eq; simpl; now nzsimpl.
 Qed.
 
+Theorem one_succ : 1 == Z.succ 0.
+Proof.
+unfold Z.eq; simpl. now nzsimpl'.
+Qed.
+
+Theorem two_succ : 2 == Z.succ 1.
+Proof.
+unfold Z.eq; simpl. now nzsimpl'.
+Qed.
+
 Theorem opp_0 : - 0 == 0.
 Proof.
 unfold Z.opp, Z.eq; simpl. now nzsimpl.
@@ -297,6 +313,8 @@ Qed.
 Definition t := Z.t.
 Definition eq := Z.eq.
 Definition zero := Z.zero.
+Definition one := Z.one.
+Definition two := Z.two.
 Definition succ := Z.succ.
 Definition pred := Z.pred.
 Definition add := Z.add.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v
index b33ed5f8ef..be201f2d66 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSig.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v
@@ -38,6 +38,7 @@ Module Type ZType.
  Parameter max : t -> t -> t.
  Parameter zero : t.
  Parameter one : t.
+ Parameter two : t.
  Parameter minus_one : t.
  Parameter succ : t -> t.
  Parameter add  : t -> t -> t.
@@ -65,6 +66,7 @@ Module Type ZType.
  Parameter spec_max : forall x y, [max x y] = Zmax [x] [y].
  Parameter spec_0: [zero] = 0.
  Parameter spec_1: [one] = 1.
+ Parameter spec_2: [two] = 2.
  Parameter spec_m1: [minus_one] = -1.
  Parameter spec_succ: forall n, [succ n] = [n] + 1.
  Parameter spec_add: forall x y, [add x y] = [x] + [y].
@@ -94,6 +96,8 @@ Module Type ZType_Notation (Import Z:ZType).
  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/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 90bda6343e..3e63755434 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -17,7 +17,7 @@ Require Import ZArith Nnat ZAxioms ZDivFloor ZSig.
 Module ZTypeIsZAxioms (Import Z : ZType').
 
 Hint Rewrite
- spec_0 spec_1 spec_add spec_sub spec_pred spec_succ
+ spec_0 spec_1 spec_2 spec_add spec_sub spec_pred spec_succ
  spec_mul spec_opp spec_of_Z spec_div spec_modulo
  spec_compare spec_eq_bool spec_max spec_min spec_abs spec_sgn
  spec_pow spec_even spec_odd
@@ -43,6 +43,16 @@ Proof.
 intros. zify. auto with zarith.
 Qed.
 
+Theorem one_succ : 1 == succ 0.
+Proof.
+now zify.
+Qed.
+
+Theorem two_succ : 2 == succ 1.
+Proof.
+now zify.
+Qed.
+
 Section Induction.
 
 Variable A : Z.t -> Prop.
@@ -225,12 +235,12 @@ Proof.
 intros n. zify. omega with *.
 Qed.
 
-Theorem sgn_pos : forall n, 0<n -> sgn n == succ 0.
+Theorem sgn_pos : forall n, 0<n -> sgn n == 1.
 Proof.
 intros n. zify. omega with *.
 Qed.
 
-Theorem sgn_neg : forall n, n<0 -> sgn n == opp (succ 0).
+Theorem sgn_neg : forall n, n<0 -> sgn n == opp 1.
 Proof.
 intros n. zify. omega with *.
 Qed.
@@ -239,9 +249,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.