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.

1 files changed, 755 insertions, 0 deletions

diff --git a/theories/Arith/PeanoNat.v b/theories/Arith/PeanoNat.v
new file mode 100644
index 000000000..3657d9544
--- /dev/null
+++ b/theories/Arith/PeanoNat.v
@@ -0,0 +1,755 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+(*                      Evgeny Makarov, INRIA, 2007                     *)
+(************************************************************************)
+
+Require Import NAxioms NProperties OrdersFacts.
+
+(** Implementation of [NAxiomsSig] by [nat] *)
+
+Module Nat
+ <: NAxiomsSig
+ <: UsualDecidableTypeFull
+ <: OrderedTypeFull
+ <: TotalOrder.
+
+(** Operations over [nat] are defined in a separate module *)
+
+Include Coq.Init.Nat.
+
+(** When including property functors, inline t eq zero one two lt le succ *)
+
+Set Inline Level 50.
+
+(** All operations are well-defined (trivial here since eq is Leibniz) *)
+
+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.
+Program Instance pow_wd : Proper (eq==>eq==>eq) pow.
+Program Instance div_wd : Proper (eq==>eq==>eq) div.
+Program Instance mod_wd : Proper (eq==>eq==>eq) modulo.
+Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
+Program Instance testbit_wd : Proper (eq==>eq==>eq) testbit.
+
+(** 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.
+
+(** 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.
+
+(** ** Remaining constants not defined in Coq.Init.Nat *)
+
+(** NB: Aliasing [le] is mandatory, since only a Definition can implement
+    an interface Parameter... *)
+
+Definition eq := @Logic.eq nat.
+Definition le := Peano.le.
+Definition lt := Peano.lt.
+
+(** ** Basic specifications : pred add sub mul *)
+
+Lemma pred_succ n : pred (S n) = n.
+Proof.
+reflexivity.
+Qed.
+
+Lemma pred_0 : pred 0 = 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma one_succ : 1 = S 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma two_succ : 2 = S 1.
+Proof.
+reflexivity.
+Qed.
+
+Lemma add_0_l n : 0 + n = n.
+Proof.
+reflexivity.
+Qed.
+
+Lemma add_succ_l n m : (S n) + m = S (n + m).
+Proof.
+reflexivity.
+Qed.
+
+Lemma sub_0_r n : n - 0 = n.
+Proof.
+now destruct n.
+Qed.
+
+Lemma sub_succ_r n m : n - (S m) = pred (n - m).
+Proof.
+revert m. induction n; destruct m; simpl; auto. apply sub_0_r.
+Qed.
+
+Lemma mul_0_l n : 0 * n = 0.
+Proof.
+reflexivity.
+Qed.
+
+Lemma mul_succ_l n m : S n * m = n * m + m.
+Proof.
+assert (succ_r : forall x y, x+S y = S(x+y)) by now induction x.
+assert (comm : forall x y, x+y = y+x).
+{ induction x; simpl; auto. intros; rewrite succ_r; now f_equal. }
+now rewrite comm.
+Qed.
+
+Lemma lt_succ_r n m : n < S m <-> n <= m.
+Proof.
+split. apply Peano.le_S_n. induction 1; auto.
+Qed.
+
+(** ** Boolean comparisons *)
+
+Lemma eqb_eq n m : eqb n m = true <-> n = m.
+Proof.
+ revert m.
+ induction n; destruct m; simpl; rewrite ?IHn; split; try easy.
+ - now intros ->.
+ - now injection 1.
+Qed.
+
+Lemma leb_le n m : (n <=? m) = true <-> n <= m.
+Proof.
+ revert m.
+ induction n; destruct m; simpl.
+ - now split.
+ - split; trivial. intros; apply Peano.le_0_n.
+ - now split.
+ - rewrite IHn; split.
+   + apply Peano.le_n_S.
+   + apply Peano.le_S_n.
+Qed.
+
+Lemma ltb_lt n m : (n <? m) = true <-> n < m.
+Proof.
+ apply leb_le.
+Qed.
+
+(** ** Decidability of equality over [nat]. *)
+
+Lemma eq_dec : forall n m : nat, {n = m} + {n <> m}.
+Proof.
+  induction n; destruct m.
+  - now left.
+  - now right.
+  - now right.
+  - destruct (IHn m); [left|right]; auto.
+Defined.
+
+(** ** Ternary comparison *)
+
+(** With [nat], it would be easier to prove first [compare_spec],
+    then the properties below. But then we wouldn't be able to
+    benefit from functor [BoolOrderFacts] *)
+
+Lemma compare_eq_iff n m : (n ?= m) = Eq <-> n = m.
+Proof.
+ revert m; induction n; destruct m; simpl; rewrite ?IHn; split; auto; easy.
+Qed.
+
+Lemma compare_lt_iff n m : (n ?= m) = Lt <-> n < m.
+Proof.
+ revert m; induction n; destruct m; simpl; rewrite ?IHn; split; try easy.
+ - intros _. apply Peano.le_n_S, Peano.le_0_n.
+ - apply Peano.le_n_S.
+ - apply Peano.le_S_n.
+Qed.
+
+Lemma compare_le_iff n m : (n ?= m) <> Gt <-> n <= m.
+Proof.
+ revert m; induction n; destruct m; simpl; rewrite ?IHn.
+ - now split.
+ - split; intros. apply Peano.le_0_n. easy.
+ - split. now destruct 1. inversion 1.
+ - split; intros. now apply Peano.le_n_S. now apply Peano.le_S_n.
+Qed.
+
+Lemma compare_antisym n m : (m ?= n) = CompOpp (n ?= m).
+Proof.
+ revert m; induction n; destruct m; simpl; trivial.
+Qed.
+
+Lemma compare_succ n m : (S n ?= S m) = (n ?= m).
+Proof.
+ reflexivity.
+Qed.
+
+
+(* BUG: Ajout d'un cas * après preuve finie (deuxième niveau +++*** ) :
+    *  --->   Anomaly: Uncaught exception Proofview.IndexOutOfRange(_). Please report. *)
+
+(** ** Minimum, maximum *)
+
+Lemma max_l : forall n m, m <= n -> max n m = n.
+Proof.
+ exact Peano.max_l.
+Qed.
+
+Lemma max_r : forall n m, n <= m -> max n m = m.
+Proof.
+ exact Peano.max_r.
+Qed.
+
+Lemma min_l : forall n m, n <= m -> min n m = n.
+Proof.
+ exact Peano.min_l.
+Qed.
+
+Lemma min_r : forall n m, m <= n -> min n m = m.
+Proof.
+ exact Peano.min_r.
+Qed.
+
+(** Some more advanced properties of comparison and orders,
+    including [compare_spec] and [lt_irrefl] and [lt_eq_cases]. *)
+
+Include BoolOrderFacts.
+
+(** We can now derive all properties of basic functions and orders,
+    and use these properties for proving the specs of more advanced
+    functions. *)
+
+Include NBasicProp <+ UsualMinMaxLogicalProperties <+ UsualMinMaxDecProperties.
+
+(** ** Power *)
+
+Lemma pow_neg_r a b : b<0 -> a^b = 0. inversion 1. Qed.
+
+Lemma pow_0_r a : a^0 = 1.
+Proof. reflexivity. Qed.
+
+Lemma pow_succ_r a b : 0<=b -> a^(S b) = a * a^b.
+Proof. reflexivity. Qed.
+
+(** ** Square *)
+
+Lemma square_spec n : square n = n * n.
+Proof. reflexivity. Qed.
+
+(** ** Parity *)
+
+Definition Even n := exists m, n = 2*m.
+Definition Odd n := exists m, n = 2*m+1.
+
+Module Private_Parity.
+
+Lemma Even_1 : ~ Even 1.
+Proof.
+ intros ([|], H); try discriminate.
+ simpl in H. now rewrite <- plus_n_Sm in H.
+Qed.
+
+Lemma Even_2 n : Even n <-> Even (S (S n)).
+Proof.
+ split; intros (m,H).
+ - exists (S m). rewrite H. simpl. now rewrite plus_n_Sm.
+ - destruct m; try discriminate.
+   exists m. simpl in H. rewrite <- plus_n_Sm in H. now inversion H.
+Qed.
+
+Lemma Odd_0 : ~ Odd 0.
+Proof.
+ now intros ([|], H).
+Qed.
+
+Lemma Odd_2 n : Odd n <-> Odd (S (S n)).
+Proof.
+ split; intros (m,H).
+ - exists (S m). rewrite H. simpl. now rewrite <- (plus_n_Sm m).
+ - destruct m; try discriminate.
+   exists m. simpl in H. rewrite <- plus_n_Sm in H. inversion H.
+   simpl. now rewrite <- !plus_n_Sm, <- !plus_n_O.
+Qed.
+
+End Private_Parity.
+Import Private_Parity.
+
+Lemma even_spec : forall n, even n = true <-> Even n.
+Proof.
+ fix 1.
+  destruct n as [|[|n]]; simpl.
+  - split; [ now exists 0 | trivial ].
+  - split; [ discriminate | intro H; elim (Even_1 H) ].
+  - rewrite even_spec. apply Even_2.
+Qed.
+
+Lemma odd_spec : forall n, odd n = true <-> Odd n.
+Proof.
+ unfold odd.
+ fix 1.
+  destruct n as [|[|n]]; simpl.
+  - split; [ discriminate | intro H; elim (Odd_0 H) ].
+  - split; [ now exists 0 | trivial ].
+  - rewrite odd_spec. apply Odd_2.
+Qed.
+
+(** ** Division *)
+
+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, sub_0_r, sub_diag, add_0_r.
+     now rewrite !add_succ_l, <- add_succ_r, <- add_assoc, mul_succ_r.
+   + assert (H' : u <= y).
+     { apply le_trans with (S u); trivial. do 2 constructor. }
+     generalize (IHx y q u H'). destruct divmod as (q',u').
+     intros (EQ,LE); split; trivial.
+     rewrite <- EQ.
+     rewrite !add_succ_l, <- add_succ_r. f_equal. now rewrite <- sub_succ_l.
+Qed.
+
+Lemma div_mod x y : y<>0 -> x = y*(x/y) + x mod y.
+Proof.
+ intros 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 mul_0_r, sub_diag, !add_0_r in U.
+Qed.
+
+Lemma mod_bound_pos x y : 0<=x -> 0<y -> 0 <= x mod y < y.
+Proof.
+ intros Hx Hy. split. apply le_0_l.
+ destruct y; [ now elim Hy | clear Hy ].
+ unfold modulo.
+ apply lt_succ_r, le_sub_l.
+Qed.
+
+(** ** Square root *)
+
+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_add_r.
+   + apply lt_succ_r.
+     rewrite mul_succ_r.
+     rewrite add_assoc, (add_comm p), <- add_assoc.
+     apply add_le_mono_l.
+     rewrite <- Hq. apply le_sub_l.
+ - (* 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. now rewrite add_succ_r, Hq. apply le_n.
+     * rewrite sub_diag, sub_0_r, add_0_r. simpl.
+       rewrite add_succ_r; f_equal. rewrite <- add_assoc; f_equal.
+       rewrite mul_succ_r, (add_comm p), <- add_assoc. now f_equal.
+   + (* r = S r' *)
+     intros Hq Hr.
+     replace (S k + p*p + (q-S r)) with (k + p*p + (q - r)).
+     * apply IHk; trivial. apply le_trans with (S r); trivial. do 2 constructor.
+     * simpl. rewrite <- add_succ_r. f_equal. rewrite <- sub_succ_l; trivial.
+Qed.
+
+Lemma sqrt_specif n : (sqrt n)*(sqrt n) <= n < S (sqrt n) * S (sqrt n).
+Proof.
+ set (s:=sqrt n).
+ replace n with (n + 0*0 + (0-0)).
+ apply sqrt_iter_spec; auto.
+ simpl. now rewrite !add_0_r.
+Qed.
+
+Definition sqrt_spec a (Ha:0<=a) := sqrt_specif a.
+
+Lemma sqrt_neg a : a<0 -> sqrt a = 0.
+Proof. inversion 1. Qed.
+
+(** ** Logarithm *)
+
+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 add_0_l.
+     rewrite (add_le_mono_l _ _ (2^p)).
+     simpl pow in EQ. rewrite add_0_r in EQ. rewrite EQ.
+     rewrite add_comm. apply add_le_mono_r. apply LT.
+   + rewrite EQ, add_comm. apply add_lt_mono_l.
+     apply lt_succ_r, le_0_l.
+ - (* k = S k' *)
+   intros p q r EQ LT. destruct r.
+   + (* r = 0 *)
+     rewrite add_succ_r, add_0_r in EQ.
+     rewrite add_succ_l, <- add_succ_r. apply IHk.
+     * rewrite <- EQ. remember (S p) as p'; simpl. now rewrite add_0_r.
+     * rewrite EQ. constructor.
+   + (* r = S r' *)
+     rewrite add_succ_l, <- add_succ_r. apply IHk.
+     * now rewrite add_succ_l, <- add_succ_r.
+     * apply le_lt_trans with (S r); trivial. do 2 constructor.
+Qed.
+
+Lemma log2_spec 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 add_1_r.
+ apply succ_pred. now apply neq_sym, lt_neq.
+Qed.
+
+Lemma log2_nonpos n : n<=0 -> log2 n = 0.
+Proof.
+ inversion 1; now subst.
+Qed.
+
+(** ** Gcd *)
+
+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 mul_comm.
+ exists ((b/a')*v + u).
+ rewrite mul_add_distr_r.
+ now rewrite <- mul_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 mul_comm in Hv.
+ rewrite mul_sub_distr_r, <- Hv, <- mul_assoc, <-Hu.
+ now rewrite add_comm, add_sub.
+Qed.
+
+Lemma gcd_nonneg a b : 0<=gcd a b.
+Proof. apply le_0_l. Qed.
+
+
+(** ** Bitwise operations *)
+
+Lemma div2_double n : div2 (2*n) = n.
+Proof.
+ induction n; trivial.
+ simpl mul. rewrite add_succ_r. simpl. now f_equal.
+Qed.
+
+Lemma div2_succ_double n : div2 (S (2*n)) = n.
+Proof.
+ induction n; trivial.
+ simpl. f_equal. now rewrite add_succ_r.
+Qed.
+
+Lemma le_div2 n : div2 (S n) <= n.
+Proof.
+ revert n.
+ fix 1.
+ destruct n; simpl; trivial. apply lt_succ_r.
+ destruct n; [simpl|]; trivial. now constructor.
+Qed.
+
+Lemma lt_div2 n : 0 < n -> div2 n < n.
+Proof.
+ destruct n.
+ - inversion 1.
+ - intros _. apply lt_succ_r, le_div2.
+Qed.
+
+Lemma div2_decr a n : a <= S n -> div2 a <= n.
+Proof.
+ destruct a; intros H.
+ - simpl. apply le_0_l.
+ - apply succ_le_mono in H.
+   apply le_trans with a; [ apply le_div2 | trivial ].
+Qed.
+
+Lemma double_twice : forall n, double n = 2*n.
+Proof.
+ simpl; intros. now rewrite add_0_r.
+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 add_1_r. f_equal.
+ apply div2_succ_double.
+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_specif : forall a n m,
+ testbit (shiftr a n) m = testbit a (m+n).
+Proof.
+ induction n; intros m. trivial.
+ now rewrite add_0_r.
+ now rewrite add_succ_r, <- add_succ_l, <- IHn.
+Qed.
+
+Lemma shiftl_specif_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 sub_0_r.
+ destruct m. inversion H.
+ simpl. apply succ_le_mono 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 succ_le_mono.
+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_succ_double.
+ now rewrite add_0_l, 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 add_comm. eexists; eauto.
+ unfold odd. apply negb_false_iff. apply even_spec.
+ rewrite add_0_l; eexists; eauto.
+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 a b n :
+ testbit (land a b) n = testbit a n && testbit b n.
+Proof.
+ unfold land. apply testbit_bitwise_1; trivial.
+Qed.
+
+Lemma ldiff_spec a b n :
+ testbit (ldiff a b) n = testbit a n && negb (testbit b n).
+Proof.
+ unfold ldiff. apply testbit_bitwise_1; trivial.
+Qed.
+
+Lemma lor_spec a b n :
+ testbit (lor a b) n = testbit a n || testbit b n.
+Proof.
+ unfold lor. apply testbit_bitwise_2.
+ - trivial.
+ - destruct (compare_spec a b).
+   + rewrite max_l; subst; trivial.
+   + apply lt_le_incl in H. now rewrite max_r.
+   + apply lt_le_incl in H. now rewrite max_l.
+ - destruct (compare_spec a b).
+   + rewrite max_r; subst; trivial.
+   + apply lt_le_incl in H. now rewrite max_r.
+   + apply lt_le_incl in H. now rewrite max_l.
+Qed.
+
+Lemma lxor_spec a b n :
+ testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
+Proof.
+ unfold lxor. apply testbit_bitwise_2.
+ - trivial.
+ - destruct (compare_spec a b).
+   + rewrite max_l; subst; trivial.
+   + apply lt_le_incl in H. now rewrite max_r.
+   + apply lt_le_incl in H. now rewrite max_l.
+ - destruct (compare_spec a b).
+   + rewrite max_r; subst; trivial.
+   + apply lt_le_incl in H. now rewrite max_r.
+   + apply lt_le_incl in H. now rewrite max_l.
+Qed.
+
+Lemma div2_spec a : div2 a = shiftr a 1.
+Proof.
+ reflexivity.
+Qed.
+
+(** Aliases with extra dummy hypothesis, to fulfil the interface *)
+
+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_high a n m (_:0<=m) := shiftl_specif_high a n m.
+Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m.
+
+(** Properties of advanced functions (pow, sqrt, log2, ...) *)
+
+Include NExtraProp.
+
+End Nat.
+
+(** Re-export notations that should be available even when
+    the [Nat] module is not imported. *)
+
+Bind Scope nat_scope with Nat.t nat.
+
+Infix "^" := Nat.pow : nat_scope.
+Infix "=?" := Nat.eqb (at level 70) : nat_scope.
+Infix "<=?" := Nat.leb (at level 70) : nat_scope.
+Infix "<?" := Nat.ltb (at level 70) : nat_scope.
+Infix "?=" := Nat.compare (at level 70) : nat_scope.
+Infix "/" := Nat.div : nat_scope.
+Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.
+
+Hint Unfold Nat.le : core.
+Hint Unfold Nat.lt : core.
+
+(** [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.