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

7 files changed, 71 insertions, 32 deletions

diff --git a/theories/Numbers/NatInt/NZAdd.v b/theories/Numbers/NatInt/NZAdd.v
index 7d7cc4ac5..202875b8a 100644
--- a/theories/Numbers/NatInt/NZAdd.v
+++ b/theories/Numbers/NatInt/NZAdd.v
@@ -14,7 +14,9 @@ Module Type NZAddProp (Import NZ : NZAxiomsSig')(Import NZBase : NZBaseProp NZ).
 
 Hint Rewrite
  pred_succ add_0_l add_succ_l mul_0_l mul_succ_l sub_0_r sub_succ_r : nz.
+Hint Rewrite one_succ two_succ : nz'.
 Ltac nzsimpl := autorewrite with nz.
+Ltac nzsimpl' := autorewrite with nz nz'.
 
 Theorem add_0_r : forall n, n + 0 == n.
 Proof.
@@ -38,14 +40,16 @@ Qed.
 
 Theorem add_1_l : forall n, 1 + n == S n.
 Proof.
-intro n; now nzsimpl.
+intro n; now nzsimpl'.
 Qed.
 
 Theorem add_1_r : forall n, n + 1 == S n.
 Proof.
-intro n; now nzsimpl.
+intro n; now nzsimpl'.
 Qed.
 
+Hint Rewrite add_1_l add_1_r : nz.
+
 Theorem add_assoc : forall n m p, n + (m + p) == (n + m) + p.
 Proof.
 intros n m p; nzinduct n. now nzsimpl.
@@ -80,7 +84,9 @@ Qed.
 
 Theorem sub_1_r : forall n, n - 1 == P n.
 Proof.
-intro n; now nzsimpl.
+intro n; now nzsimpl'.
 Qed.
 
+Hint Rewrite sub_1_r : nz.
+
 End NZAddProp.
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index f2b300cff..8d56772ac 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -26,8 +26,6 @@ Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T).
  Notation "0" := zero.
  Notation S := succ.
  Notation P := pred.
- Notation "1" := (S 0).
- Notation "2" := (S 1).
 End ZeroSuccPredNotation.
 
 Module Type ZeroSuccPred' (T:Typ) :=
@@ -42,9 +40,33 @@ Module Type IsNZDomain (Import E:Eq')(Import NZ:ZeroSuccPred' E).
     A 0 -> (forall n, A n <-> A (S n)) -> forall n, A n.
 End IsNZDomain.
 
-Module Type NZDomainSig := EqualityType <+ ZeroSuccPred <+ IsNZDomain.
-Module Type NZDomainSig' := EqualityType' <+ ZeroSuccPred' <+ IsNZDomain.
+(** Axiomatization of some more constants
 
+    Simply denoting "1" for (S 0) and so on works ok when implementing
+    by nat, but leaves some (Nsucc N0) when implementing by N.
+*)
+
+Module Type OneTwo (Import T:Typ).
+ Parameter Inline one two : t.
+End OneTwo.
+
+Module Type OneTwoNotation (T:Typ)(Import NZ:OneTwo T).
+ Notation "1" := one.
+ Notation "2" := two.
+End OneTwoNotation.
+
+Module Type OneTwo' (T:Typ) := OneTwo T <+ OneTwoNotation T.
+
+Module Type IsOneTwo (E:Eq')(Z:ZeroSuccPred' E)(O:OneTwo' E).
+ Import E Z O.
+ Axiom one_succ : 1 == S 0.
+ Axiom two_succ : 2 == S 1.
+End IsOneTwo.
+
+Module Type NZDomainSig :=
+ EqualityType <+ ZeroSuccPred <+ IsNZDomain <+ OneTwo <+ IsOneTwo.
+Module Type NZDomainSig' :=
+ EqualityType' <+ ZeroSuccPred' <+ IsNZDomain <+ OneTwo' <+ IsOneTwo.
 
 (** Axiomatization of basic operations : [+] [-] [*] *)
 
diff --git a/theories/Numbers/NatInt/NZDiv.v b/theories/Numbers/NatInt/NZDiv.v
index 3b9720f32..fe66d88c6 100644
--- a/theories/Numbers/NatInt/NZDiv.v
+++ b/theories/Numbers/NatInt/NZDiv.v
@@ -160,12 +160,12 @@ Qed.
 
 Lemma div_1_l: forall a, 1<a -> 1/a == 0.
 Proof.
-intros; apply div_small; split; auto. apply le_succ_diag_r.
+intros; apply div_small; split; auto. apply le_0_1.
 Qed.
 
 Lemma mod_1_l: forall a, 1<a -> 1 mod a == 1.
 Proof.
-intros; apply mod_small; split; auto. apply le_succ_diag_r.
+intros; apply mod_small; split; auto. apply le_0_1.
 Qed.
 
 Lemma div_mul : forall a b, 0<=a -> 0<b -> (a*b)/b == a.
diff --git a/theories/Numbers/NatInt/NZDomain.v b/theories/Numbers/NatInt/NZDomain.v
index a26e93d76..2ab7413e3 100644
--- a/theories/Numbers/NatInt/NZDomain.v
+++ b/theories/Numbers/NatInt/NZDomain.v
@@ -313,8 +313,8 @@ Theorem ofnat_S_gt_0 :
 Proof.
 unfold ofnat.
 intros n; induction n as [| n IH]; simpl in *.
-apply lt_0_1.
-apply lt_trans with 1. apply lt_0_1. now rewrite <- succ_lt_mono.
+apply lt_succ_diag_r.
+apply lt_trans with (S 0). apply lt_succ_diag_r. now rewrite <- succ_lt_mono.
 Qed.
 
 Theorem ofnat_S_neq_0 :
diff --git a/theories/Numbers/NatInt/NZMul.v b/theories/Numbers/NatInt/NZMul.v
index 55ec3f30e..33c50b24e 100644
--- a/theories/Numbers/NatInt/NZMul.v
+++ b/theories/Numbers/NatInt/NZMul.v
@@ -56,14 +56,16 @@ Qed.
 
 Theorem mul_1_l : forall n, 1 * n == n.
 Proof.
-intro n. now nzsimpl.
+intro n. now nzsimpl'.
 Qed.
 
 Theorem mul_1_r : forall n, n * 1 == n.
 Proof.
-intro n. now nzsimpl.
+intro n. now nzsimpl'.
 Qed.
 
+Hint Rewrite mul_1_l mul_1_r : nz.
+
 Theorem mul_shuffle0 : forall n m p, n*m*p == n*p*m.
 Proof.
 intros n m p. now rewrite <- 2 mul_assoc, (mul_comm m).
diff --git a/theories/Numbers/NatInt/NZOrder.v b/theories/Numbers/NatInt/NZOrder.v
index 93201964e..e2e398025 100644
--- a/theories/Numbers/NatInt/NZOrder.v
+++ b/theories/Numbers/NatInt/NZOrder.v
@@ -231,19 +231,33 @@ Qed.
 
 Theorem lt_0_1 : 0 < 1.
 Proof.
-apply lt_succ_diag_r.
+rewrite one_succ. apply lt_succ_diag_r.
 Qed.
 
 Theorem le_0_1 : 0 <= 1.
 Proof.
-apply le_succ_diag_r.
+apply lt_le_incl, lt_0_1.
+Qed.
+
+Theorem lt_0_2 : 0 < 2.
+Proof.
+transitivity 1. apply lt_0_1. rewrite two_succ. apply lt_succ_diag_r.
+Qed.
+
+Theorem le_0_2 : 0 <= 2.
+Proof.
+apply lt_le_incl, lt_0_2.
 Qed.
 
 Theorem lt_1_l : forall n m, 0 < n -> n < m -> 1 < m.
 Proof.
-intros n m H1 H2. apply <- le_succ_l in H1. order.
+intros n m H1 H2. rewrite one_succ. apply <- le_succ_l in H1. order.
 Qed.
 
+(** The order tactic enriched with some knowledge of 0,1,2 *)
+
+Ltac order' := generalize lt_0_1 lt_0_2; order.
+
 
 (** More Trichotomy, decidability and double negation elimination. *)
 
diff --git a/theories/Numbers/NatInt/NZPow.v b/theories/Numbers/NatInt/NZPow.v
index cbc286fbb..a9b2fdc31 100644
--- a/theories/Numbers/NatInt/NZPow.v
+++ b/theories/Numbers/NatInt/NZPow.v
@@ -40,13 +40,6 @@ Module NZPowProp
 
 Hint Rewrite pow_0_r pow_succ_r : nz.
 
-Lemma lt_0_2 : 0 < 2.
-Proof.
- apply lt_succ_r, le_0_1.
-Qed.
-
-Ltac order' := generalize lt_0_1 lt_0_2; order.
-
 (** Power and basic constants *)
 
 Lemma pow_0_l : forall a, 0<a -> 0^a == 0.
@@ -58,7 +51,7 @@ Qed.
 
 Lemma pow_1_r : forall a, a^1 == a.
 Proof.
- intros. now nzsimpl.
+ intros. now nzsimpl'.
 Qed.
 
 Lemma pow_1_l : forall a, 0<=a -> 1^a == 1.
@@ -68,13 +61,15 @@ Proof.
  now nzsimpl.
 Qed.
 
-Hint Rewrite pow_1_l : nz.
+Hint Rewrite pow_1_r pow_1_l : nz.
 
 Lemma pow_2_r : forall a, a^2 == a*a.
 Proof.
- intros. nzsimpl; order'.
+ intros. rewrite two_succ. nzsimpl; order'.
 Qed.
 
+Hint Rewrite pow_2_r : nz.
+
 (** Power and addition, multiplication *)
 
 Lemma pow_add_r : forall a b c, 0<=b -> 0<=c ->
@@ -173,7 +168,7 @@ Qed.
 Lemma pow_le_mono_r : forall a b c, 0<a -> 0<=b<=c -> a^b <= a^c.
 Proof.
  intros a b c Ha (Hb,H).
- apply le_succ_l in Ha.
+ apply le_succ_l in Ha; rewrite <- one_succ in Ha.
  apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
  apply lt_eq_cases in H; destruct H as [H|H]; [|now rewrite <- H].
  apply lt_le_incl, pow_lt_mono_r; now try split.
@@ -192,7 +187,7 @@ Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d ->
  a^b < c^d.
 Proof.
  intros a b c d (Ha,Hac) (Hb,Hbd).
- apply le_succ_l in Ha.
+ apply le_succ_l in Ha; rewrite <- one_succ in Ha.
  apply lt_eq_cases in Ha; destruct Ha as [Ha|Ha]; [|rewrite <- Ha].
  transitivity (a^d).
  apply pow_lt_mono_r; intuition order.
@@ -277,9 +272,9 @@ Proof.
  intros a b Ha Hb. apply le_ind with (4:=Hb). solve_predicate_wd.
  nzsimpl. order'.
  clear b Hb. intros b Hb IH. nzsimpl; trivial.
- rewrite <- !le_succ_l in *.
+ rewrite <- !le_succ_l in *. rewrite <- two_succ in Ha.
  transitivity (2*(S b)).
-  nzsimpl. rewrite <- 2 succ_le_mono.
+  nzsimpl'. rewrite <- 2 succ_le_mono.
   rewrite <- (add_0_l b) at 1. apply add_le_mono; order.
  apply mul_le_mono_nonneg; trivial.
  order'.
@@ -323,7 +318,7 @@ Proof.
          (a + b) * (a ^ c + b ^ c) <= 2 * (a * a ^ c + b * b ^ c)).
  (* begin *)
   intros a b c (Ha,H) Hc.
-  rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl.
+  rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'.
   rewrite <- !add_assoc. apply add_le_mono_l.
   rewrite !add_assoc. apply add_le_mono_r.
   destruct (le_exists_sub _ _ H) as (d & EQ & Hd).
@@ -345,7 +340,7 @@ Proof.
  rewrite mul_assoc. rewrite (mul_comm (a+b)).
  assert (EQ : S (P c) == c) by (apply lt_succ_pred with 0; order').
  assert (LE : 0 <= P c) by (now rewrite succ_le_mono, EQ, le_succ_l).
- assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl; order).
+ assert (EQ' : 2^c == 2^(P c) * 2) by (rewrite <- EQ at 1; nzsimpl'; order).
  rewrite EQ', <- !mul_assoc.
  apply mul_le_mono_nonneg_l.
  apply pow_nonneg_nonneg; order'.