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, 21 insertions, 10 deletions

diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
index 627235252..fd192dce6 100644
--- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v
+++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v
@@ -31,6 +31,8 @@ Local Notation "[| x |]" := (ZnZ.to_Z x) (at level 0, x at level 99).
 
 Definition eq (n m : t) := [| n |] = [| m |].
 Definition zero := ZnZ.zero.
+Definition one := ZnZ.one.
+Definition two := ZnZ.succ ZnZ.one.
 Definition succ := ZnZ.succ.
 Definition pred := ZnZ.pred.
 Definition add := ZnZ.add.
@@ -45,10 +47,10 @@ Local Infix "+" := add.
 Local Infix "-" := sub.
 Local Infix "*" := mul.
 
-Hint Rewrite ZnZ.spec_0 ZnZ.spec_succ ZnZ.spec_pred
+Hint Rewrite ZnZ.spec_0 ZnZ.spec_1 ZnZ.spec_succ ZnZ.spec_pred
  ZnZ.spec_add ZnZ.spec_mul ZnZ.spec_sub : cyclic.
 Ltac zify :=
- unfold eq, zero, succ, pred, add, sub, mul in *;
+ unfold eq, zero, one, two, succ, pred, add, sub, mul in *;
  autorewrite with cyclic.
 Ltac zcongruence := repeat red; intros; zify; congruence.
 
@@ -75,20 +77,19 @@ Proof.
 pose proof gt_wB_1; auto with zarith.
 Qed.
 
+Lemma one_mod_wB : 1 mod wB = 1.
+Proof.
+rewrite Zmod_small. reflexivity. split. auto with zarith. apply gt_wB_1.
+Qed.
+
 Lemma succ_mod_wB : forall n : Z, (n + 1) mod wB = ((n mod wB) + 1) mod wB.
 Proof.
-intro n.
-pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zplus_mod.
-reflexivity.
-now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
+intro n. rewrite <- one_mod_wB at 2. now rewrite <- Zplus_mod.
 Qed.
 
 Lemma pred_mod_wB : forall n : Z, (n - 1) mod wB = ((n mod wB) - 1) mod wB.
 Proof.
-intro n.
-pattern 1 at 2. replace 1 with (1 mod wB). rewrite <- Zminus_mod.
-reflexivity.
-now rewrite Zmod_small; [ | split; [auto with zarith | apply gt_wB_1]].
+intro n. rewrite <- one_mod_wB at 2. now rewrite Zminus_mod.
 Qed.
 
 Lemma NZ_to_Z_mod : forall n, [| n |] mod wB = [| n |].
@@ -103,6 +104,16 @@ rewrite <- pred_mod_wB.
 replace ([| n |] + 1 - 1)%Z with [| n |] by ring. apply NZ_to_Z_mod.
 Qed.
 
+Theorem one_succ : one == succ zero.
+Proof.
+zify; simpl. now rewrite one_mod_wB.
+Qed.
+
+Theorem two_succ : two == succ one.
+Proof.
+reflexivity.
+Qed.
+
 Section Induction.
 
 Variable A : t -> Prop.