Modularization of BinInt, related fixes in the stdlib

 All the functions about Z is now in a separated file BinIntDef,
 which is Included in BinInt.Z. This BinInt.Z directly
 implements ZAxiomsSig, and instantiates derived properties ZProp.

 Note that we refer to Z instead of t inside BinInt.Z,
 otherwise ring breaks later on @eq Z.t

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14106 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 138 insertions, 120 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index f150f12c8..2e3b7c49d 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -27,7 +27,7 @@ Local Open Scope N_scope.
     are placed in a module [N] for qualification purpose. *)
 
 Module N
- <: NAxiomsMiniSig
+ <: NAxiomsSig
  <: UsualOrderedTypeFull
  <: UsualDecidableTypeFull
  <: TotalOrder.
@@ -38,8 +38,8 @@ Include BinNatDef.N.
 
 (** Logical predicates *)
 
-Definition eq := @Logic.eq t.
-Definition eq_equiv := @eq_equivalence t.
+Definition eq := @Logic.eq N.
+Definition eq_equiv := @eq_equivalence N.
 
 Definition lt x y := (x ?= y) = Lt.
 Definition gt x y := (x ?= y) = Gt.
@@ -145,18 +145,6 @@ Proof.
 apply peano_rect_succ.
 Qed.
 
-(** Properties of double *)
-
-Lemma double_spec n : double n = 2 * n.
-Proof.
- reflexivity.
-Qed.
-
-Lemma succ_double_spec n : succ_double n = 2 * n + 1.
-Proof.
- now destruct n.
-Qed.
-
 (** Properties of mixed successor and predecessor. *)
 
 Lemma pos_pred_spec p : Pos.pred_N p = pred (Npos p).
@@ -324,14 +312,6 @@ Qed.
 
 Module Import BootStrap.
 
-Theorem succ_inj n m : succ n = succ m -> n = m.
-Proof.
-destruct n as [|p], m as [|q]; intro H; simpl in *; trivial; destr_eq H.
- now destruct (Pos.succ_not_1 q).
- now destruct (Pos.succ_not_1 p).
- f_equal. now apply Pos.succ_inj.
-Qed.
-
 Theorem add_0_r n : n + 0 = n.
 Proof.
 now destruct n.
@@ -362,53 +342,16 @@ Proof.
  rewrite <- H1 in H. now destruct H.
 Qed.
 
-Theorem mul_1_l n : 1 * n = n.
-Proof.
-now destruct n.
-Qed.
-
 Theorem mul_comm n m : n * m = m * n.
 Proof.
 destruct n, m; simpl; trivial. f_equal. apply Pos.mul_comm.
 Qed.
 
-Theorem mul_assoc n m p : n * (m * p) = n * m * p.
-Proof.
-destruct n; try reflexivity.
-destruct m; try reflexivity.
-destruct p; try reflexivity.
-simpl. f_equal. apply Pos.mul_assoc.
-Qed.
-
-Theorem mul_add_distr_r n m p : (n + m) * p = n * p + m * p.
-Proof.
-destruct n; try reflexivity.
-destruct m, p; try reflexivity.
-simpl. f_equal. apply Pos.mul_add_distr_r.
-Qed.
-
-Theorem mul_add_distr_l n m p : n * (m + p) = n * m + n * p.
-Proof.
-rewrite !(mul_comm n); apply mul_add_distr_r.
-Qed.
-
 Lemma le_0_l n : 0<=n.
 Proof.
 now destruct n.
 Qed.
 
-Theorem lt_trans n m q : n < m -> m < q -> n < q.
-Proof.
-destruct n, m, q; try easy. eapply Pos.lt_trans; eauto.
-Qed.
-
-Lemma le_trans n m p : n<=m -> m<=p -> n<=p.
-Proof.
- rewrite 3 lt_eq_cases. intros [H|H] [H'|H']; subst;
-  (now right) || left; trivial.
- now apply lt_trans with m.
-Qed.
-
 Lemma add_lt_cancel_l n m p : p+n < p+m -> n<m.
 Proof.
  intro H. destruct p. simpl; auto.
@@ -423,38 +366,40 @@ Qed.
 
 End BootStrap.
 
-(** Specification of minimum and maximum *)
 
-Theorem min_l n m : n <= m -> min n m = n.
+(** Properties of [double] and [succ_double] *)
+
+Lemma double_spec n : double n = 2 * n.
 Proof.
-unfold min, le. case compare; trivial. now destruct 1.
+ reflexivity.
 Qed.
 
-Theorem min_r n m : m <= n -> min n m = m.
+Lemma succ_double_spec n : succ_double n = 2 * n + 1.
 Proof.
-unfold min, le. rewrite <- compare_antisym.
-case compare_spec; trivial. now destruct 2.
+ now destruct n.
 Qed.
 
-Theorem max_l n m : m <= n -> max n m = n.
+Lemma double_add n m : double (n+m) = double n + double m.
 Proof.
-unfold max, le. rewrite <- compare_antisym.
-case compare_spec; auto. now destruct 2.
+ now destruct n, m.
 Qed.
 
-Theorem max_r n m : n <= m -> max n m = m.
+Lemma succ_double_add n m : succ_double (n+m) = double n + succ_double m.
 Proof.
-unfold max, le. case compare; trivial. now destruct 1.
+ now destruct n, m.
 Qed.
 
-(** 0 is the least natural number *)
-
-Theorem compare_0_r n : (n ?= 0) <> Lt.
+Lemma double_mul n m : double (n*m) = double n * m.
 Proof.
-now destruct n.
+ now destruct n, m.
 Qed.
 
-(** Dividing by 2 *)
+Lemma succ_double_mul n m :
+ succ_double n * m = double n * m + m.
+Proof.
+ destruct n; simpl; destruct m; trivial.
+ now rewrite Pos.add_comm.
+Qed.
 
 Lemma div2_double n : div2 (double n) = n.
 Proof.
@@ -476,7 +421,45 @@ Proof.
 intro H. rewrite <- (div2_succ_double n), H. apply div2_succ_double.
 Qed.
 
-(** Speficications of power *)
+Lemma succ_double_lt n m : n<m -> succ_double n < double m.
+Proof.
+ destruct n as [|n], m as [|m]; intros H; try easy.
+ unfold lt in *; simpl in *. now rewrite Pos.compare_xI_xO, H.
+Qed.
+
+
+(** Specification of minimum and maximum *)
+
+Theorem min_l n m : n <= m -> min n m = n.
+Proof.
+unfold min, le. case compare; trivial. now destruct 1.
+Qed.
+
+Theorem min_r n m : m <= n -> min n m = m.
+Proof.
+unfold min, le. rewrite <- compare_antisym.
+case compare_spec; trivial. now destruct 2.
+Qed.
+
+Theorem max_l n m : m <= n -> max n m = n.
+Proof.
+unfold max, le. rewrite <- compare_antisym.
+case compare_spec; auto. now destruct 2.
+Qed.
+
+Theorem max_r n m : n <= m -> max n m = m.
+Proof.
+unfold max, le. case compare; trivial. now destruct 1.
+Qed.
+
+(** 0 is the least natural number *)
+
+Theorem compare_0_r n : (n ?= 0) <> Lt.
+Proof.
+now destruct n.
+Qed.
+
+(** Specifications of power *)
 
 Lemma pow_0_r n : n ^ 0 = 1.
 Proof. reflexivity. Qed.
@@ -494,13 +477,28 @@ Qed.
 
 (** Specification of Base-2 logarithm *)
 
+Lemma size_log2 n : n<>0 -> size n = succ (log2 n).
+Proof.
+ destruct n as [|[n|n| ]]; trivial. now destruct 1.
+Qed.
+
+Lemma size_gt n : n < 2^(size n).
+Proof.
+ destruct n. reflexivity. simpl. apply Pos.size_gt.
+Qed.
+
+Lemma size_le n : 2^(size n) <= succ_double n.
+Proof.
+ destruct n. discriminate. simpl.
+ change (2^Pos.size p <= Pos.succ (p~0))%positive.
+ apply Pos.lt_le_incl, Pos.lt_succ_r, Pos.size_le.
+Qed.
+
 Lemma log2_spec n : 0 < n ->
  2^(log2 n) <= n < 2^(succ (log2 n)).
 Proof.
  destruct n as [|[p|p|]]; discriminate || intros _; simpl; split.
- eapply le_trans with (Npos (p~0)).
- apply Pos.size_le.
- apply lt_eq_cases; left. apply Pos.lt_succ_diag_r.
+ apply (size_le (Npos p)).
  apply Pos.size_gt.
  apply Pos.size_le.
  apply Pos.size_gt.
@@ -513,24 +511,6 @@ Proof.
  destruct n; intros Hn. reflexivity. now destruct Hn.
 Qed.
 
-Lemma size_log2 n : n<>0 -> size n = succ (log2 n).
-Proof.
- destruct n as [|[n|n| ]]; trivial. now destruct 1.
-Qed.
-
-Lemma size_gt n : n < 2^(size n).
-Proof.
- destruct n. reflexivity. simpl. apply Pos.size_gt.
-Qed.
-
-Lemma size_le n : 2^(size n) <= succ_double n.
-Proof.
- destruct n. discriminate.
- simpl. apply le_trans with (Npos (p~0)).
- apply Pos.size_le.
- apply lt_eq_cases. left. apply Pos.lt_succ_diag_r.
-Qed.
-
 (** Specification of parity functions *)
 
 Lemma even_spec n : even n = true <-> Even n.
@@ -563,21 +543,17 @@ Proof.
   induction a; cbv beta iota delta [pos_div_eucl]; fold pos_div_eucl; cbv zeta.
   (* a~1 *)
   destruct pos_div_eucl as (q,r).
-  assert (Npos a~1 = (double q)*b + succ_double r).
-   rewrite succ_double_spec, double_spec.
-   now rewrite add_assoc, <- mul_assoc, <- mul_add_distr_l, <- IHa.
-  case leb_spec; intros H'; trivial.
-  rewrite (succ_double_spec q), mul_add_distr_r, <- double_spec,
-   mul_1_l, <- add_assoc.
+  change (Npos a~1) with (succ_double (Npos a)).
+  rewrite IHa, succ_double_add, double_mul.
+  case leb_spec; intros H; trivial.
+  rewrite succ_double_mul, <- add_assoc. f_equal.
   now rewrite (add_comm b), sub_add.
   (* a~0 *)
   destruct pos_div_eucl as (q,r).
-  assert (Npos a~0 = (double q)*b + double r).
-   rewrite (double_spec q), (double_spec r). (* BUG: !double_spec *)
-   now rewrite <- mul_assoc, <- mul_add_distr_l, <- IHa.
-  case leb_spec; intros H'; trivial.
-  rewrite (succ_double_spec q), mul_add_distr_r, <- double_spec,
-   mul_1_l, <- add_assoc.
+  change (Npos a~0) with (double (Npos a)).
+  rewrite IHa, double_add, double_mul.
+  case leb_spec; intros H; trivial.
+  rewrite succ_double_mul, <- add_assoc. f_equal.
   now rewrite (add_comm b), sub_add.
   (* 1 *)
   now destruct b as [|[ | | ]].
@@ -602,12 +578,6 @@ Proof.
  intros _. apply div_mod'.
 Qed.
 
-Lemma succ_double_lt n m : n<m -> succ_double n < double m.
-Proof.
- destruct n as [|n], m as [|m]; intros H; try easy.
- unfold lt in *; simpl in *. now rewrite Pos.compare_xI_xO, H.
-Qed.
-
 Theorem pos_div_eucl_remainder (a:positive) (b:N) :
   b<>0 -> snd (pos_div_eucl a b) < b.
 Proof.
@@ -898,7 +868,7 @@ Proof. reflexivity. Qed.
 Definition pred_0 : pred 0 = 0.
 Proof. reflexivity. Qed.
 
-(** Proof of morphisms, obvious since eq is Leibniz *)
+(** Proofs of morphisms, obvious since eq is Leibniz *)
 
 Local Obligation Tactic := simpl_relation.
 Program Definition succ_wd : Proper (eq==>eq) succ := _.
@@ -947,10 +917,57 @@ Qed.
 
 (** Instantiation of generic properties of natural numbers *)
 
-Include !NProp
- <+ !UsualMinMaxLogicalProperties <+ !UsualMinMaxDecProperties.
+Set Inline Level 30. (* For inlining only t eq zero one two *)
+
+Include NProp
+ <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+
+(** Auxiliary results about right shift on positive numbers,
+    used in BinInt *)
 
-(* TODO : avoir un inlining selectif : t eq zero one two *)
+Lemma pos_pred_shiftl_low : forall p n m, m<n ->
+ testbit (Pos.pred_N (Pos.shiftl p n)) m = true.
+Proof.
+ induction n using peano_ind.
+ now destruct m.
+ intros m H. unfold Pos.shiftl.
+ destruct n as [|n]; simpl in *.
+ destruct m. now destruct p. elim (Pos.nlt_1_r _ H).
+ rewrite Pos.iter_succ. simpl.
+ set (u:=Pos.iter n xO p) in *; clearbody u.
+ destruct m as [|m]. now destruct u.
+ rewrite <- (IHn (Pos.pred_N m)).
+ rewrite <- (testbit_odd_succ _ (Pos.pred_N m)).
+ rewrite succ_pos_pred. now destruct u.
+ apply le_0_l.
+ apply succ_lt_mono. now rewrite succ_pos_pred.
+Qed.
+
+Lemma pos_pred_shiftl_high : forall p n m, n<=m ->
+ testbit (Pos.pred_N (Pos.shiftl p n)) m =
+ testbit (shiftl (Pos.pred_N p) n) m.
+Proof.
+ induction n using peano_ind; intros m H.
+ unfold shiftl. simpl. now destruct (Pos.pred_N p).
+ rewrite shiftl_succ_r.
+ destruct n as [|n].
+ destruct m as [|m]. now destruct H. now destruct p.
+ destruct m as [|m]. now destruct H.
+ rewrite <- (succ_pos_pred m).
+ rewrite double_spec, testbit_even_succ by apply le_0_l.
+ rewrite <- IHn.
+ rewrite testbit_succ_r_div2 by apply le_0_l.
+ f_equal. simpl. rewrite Pos.iter_succ.
+ now destruct (Pos.iter n xO p).
+ apply succ_le_mono. now rewrite succ_pos_pred.
+Qed.
+
+Lemma pred_div2_up p : Pos.pred_N (Pos.div2_up p) = div2 (Pos.pred_N p).
+Proof.
+ destruct p as [p|p| ]; trivial.
+ simpl. apply Pos.pred_N_succ.
+ destruct p; simpl; trivial.
+Qed.
 
 End N.
 
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v
index ec91dc5db..d459f8509 100644
--- a/theories/NArith/BinNatDef.v
+++ b/theories/NArith/BinNatDef.v
@@ -8,6 +8,7 @@
 
 Require Export BinNums.
 Require Import BinPos.
+
 Local Open Scope N_scope.
 
 (**********************************************************************)