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

2 files changed, 17 insertions, 6 deletions

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.