Arith: full integration of the "Numbers" modular framework

 - The earlier proof-of-concept file NPeano (which instantiates
   the "Numbers" framework for nat) becomes now the entry point
   in the Arith lib, and gets renamed PeanoNat. It still provides
   an inner module "Nat" which sums up everything about type nat
   (functions, predicates and properties of them).
   This inner module Nat is usable as soon as you Require Import Arith,
   or just Arith_base, or simply PeanoNat.

 - Definitions of operations over type nat are now grouped in a new
   file Init/Nat.v. This file is meant to be used without "Import",
   hence providing for instance Nat.add or Nat.sqrt as soon as coqtop
   starts (but no proofs about them).

 - The definitions that used to be in Init/Peano.v (pred, plus, minus, mult)
   are now compatibility notations (for Nat.pred, Nat.add, Nat.sub, Nat.mul
   where here Nat is Init/Nat.v).

 - This Coq.Init.Nat module (with only pure definitions) is Include'd
   in the aforementioned Coq.Arith.PeanoNat.Nat. You might see Init.Nat
   sometimes instead of just Nat (for instance when doing "Print plus").
   Normally it should be ok to just ignore these "Init" since
   Init.Nat is included in the full PeanoNat.Nat. I'm investigating if
   it's possible to get rid of these "Init" prefixes.

 - Concerning predicates, orders le and lt are still defined in Init/Peano.v,
   with their notations "<=" and "<". Properties in PeanoNat.Nat directly
   refer to these predicates in Peano. For instantation reasons, PeanoNat.Nat
   also contains a Nat.le and Nat.lt (defined via "Definition le := Peano.le",
   we cannot yet include an Inductive to implement a Parameter), but these
   aliased predicates won't probably be very convenient to use.

 - Technical remark: I've split the previous property functor NProp in
   two parts (NBasicProp and NExtraProp), it helps a lot for building
   PeanoNat.Nat incrementally. Roughly speaking, we have the following schema:

   Module Nat.
     Include Coq.Init.Nat. (* definition of operations : add ... sqrt ... *)
     ... (** proofs of specifications for basic ops such as + * - *)
     Include NBasicProp. (** generic properties of these basic ops *)
     ... (** proofs of specifications for advanced ops (pow sqrt log2...)
             that may rely on proofs for + * - *)
     Include NExtraProp. (** all remaining properties *)
   End Nat.

- All other files in directory Arith are now taking advantage of PeanoNat :
  they are now filled with compatibility notations (when earlier lemmas
  have exact counterpart in the Nat module) or lemmas with one-line proofs
  based on the Nat module. All hints for database "arith" remain declared
  in these old-style file (such as Plus.v, Lt.v, etc). All the old-style
  files are still Require'd (or not) by Arith.v, just as before.

- Compatibility should be almost complete. For instance in the stdlib,
  the only adaptations were due to .ml code referring to some Coq constant
  name such as Coq.Init.Peano.pred, which doesn't live well with the
  new compatibility notations.

7 files changed, 43 insertions, 820 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZProperties.v b/theories/Numbers/Integer/Abstract/ZProperties.v
index 8973df358..446fd7eb8 100644
--- a/theories/Numbers/Integer/Abstract/ZProperties.v
+++ b/theories/Numbers/Integer/Abstract/ZProperties.v
@@ -9,11 +9,22 @@
 Require Export ZAxioms ZMaxMin ZSgnAbs ZParity ZPow ZDivTrunc ZDivFloor
  ZGcd ZLcm NZLog NZSqrt ZBits.
 
-(** This functor summarizes all known facts about Z. *)
+(** The two following functors summarize all known facts about N.
 
-Module Type ZProp (Z:ZAxiomsSig) :=
- ZMaxMinProp Z <+ ZSgnAbsProp Z <+ ZParityProp Z <+ ZPowProp Z
- <+ NZSqrtProp Z Z <+ NZSqrtUpProp Z Z
- <+ NZLog2Prop Z Z Z <+ NZLog2UpProp Z Z Z
- <+ ZDivProp Z <+ ZQuotProp Z <+ ZGcdProp Z <+ ZLcmProp Z
- <+ ZBitsProp Z.
+    - [ZBasicProp] provides properties of basic functions:
+      + - * min max <= <
+
+    - [ZExtraProp] provides properties of advanced functions:
+      pow, sqrt, log2, div, gcd, and bitwise functions.
+
+    If necessary, the earlier all-in-one functor [ZProp]
+    could be re-obtained via [ZBasicProp <+ ZExtraProp] *)
+
+Module Type ZBasicProp (Z:ZAxiomsMiniSig) := ZMaxMinProp Z.
+
+Module Type ZExtraProp (Z:ZAxiomsSig)(P:ZBasicProp Z) :=
+ ZSgnAbsProp Z P <+ ZParityProp Z P <+ ZPowProp Z P
+ <+ NZSqrtProp Z Z P <+ NZSqrtUpProp Z Z P
+ <+ NZLog2Prop Z Z Z P <+ NZLog2UpProp Z Z Z P
+ <+ ZDivProp Z P <+ ZQuotProp Z P <+ ZGcdProp Z P <+ ZLcmProp Z P
+ <+ ZBitsProp Z P.
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index eca97ace9..c1c78d911 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -29,7 +29,7 @@ Delimit Scope bigZ_scope with bigZ.
 Module BigZ <: ZType <: OrderedTypeFull <: TotalOrder :=
  ZMake.Make BigN
  <+ ZTypeIsZAxioms
- <+ ZProp [no inline]
+ <+ ZBasicProp [no inline] <+ ZExtraProp [no inline]
  <+ HasEqBool2Dec [no inline]
  <+ MinMaxLogicalProperties [no inline]
  <+ MinMaxDecProperties [no inline].
diff --git a/theories/Numbers/Integer/NatPairs/ZNatPairs.v b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
index b5e1fa5b0..11eb6e4d0 100644
--- a/theories/Numbers/Integer/NatPairs/ZNatPairs.v
+++ b/theories/Numbers/Integer/NatPairs/ZNatPairs.v
@@ -332,9 +332,9 @@ and get their properties *)
 
 (* The following lines increase the compilation time at least twice *)
 (*
-Require Import NPeano.
+Require PeanoNat.
 
-Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod NPeanoAxiomsMod.
+Module Export ZPairsPeanoAxiomsMod := ZPairsAxiomsMod PeanoNat.Nat.
 Module Export ZPairsPropMod := ZPropFunct ZPairsPeanoAxiomsMod.
 
 Eval compute in (3, 5) * (4, 6).
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v
index 3a432eaa0..5b41dba43 100644
--- a/theories/Numbers/NatInt/NZAxioms.v
+++ b/theories/Numbers/NatInt/NZAxioms.v
@@ -19,7 +19,8 @@ Require Export Equalities Orders NumPrelude GenericMinMax.
 
 Module Type ZeroSuccPred (Import T:Typ).
  Parameter Inline(20) zero : t.
- Parameters Inline succ pred : t -> t.
+ Parameter Inline(50) succ : t -> t.
+ Parameter Inline pred : t -> t.
 End ZeroSuccPred.
 
 Module Type ZeroSuccPredNotation (T:Typ)(Import NZ:ZeroSuccPred T).
diff --git a/theories/Numbers/Natural/Abstract/NProperties.v b/theories/Numbers/Natural/Abstract/NProperties.v
index 907394101..df3e7c7e4 100644
--- a/theories/Numbers/Natural/Abstract/NProperties.v
+++ b/theories/Numbers/Natural/Abstract/NProperties.v
@@ -9,9 +9,20 @@
 Require Export NAxioms.
 Require Import NMaxMin NParity NPow NSqrt NLog NDiv NGcd NLcm NBits.
 
-(** This functor summarizes all known facts about N. *)
+(** The two following functors summarize all known facts about N.
 
-Module Type NProp (N:NAxiomsSig) :=
- NMaxMinProp N <+ NParityProp N <+ NPowProp N <+ NSqrtProp N
-  <+ NLog2Prop N <+ NDivProp N <+ NGcdProp N <+ NLcmProp N
-  <+ NBitsProp N.
+    - [NBasicProp] provides properties of basic functions:
+      + - * min max <= <
+
+    - [NExtraProp] provides properties of advanced functions:
+      pow, sqrt, log2, div, gcd, and bitwise functions.
+
+    If necessary, the earlier all-in-one functor [NProp]
+    could be re-obtained via [NBasicProp <+ NExtraProp] *)
+
+Module Type NBasicProp (N:NAxiomsMiniSig) := NMaxMinProp N.
+
+Module Type NExtraProp (N:NAxiomsSig)(P:NBasicProp N) :=
+ NParityProp N P <+ NPowProp N P <+ NSqrtProp N P
+  <+ NLog2Prop N P <+ NDivProp N P <+ NGcdProp N P <+ NLcmProp N P
+  <+ NBitsProp N P.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 380963cff..02ed9fe53 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -31,7 +31,7 @@ Delimit Scope bigN_scope with bigN.
 Module BigN <: NType <: OrderedTypeFull <: TotalOrder :=
   NMake.Make Int31Cyclic
   <+ NTypeIsNAxioms
-  <+ NProp [no inline]
+  <+ NBasicProp [no inline] <+ NExtraProp [no inline]
   <+ HasEqBool2Dec [no inline]
   <+ MinMaxLogicalProperties [no inline]
   <+ MinMaxDecProperties [no inline].
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 5e36916b9..1620cfed8 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -8,808 +8,8 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Import
- Bool Peano Peano_dec Compare_dec Plus Mult Minus Le Lt EqNat Div2 Wf_nat
- NAxioms NProperties.
+Require Import PeanoNat NAxioms.
 
-(** Functions not already defined *)
+(** * [PeanoNat.Nat] already implements [NAxiomSig] *)
 
-Fixpoint leb n m :=
-  match n, m with
-    | O, _ => true
-    | _, O => false
-    | S n', S m' => leb n' m'
-  end.
-
-Definition ltb n m := leb (S n) m.
-
-Infix "<=?" := leb (at level 70) : nat_scope.
-Infix "<?" := ltb (at level 70) : nat_scope.
-
-Lemma leb_le n m : (n <=? m) = true <-> n <= m.
-Proof.
- revert m.
- induction n. split; auto with arith.
- destruct m; simpl. now split.
- rewrite IHn. split; auto with arith.
-Qed.
-
-Lemma ltb_lt n m : (n <? m) = true <-> n < m.
-Proof.
- unfold ltb, lt. apply leb_le.
-Qed.
-
-Fixpoint pow n m :=
-  match m with
-    | O => 1
-    | S m => n * (pow n m)
-  end.
-
-Infix "^" := pow : nat_scope.
-
-Lemma pow_0_r : forall a, a^0 = 1.
-Proof. reflexivity. Qed.
-
-Lemma pow_succ_r : forall a b, 0<=b -> a^(S b) = a * a^b.
-Proof. reflexivity. Qed.
-
-Definition square n := n * n.
-
-Lemma square_spec n : square n = n * n.
-Proof. reflexivity. Qed.
-
-Definition Even n := exists m, n = 2*m.
-Definition Odd n := exists m, n = 2*m+1.
-
-Fixpoint even n :=
-  match n with
-    | O => true
-    | 1 => false
-    | S (S n') => even n'
-  end.
-
-Definition odd n := negb (even n).
-
-Lemma even_spec : forall n, even n = true <-> Even n.
-Proof.
- fix 1.
-  destruct n as [|[|n]]; simpl; try rewrite even_spec; split.
-  now exists 0.
-  trivial.
-  discriminate.
-  intros (m,H). destruct m. discriminate.
-   simpl in H. rewrite <- plus_n_Sm in H. discriminate.
-  intros (m,H). exists (S m). rewrite H. simpl. now rewrite plus_n_Sm.
-  intros (m,H). destruct m. discriminate. exists m.
-   simpl in H. rewrite <- plus_n_Sm in H. inversion H. reflexivity.
-Qed.
-
-Lemma odd_spec : forall n, odd n = true <-> Odd n.
-Proof.
- unfold odd.
- fix 1.
-  destruct n as [|[|n]]; simpl; try rewrite odd_spec; split.
-  discriminate.
-  intros (m,H). rewrite <- plus_n_Sm in H; discriminate.
-  now exists 0.
-  trivial.
-  intros (m,H). exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m).
-  intros (m,H). destruct m. discriminate. exists m.
-   simpl in H. rewrite <- plus_n_Sm in H. inversion H. simpl.
-   now rewrite <- !plus_n_Sm, <- !plus_n_O.
-Qed.
-
-Lemma Even_equiv : forall n, Even n <-> Even.even n.
-Proof.
- split. intros (p,->). apply Even.even_mult_l. do 3 constructor.
- intros H. destruct (even_2n n H) as (p,->).
- exists p. unfold double. simpl. now rewrite <- plus_n_O.
-Qed.
-
-Lemma Odd_equiv : forall n, Odd n <-> Even.odd n.
-Proof.
- split. intros (p,->). rewrite <- plus_n_Sm, <- plus_n_O.
- apply Even.odd_S. apply Even.even_mult_l. do 3 constructor.
- intros H. destruct (odd_S2n n H) as (p,->).
- exists p. unfold double. simpl. now rewrite <- plus_n_Sm, <- !plus_n_O.
-Qed.
-
-(* A linear, tail-recursive, division for nat.
-
-   In [divmod], [y] is the predecessor of the actual divisor,
-   and [u] is [y] minus the real remainder
-*)
-
-Fixpoint divmod x y q u :=
-  match x with
-    | 0 => (q,u)
-    | S x' => match u with
-                | 0 => divmod x' y (S q) y
-                | S u' => divmod x' y q u'
-              end
-  end.
-
-Definition div x y :=
-  match y with
-    | 0 => y
-    | S y' => fst (divmod x y' 0 y')
-  end.
-
-Definition modulo x y :=
-  match y with
-    | 0 => y
-    | S y' => y' - snd (divmod x y' 0 y')
-  end.
-
-Infix "/" := div : nat_scope.
-Infix "mod" := modulo (at level 40, no associativity) : nat_scope.
-
-Lemma divmod_spec : forall x y q u, u <= y ->
- let (q',u') := divmod x y q u in
- x + (S y)*q + (y-u) = (S y)*q' + (y-u') /\ u' <= y.
-Proof.
- induction x. simpl. intuition.
- intros y q u H. destruct u; simpl divmod.
- generalize (IHx y (S q) y (le_n y)). destruct divmod as (q',u').
- intros (EQ,LE); split; trivial.
- rewrite <- EQ, <- minus_n_O, minus_diag, <- plus_n_O.
- now rewrite !plus_Sn_m, plus_n_Sm, <- plus_assoc, mult_n_Sm.
- generalize (IHx y q u (le_Sn_le _ _ H)). destruct divmod as (q',u').
- intros (EQ,LE); split; trivial.
- rewrite <- EQ.
- rewrite !plus_Sn_m, plus_n_Sm. f_equal. now apply minus_Sn_m.
-Qed.
-
-Lemma div_mod : forall x y, y<>0 -> x = y*(x/y) + x mod y.
-Proof.
- intros x y Hy.
- destruct y; [ now elim Hy | clear Hy ].
- unfold div, modulo.
- generalize (divmod_spec x y 0 y (le_n y)).
- destruct divmod as (q,u).
- intros (U,V).
- simpl in *.
- now rewrite <- mult_n_O, minus_diag, <- !plus_n_O in U.
-Qed.
-
-Lemma mod_bound_pos : forall x y, 0<=x -> 0<y -> 0 <= x mod y < y.
-Proof.
- intros x y Hx Hy. split. auto with arith.
- destruct y; [ now elim Hy | clear Hy ].
- unfold modulo.
- apply le_n_S, le_minus.
-Qed.
-
-(** Square root *)
-
-(** The following square root function is linear (and tail-recursive).
-  With Peano representation, we can't do better. For faster algorithm,
-  see Psqrt/Zsqrt/Nsqrt...
-
-  We search the square root of n = k + p^2 + (q - r)
-  with q = 2p and 0<=r<=q. We start with p=q=r=0, hence
-  looking for the square root of n = k. Then we progressively
-  decrease k and r. When k = S k' and r=0, it means we can use (S p)
-  as new sqrt candidate, since (S k')+p^2+2p = k'+(S p)^2.
-  When k reaches 0, we have found the biggest p^2 square contained
-  in n, hence the square root of n is p.
-*)
-
-Fixpoint sqrt_iter k p q r :=
-  match k with
-    | O => p
-    | S k' => match r with
-                | O => sqrt_iter k' (S p) (S (S q)) (S (S q))
-                | S r' => sqrt_iter k' p q r'
-              end
-  end.
-
-Definition sqrt n := sqrt_iter n 0 0 0.
-
-Lemma sqrt_iter_spec : forall k p q r,
- q = p+p -> r<=q ->
- let s := sqrt_iter k p q r in
- s*s <= k + p*p + (q - r) < (S s)*(S s).
-Proof.
- induction k.
- (* k = 0 *)
- simpl; intros p q r Hq Hr.
- split.
- apply le_plus_l.
- apply le_lt_n_Sm.
- rewrite <- mult_n_Sm.
- rewrite plus_assoc, (plus_comm p), <- plus_assoc.
- apply plus_le_compat; trivial.
- rewrite <- Hq. apply le_minus.
- (* k = S k' *)
- destruct r.
- (* r = 0 *)
- intros Hq _.
- replace (S k + p*p + (q-0)) with (k + (S p)*(S p) + (S (S q) - S (S q))).
- apply IHk.
- simpl. rewrite <- plus_n_Sm. congruence.
- auto with arith.
- rewrite minus_diag, <- minus_n_O, <- plus_n_O. simpl.
- rewrite <- plus_n_Sm; f_equal. rewrite <- plus_assoc; f_equal.
- rewrite <- mult_n_Sm, (plus_comm p), <- plus_assoc. congruence.
- (* r = S r' *)
- intros Hq Hr.
- replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)).
- apply IHk; auto with arith.
- simpl. rewrite plus_n_Sm. f_equal. rewrite minus_Sn_m; auto.
-Qed.
-
-Lemma sqrt_spec : forall n,
- (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n).
-Proof.
- intros.
- set (s:=sqrt n).
- replace n with (n + 0*0 + (0-0)).
- apply sqrt_iter_spec; auto.
- simpl. now rewrite <- 2 plus_n_O.
-Qed.
-
-(** A linear tail-recursive base-2 logarithm
-
-  In [log2_iter], we maintain the logarithm [p] of the counter [q],
-  while [r] is the distance between [q] and the next power of 2,
-  more precisely [q + S r = 2^(S p)] and [r<2^p]. At each
-  recursive call, [q] goes up while [r] goes down. When [r]
-  is 0, we know that [q] has almost reached a power of 2,
-  and we increase [p] at the next call, while resetting [r]
-  to [q].
-
-  Graphically (numbers are [q], stars are [r]) :
-
-<<
-                    10
-                  9
-                8
-              7   *
-            6       *
-          5           ...
-        4
-      3   *
-    2       *
-  1   *       *
-0   *   *       *
->>
-
-  We stop when [k], the global downward counter reaches 0.
-  At that moment, [q] is the number we're considering (since
-  [k+q] is invariant), and [p] its logarithm.
-*)
-
-Fixpoint log2_iter k p q r :=
-  match k with
-    | O => p
-    | S k' => match r with
-                | O => log2_iter k' (S p) (S q) q
-                | S r' => log2_iter k' p (S q) r'
-              end
-  end.
-
-Definition log2 n := log2_iter (pred n) 0 1 0.
-
-Lemma log2_iter_spec : forall k p q r,
- 2^(S p) = q + S r -> r < 2^p ->
- let s := log2_iter k p q r in
- 2^s <= k + q < 2^(S s).
-Proof.
- induction k.
- (* k = 0 *)
- intros p q r EQ LT. simpl log2_iter. cbv zeta.
- split.
- rewrite plus_O_n.
- apply plus_le_reg_l with (2^p).
- simpl pow in EQ. rewrite <- plus_n_O in EQ. rewrite EQ.
- rewrite plus_comm. apply plus_le_compat_r. now apply lt_le_S.
- rewrite EQ, plus_comm. apply plus_lt_compat_l. apply lt_0_Sn.
- (* k = S k' *)
- intros p q r EQ LT. destruct r.
- (* r = 0 *)
- rewrite <- plus_n_Sm, <- plus_n_O in EQ.
- rewrite plus_Sn_m, plus_n_Sm. apply IHk.
- rewrite <- EQ. remember (S p) as p'; simpl. now rewrite <- plus_n_O.
- unfold lt. now rewrite EQ.
- (* r = S r' *)
- rewrite plus_Sn_m, plus_n_Sm. apply IHk.
- now rewrite plus_Sn_m, plus_n_Sm.
- unfold lt.
- now apply lt_le_weak.
-Qed.
-
-Lemma log2_spec : forall n, 0<n ->
- 2^(log2 n) <= n < 2^(S (log2 n)).
-Proof.
- intros.
- set (s:=log2 n).
- replace n with (pred n + 1).
- apply log2_iter_spec; auto.
- rewrite <- plus_n_Sm, <- plus_n_O.
- symmetry. now apply S_pred with 0.
-Qed.
-
-Lemma log2_nonpos : forall n, n<=0 -> log2 n = 0.
-Proof.
- inversion 1; now subst.
-Qed.
-
-(** * Gcd *)
-
-(** We use Euclid algorithm, which is normally not structural,
-    but Coq is now clever enough to accept this (behind modulo
-    there is a subtraction, which now preserves being a subterm)
-*)
-
-Fixpoint gcd a b :=
-  match a with
-   | O => b
-   | S a' => gcd (b mod (S a')) (S a')
-  end.
-
-Definition divide x y := exists z, y=z*x.
-Notation "( x | y )" := (divide x y) (at level 0) : nat_scope.
-
-Lemma gcd_divide : forall a b, (gcd a b | a) /\ (gcd a b | b).
-Proof.
- fix 1.
- intros [|a] b; simpl.
- split.
-  now exists 0.
-  exists 1. simpl. now rewrite <- plus_n_O.
- fold (b mod (S a)).
- destruct (gcd_divide (b mod (S a)) (S a)) as (H,H').
- set (a':=S a) in *.
- split; auto.
- rewrite (div_mod b a') at 2 by discriminate.
- destruct H as (u,Hu), H' as (v,Hv).
- rewrite mult_comm.
- exists ((b/a')*v + u).
- rewrite mult_plus_distr_r.
- now rewrite <- mult_assoc, <- Hv, <- Hu.
-Qed.
-
-Lemma gcd_divide_l : forall a b, (gcd a b | a).
-Proof.
- intros. apply gcd_divide.
-Qed.
-
-Lemma gcd_divide_r : forall a b, (gcd a b | b).
-Proof.
- intros. apply gcd_divide.
-Qed.
-
-Lemma gcd_greatest : forall a b c, (c|a) -> (c|b) -> (c|gcd a b).
-Proof.
- fix 1.
- intros [|a] b; simpl; auto.
- fold (b mod (S a)).
- intros c H H'. apply gcd_greatest; auto.
- set (a':=S a) in *.
- rewrite (div_mod b a') in H' by discriminate.
- destruct H as (u,Hu), H' as (v,Hv).
- exists (v - (b/a')*u).
- rewrite mult_comm in Hv.
- now rewrite mult_minus_distr_r, <- Hv, <-mult_assoc, <-Hu, minus_plus.
-Qed.
-
-(** * Bitwise operations *)
-
-(** We provide here some bitwise operations for unary numbers.
-  Some might be really naive, they are just there for fullfiling
-  the same interface as other for natural representations. As
-  soon as binary representations such as NArith are available,
-  it is clearly better to convert to/from them and use their ops.
-*)
-
-Fixpoint testbit a n :=
- match n with
-   | O => odd a
-   | S n => testbit (div2 a) n
- end.
-
-Definition shiftl a n := iter_nat n _ double a.
-Definition shiftr a n := iter_nat n _ div2 a.
-
-Fixpoint bitwise (op:bool->bool->bool) n a b :=
- match n with
-  | O => O
-  | S n' =>
-    (if op (odd a) (odd b) then 1 else 0) +
-    2*(bitwise op n' (div2 a) (div2 b))
- end.
-
-Definition land a b := bitwise andb a a b.
-Definition lor a b := bitwise orb (max a b) a b.
-Definition ldiff a b := bitwise (fun b b' => b && negb b') a a b.
-Definition lxor a b := bitwise xorb (max a b) a b.
-
-Lemma double_twice : forall n, double n = 2*n.
-Proof.
- simpl; intros. now rewrite <- plus_n_O.
-Qed.
-
-Lemma testbit_0_l : forall n, testbit 0 n = false.
-Proof.
- now induction n.
-Qed.
-
-Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.
-Proof.
- unfold testbit. rewrite odd_spec. now exists a.
-Qed.
-
-Lemma testbit_even_0 a : testbit (2*a) 0 = false.
-Proof.
- unfold testbit, odd. rewrite (proj2 (even_spec _)); trivial.
- now exists a.
-Qed.
-
-Lemma testbit_odd_succ a n : testbit (2*a+1) (S n) = testbit a n.
-Proof.
- unfold testbit; fold testbit.
- rewrite <- plus_n_Sm, <- plus_n_O. f_equal.
- apply div2_double_plus_one.
-Qed.
-
-Lemma testbit_even_succ a n : testbit (2*a) (S n) = testbit a n.
-Proof.
- unfold testbit; fold testbit. f_equal. apply div2_double.
-Qed.
-
-Lemma shiftr_spec : forall a n m,
- testbit (shiftr a n) m = testbit a (m+n).
-Proof.
- induction n; intros m. trivial.
- now rewrite <- plus_n_O.
- now rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn.
-Qed.
-
-Lemma shiftl_spec_high : forall a n m, n<=m ->
- testbit (shiftl a n) m = testbit a (m-n).
-Proof.
- induction n; intros m H. trivial.
- now rewrite <- minus_n_O.
- destruct m. inversion H.
- simpl. apply le_S_n in H.
- change (shiftl a (S n)) with (double (shiftl a n)).
- rewrite double_twice, div2_double. now apply IHn.
-Qed.
-
-Lemma shiftl_spec_low : forall a n m, m<n ->
- testbit (shiftl a n) m = false.
-Proof.
- induction n; intros m H. inversion H.
- change (shiftl a (S n)) with (double (shiftl a n)).
- destruct m; simpl.
- unfold odd. apply negb_false_iff.
- apply even_spec. exists (shiftl a n). apply double_twice.
- rewrite double_twice, div2_double. apply IHn.
- now apply lt_S_n.
-Qed.
-
-Lemma div2_bitwise : forall op n a b,
- div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).
-Proof.
- intros. unfold bitwise; fold bitwise.
- destruct (op (odd a) (odd b)).
- now rewrite div2_double_plus_one.
- now rewrite plus_O_n, div2_double.
-Qed.
-
-Lemma odd_bitwise : forall op n a b,
- odd (bitwise op (S n) a b) = op (odd a) (odd b).
-Proof.
- intros. unfold bitwise; fold bitwise.
- destruct (op (odd a) (odd b)).
- apply odd_spec. rewrite plus_comm. eexists; eauto.
- unfold odd. apply negb_false_iff. apply even_spec.
- rewrite plus_O_n; eexists; eauto.
-Qed.
-
-Lemma div2_decr : forall a n, a <= S n -> div2 a <= n.
-Proof.
- destruct a; intros. apply le_0_n.
- apply le_trans with a.
- apply lt_n_Sm_le, lt_div2, lt_0_Sn. now apply le_S_n.
-Qed.
-
-Lemma testbit_bitwise_1 : forall op, (forall b, op false b = false) ->
- forall n m a b, a<=n ->
- testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
-Proof.
- intros op Hop.
- induction n; intros m a b Ha.
- simpl. inversion Ha; subst. now rewrite testbit_0_l.
- destruct m.
- apply odd_bitwise.
- unfold testbit; fold testbit. rewrite div2_bitwise.
- apply IHn; now apply div2_decr.
-Qed.
-
-Lemma testbit_bitwise_2 : forall op, op false false = false ->
- forall n m a b, a<=n -> b<=n ->
- testbit (bitwise op n a b) m = op (testbit a m) (testbit b m).
-Proof.
- intros op Hop.
- induction n; intros m a b Ha Hb.
- simpl. inversion Ha; inversion Hb; subst. now rewrite testbit_0_l.
- destruct m.
- apply odd_bitwise.
- unfold testbit; fold testbit. rewrite div2_bitwise.
- apply IHn; now apply div2_decr.
-Qed.
-
-Lemma land_spec : forall a b n,
- testbit (land a b) n = testbit a n && testbit b n.
-Proof.
- intros. unfold land. apply testbit_bitwise_1; trivial.
-Qed.
-
-Lemma ldiff_spec : forall a b n,
- testbit (ldiff a b) n = testbit a n && negb (testbit b n).
-Proof.
- intros. unfold ldiff. apply testbit_bitwise_1; trivial.
-Qed.
-
-Lemma lor_spec : forall a b n,
- testbit (lor a b) n = testbit a n || testbit b n.
-Proof.
- intros. unfold lor. apply testbit_bitwise_2. trivial.
- destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l.
- destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l.
-Qed.
-
-Lemma lxor_spec : forall a b n,
- testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
-Proof.
- intros. unfold lxor. apply testbit_bitwise_2. trivial.
- destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l.
- destruct (le_ge_dec a b). now rewrite max_r. now rewrite max_l.
-Qed.
-
-(** * Implementation of [NAxiomsSig] by [nat] *)
-
-Module Nat
- <: NAxiomsSig <: UsualDecidableTypeFull <: OrderedTypeFull <: TotalOrder.
-
-(** Bi-directional induction. *)
-
-Theorem bi_induction :
-  forall A : nat -> Prop, Proper (eq==>iff) A ->
-    A 0 -> (forall n : nat, A n <-> A (S n)) -> forall n : nat, A n.
-Proof.
-intros A A_wd A0 AS. apply nat_ind. assumption. intros; now apply -> AS.
-Qed.
-
-(** Basic operations. *)
-
-Definition eq_equiv : Equivalence (@eq nat) := eq_equivalence.
-Local Obligation Tactic := simpl_relation.
-Program Instance succ_wd : Proper (eq==>eq) S.
-Program Instance pred_wd : Proper (eq==>eq) pred.
-Program Instance add_wd : Proper (eq==>eq==>eq) plus.
-Program Instance sub_wd : Proper (eq==>eq==>eq) minus.
-Program Instance mul_wd : Proper (eq==>eq==>eq) mult.
-
-Theorem pred_succ : forall n : nat, pred (S n) = n.
-Proof.
-reflexivity.
-Qed.
-
-Theorem one_succ : 1 = S 0.
-Proof.
-reflexivity.
-Qed.
-
-Theorem two_succ : 2 = S 1.
-Proof.
-reflexivity.
-Qed.
-
-Theorem add_0_l : forall n : nat, 0 + n = n.
-Proof.
-reflexivity.
-Qed.
-
-Theorem add_succ_l : forall n m : nat, (S n) + m = S (n + m).
-Proof.
-reflexivity.
-Qed.
-
-Theorem sub_0_r : forall n : nat, n - 0 = n.
-Proof.
-intro n; now destruct n.
-Qed.
-
-Theorem sub_succ_r : forall n m : nat, n - (S m) = pred (n - m).
-Proof.
-induction n; destruct m; simpl; auto. apply sub_0_r.
-Qed.
-
-Theorem mul_0_l : forall n : nat, 0 * n = 0.
-Proof.
-reflexivity.
-Qed.
-
-Theorem mul_succ_l : forall n m : nat, S n * m = n * m + m.
-Proof.
-assert (add_S_r : forall n m, n+S m = S(n+m)) by (induction n; auto).
-assert (add_comm : forall n m, n+m = m+n).
- induction n; simpl; auto. intros; rewrite add_S_r; auto.
-intros n m; now rewrite add_comm.
-Qed.
-
-(** Order on natural numbers *)
-
-Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
-
-Theorem lt_succ_r : forall n m : nat, n < S m <-> n <= m.
-Proof.
-unfold lt; split. apply le_S_n. induction 1; auto.
-Qed.
-
-
-Theorem lt_eq_cases : forall n m : nat, n <= m <-> n < m \/ n = m.
-Proof.
-split.
-inversion 1; auto. rewrite lt_succ_r; auto.
-destruct 1; [|subst; auto]. rewrite <- lt_succ_r; auto.
-Qed.
-
-Theorem lt_irrefl : forall n : nat, ~ (n < n).
-Proof.
-induction n. intro H; inversion H. rewrite lt_succ_r; auto.
-Qed.
-
-(** Facts specific to natural numbers, not integers. *)
-
-Theorem pred_0 : pred 0 = 0.
-Proof.
-reflexivity.
-Qed.
-
-(** Recursion fonction *)
-
-Definition recursion {A} : A -> (nat -> A -> A) -> nat -> A :=
-  nat_rect (fun _ => A).
-
-Instance recursion_wd {A} (Aeq : relation A) :
- Proper (Aeq ==> (eq==>Aeq==>Aeq) ==> eq ==> Aeq) recursion.
-Proof.
-intros a a' Ha f f' Hf n n' Hn. subst n'.
-induction n; simpl; auto. apply Hf; auto.
-Qed.
-
-Theorem recursion_0 :
-  forall {A} (a : A) (f : nat -> A -> A), recursion a f 0 = a.
-Proof.
-reflexivity.
-Qed.
-
-Theorem recursion_succ :
-  forall {A} (Aeq : relation A) (a : A) (f : nat -> A -> A),
-    Aeq a a -> Proper (eq==>Aeq==>Aeq) f ->
-      forall n : nat, Aeq (recursion a f (S n)) (f n (recursion a f n)).
-Proof.
-unfold Proper, respectful in *; induction n; simpl; auto.
-Qed.
-
-(** The instantiation of operations.
-    Placing them at the very end avoids having indirections in above lemmas. *)
-
-Definition t := nat.
-Definition eq := @eq nat.
-Definition eqb := beq_nat.
-Definition compare := nat_compare.
-Definition zero := 0.
-Definition one := 1.
-Definition two := 2.
-Definition succ := S.
-Definition pred := pred.
-Definition add := plus.
-Definition sub := minus.
-Definition mul := mult.
-Definition lt := lt.
-Definition le := le.
-Definition ltb := ltb.
-Definition leb := leb.
-
-Definition min := min.
-Definition max := max.
-Definition max_l := max_l.
-Definition max_r := max_r.
-Definition min_l := min_l.
-Definition min_r := min_r.
-
-Definition eqb_eq := beq_nat_true_iff.
-Definition compare_spec := nat_compare_spec.
-Definition eq_dec := eq_nat_dec.
-Definition leb_le := leb_le.
-Definition ltb_lt := ltb_lt.
-
-Definition Even := Even.
-Definition Odd := Odd.
-Definition even := even.
-Definition odd := odd.
-Definition even_spec := even_spec.
-Definition odd_spec := odd_spec.
-
-Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
-Definition pow_0_r := pow_0_r.
-Definition pow_succ_r := pow_succ_r.
-Lemma pow_neg_r : forall a b, b<0 -> a^b = 0. inversion 1. Qed.
-Definition pow := pow.
-
-Definition square := square.
-Definition square_spec := square_spec.
-
-Definition log2_spec := log2_spec.
-Definition log2_nonpos := log2_nonpos.
-Definition log2 := log2.
-
-Definition sqrt_spec a (Ha:0<=a) := sqrt_spec a.
-Lemma sqrt_neg : forall a, a<0 -> sqrt a = 0. inversion 1. Qed.
-Definition sqrt := sqrt.
-
-Definition div := div.
-Definition modulo := modulo.
-Program Instance div_wd : Proper (eq==>eq==>eq) div.
-Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
-Definition div_mod := div_mod.
-Definition mod_bound_pos := mod_bound_pos.
-
-Definition divide := divide.
-Definition gcd := gcd.
-Definition gcd_divide_l := gcd_divide_l.
-Definition gcd_divide_r := gcd_divide_r.
-Definition gcd_greatest := gcd_greatest.
-Lemma gcd_nonneg : forall a b, 0<=gcd a b.
-Proof. intros. apply le_O_n. Qed.
-
-Definition testbit := testbit.
-Definition shiftl := shiftl.
-Definition shiftr := shiftr.
-Definition lxor := lxor.
-Definition land := land.
-Definition lor := lor.
-Definition ldiff := ldiff.
-Definition div2 := div2.
-
-Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
-Definition testbit_odd_0 := testbit_odd_0.
-Definition testbit_even_0 := testbit_even_0.
-Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ a n.
-Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ a n.
-Lemma testbit_neg_r a n (H:n<0) : testbit a n = false.
-Proof. inversion H. Qed.
-Definition shiftl_spec_low := shiftl_spec_low.
-Definition shiftl_spec_high a n m (_:0<=m) := shiftl_spec_high a n m.
-Definition shiftr_spec a n m (_:0<=m) := shiftr_spec a n m.
-Definition lxor_spec := lxor_spec.
-Definition land_spec := land_spec.
-Definition lor_spec := lor_spec.
-Definition ldiff_spec := ldiff_spec.
-Definition div2_spec a : div2 a = shiftr a 1 := eq_refl _.
-
-(** Generic Properties *)
-
-Include NProp
- <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
-
-End Nat.
-
-Bind Scope nat_scope with Nat.t nat.
-
-(** [Nat] contains an [order] tactic for natural numbers *)
-
-(** Note that [Nat.order] is domain-agnostic: it will not prove
-    [1<=2] or [x<=x+x], but rather things like [x<=y -> y<=x -> x=y]. *)
-
-Section TestOrder.
- Let test : forall x y, x<=y -> y<=x -> x=y.
- Proof.
- Nat.order.
- Qed.
-End TestOrder.
+Module Nat <: NAxiomsSig := Nat.