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

1 files changed, 28 insertions, 10 deletions

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.