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, 15 insertions, 4 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSig.v b/theories/Numbers/Natural/SpecViaZ/NSig.v
index 3ff2ded62..7cf3e7046 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 568ebeae8..e1dc5349b 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.