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, 2 deletions

diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index ef4ac7c45..0f04869c0 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 6697d59c3..9e6e4b609 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 =>