Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits

Initial plan was only to add shiftl/shiftr/land/... to N and
other number type, this is only partly done, but this work has
diverged into a big reorganisation and improvement session
of PArith,NArith,ZArith.

Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a)

PArith/BinPos:
 - added a power function Ppow
 - iterator iter_pos moved from Zmisc to here + some lemmas
 - added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2
 - more lemmas on Pcompare and succ/+/* and order, allow
   to simplify a lot some old proofs elsewhere.
 - new/revised results on Pminus (including some direct proof of
   stuff from Pnat)

PArith/Pnat:
 - more direct proofs (limit the need of stuff about Pmult_nat).
 - provide nicer names for some lemmas (eg. Pplus_plus instead of
   nat_of_P_plus_morphism), compatibility notations provided.
 - kill some too-specific lemmas unused in stdlib + contribs

NArith/BinNat:
 - N_of_nat, nat_of_N moved from Nnat to here.
 - a lemma relating Npred and Nminus
 - revised definitions and specification proofs of Npow and Nlog2

NArith/Nnat:
 - shorter proofs.
 - stuff about Z_of_N is moved to Znat. This way, NArith is
   entirely independent from ZArith.

NArith/Ndigits:
 - added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr
 - revised proofs about Nxor, still using functional bit stream
 - use the same approach to prove properties of Nand Nor Ndiff

ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff

ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat

ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N

ZArith/Zmisc: almost empty new, only contain stuff about badly-named
 iter. Should be reformed more someday.

ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes
 proofs and avoid slowdown due to adding 1 in Z instead of in positive

Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt
 as long as I dont't know why it's slower on powers of two.

Elsewhere: propagate new names + some nicer proofs

NB: Impact on compatibility is probably non-zero, but should be
really moderate. We'll see on contribs, but a few Require here
and there might be necessary.

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

3 files changed, 619 insertions, 562 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index eb89fb20d..51c5b462b 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -152,6 +152,20 @@ Definition Nmax (n n' : N) := match Ncompare n n' with
  | Gt => n
  end.
 
+(** Translation from [N] to [nat] and back. *)
+
+Definition nat_of_N (a:N) :=
+  match a with
+  | N0 => O
+  | Npos p => nat_of_P p
+  end.
+
+Definition N_of_nat (n:nat) :=
+  match n with
+  | O => N0
+  | S n' => Npos (P_of_succ_nat n')
+  end.
+
 (** Decidability of equality. *)
 
 Definition N_eq_dec : forall n m : N, { n = m } + { n <> m }.
@@ -229,7 +243,7 @@ Qed.
 
 Theorem Npred_succ : forall n : N, Npred (Nsucc n) = n.
 Proof.
-destruct n as [| p]; simpl. reflexivity.
+intros [| p]; simpl. reflexivity.
 case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ).
 intro H; false_hyp H Psucc_not_one.
 Qed.
@@ -249,7 +263,7 @@ Qed.
 Theorem Nplus_comm : forall n m:N, n + m = m + n.
 Proof.
 intros.
-destruct n; destruct m; simpl in |- *; try reflexivity.
+destruct n; destruct m; simpl; try reflexivity.
 rewrite Pplus_comm; reflexivity.
 Qed.
 
@@ -259,51 +273,49 @@ intros.
 destruct n; try reflexivity.
 destruct m; try reflexivity.
 destruct p; try reflexivity.
-simpl in |- *; rewrite Pplus_assoc; reflexivity.
+simpl; rewrite Pplus_assoc; reflexivity.
 Qed.
 
 Theorem Nplus_succ : forall n m:N, Nsucc n + m = Nsucc (n + m).
 Proof.
-destruct n; destruct m.
-  simpl in |- *; reflexivity.
-  unfold Nsucc, Nplus in |- *; rewrite <- Pplus_one_succ_l; reflexivity.
-  simpl in |- *; reflexivity.
-  simpl in |- *; rewrite Pplus_succ_permute_l; reflexivity.
+destruct n, m.
+  simpl; reflexivity.
+  unfold Nsucc, Nplus; rewrite <- Pplus_one_succ_l; reflexivity.
+  simpl; reflexivity.
+  simpl; rewrite Pplus_succ_permute_l; reflexivity.
 Qed.
 
 Theorem Nsucc_0 : forall n : N, Nsucc n <> N0.
 Proof.
-intro n; elim n; simpl Nsucc; intros; discriminate.
+now destruct n.
 Qed.
 
 Theorem Nsucc_inj : forall n m:N, Nsucc n = Nsucc m -> n = m.
 Proof.
-destruct n; destruct m; simpl in |- *; intro H; reflexivity || injection H;
- clear H; intro H.
-  symmetry  in H; contradiction Psucc_not_one with p.
-  contradiction Psucc_not_one with p.
-  rewrite Psucc_inj with (1 := H); reflexivity.
+intros [|p] [|q] H; simpl in *; trivial; injection H; clear H; intro H.
+  now elim (Psucc_not_one q).
+  now elim (Psucc_not_one p).
+  apply Psucc_inj in H. now f_equal.
 Qed.
 
 Theorem Nplus_reg_l : forall n m p:N, n + m = n + p -> m = p.
 Proof.
-intro n; pattern n in |- *; apply Nind; clear n; simpl in |- *.
+ induction n using Nind.
   trivial.
-  intros n IHn m p H0; do 2 rewrite Nplus_succ in H0.
-  apply IHn; apply Nsucc_inj; assumption.
+  intros m p H; rewrite 2 Nplus_succ in H.
+  apply Nsucc_inj in H. now apply IHn.
 Qed.
 
 (** Properties of subtraction. *)
 
 Lemma Nminus_N0_Nle : forall n n' : N, n - n' = N0 <-> n <= n'.
 Proof.
-destruct n as [| p]; destruct n' as [| q]; unfold Nle; simpl;
-split; intro H; try discriminate; try reflexivity.
+intros [| p] [| q]; unfold Nle; simpl;
+split; intro H; try easy.
 now elim H.
-intro H1; apply Pminus_mask_Gt in H1. destruct H1 as [h [H1 _]].
-rewrite H1 in H; discriminate.
-case_eq (Pcompare p q Eq); intro H1; rewrite H1 in H; try now elim H.
-assert (H2 : p = q); [now apply Pcompare_Eq_eq |]. now rewrite H2, Pminus_mask_diag.
+contradict H. now destruct (Pminus_mask_Gt _ _ H) as (h & -> & _).
+destruct (Pcompare_spec p q); try now elim H.
+subst. now rewrite Pminus_mask_diag.
 now rewrite Pminus_mask_Lt.
 Qed.
 
@@ -314,10 +326,15 @@ Qed.
 
 Theorem Nminus_succ_r : forall n m : N, n - (Nsucc m) = Npred (n - m).
 Proof.
-destruct n as [| p]; destruct m as [| q]; try reflexivity.
+intros [|p] [|q]; trivial.
 now destruct p.
 simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
-now destruct (Pminus_mask p q) as [| r |]; [| destruct r |].
+now destruct (Pminus_mask p q) as [|[r|r|]|].
+Qed.
+
+Theorem Npred_minus : forall n, Npred n = Nminus n (Npos 1).
+Proof.
+ intros [|[p|p|]]; trivial.
 Qed.
 
 (** Properties of multiplication *)
@@ -334,21 +351,17 @@ Qed.
 
 Theorem Nmult_Sn_m : forall n m : N, (Nsucc n) * m = m + n * m.
 Proof.
-destruct n as [| n]; destruct m as [| m]; simpl; auto.
-rewrite Pmult_Sn_m; reflexivity.
+intros [|n] [|m]; simpl; trivial. now rewrite Pmult_Sn_m.
 Qed.
 
 Theorem Nmult_1_r : forall n:N, n * Npos 1%positive = n.
 Proof.
-destruct n; simpl in |- *; try reflexivity.
-rewrite Pmult_1_r; reflexivity.
+intros [|n]; simpl; trivial. now rewrite Pmult_1_r.
 Qed.
 
 Theorem Nmult_comm : forall n m:N, n * m = m * n.
 Proof.
-intros.
-destruct n; destruct m; simpl in |- *; try reflexivity.
-rewrite Pmult_comm; reflexivity.
+intros [|n] [|m]; simpl; trivial. now rewrite Pmult_comm.
 Qed.
 
 Theorem Nmult_assoc : forall n m p:N, n * (m * p) = n * m * p.
@@ -357,7 +370,7 @@ intros.
 destruct n; try reflexivity.
 destruct m; try reflexivity.
 destruct p; try reflexivity.
-simpl in |- *; rewrite Pmult_assoc; reflexivity.
+simpl; rewrite Pmult_assoc; reflexivity.
 Qed.
 
 Theorem Nmult_plus_distr_r : forall n m p:N, (n + m) * p = n * p + m * p.
@@ -365,7 +378,7 @@ Proof.
 intros.
 destruct n; try reflexivity.
 destruct m; destruct p; try reflexivity.
-simpl in |- *; rewrite Pmult_plus_distr_r; reflexivity.
+simpl; rewrite Pmult_plus_distr_r; reflexivity.
 Qed.
 
 Theorem Nmult_plus_distr_l : forall n m p:N, p * (n + m) = p * n + p * m.
@@ -400,7 +413,7 @@ Qed.
 
 Theorem Ncompare_Eq_eq : forall n m:N, (n ?= m) = Eq -> n = m.
 Proof.
-destruct n as [| n]; destruct m as [| m]; simpl in |- *; intro H;
+destruct n as [| n]; destruct m as [| m]; simpl; intro H;
  reflexivity || (try discriminate H).
   rewrite (Pcompare_Eq_eq n m H); reflexivity.
 Qed.
@@ -509,22 +522,6 @@ Proof.
  now apply (Pplus_lt_mono_l p).
 Qed.
 
-Lemma Nmult_lt_mono_l : forall n m p, N0<n -> m<p -> n*m<n*p.
-Proof.
- intros [|n] m p. discriminate. intros _.
- destruct m, p; try discriminate. auto.
- simpl.
- apply Pmult_lt_mono_l.
-Qed.
-
-Lemma Nmult_le_mono_l : forall n m p, m<=p -> n*m<=n*p.
-Proof.
- intros [|n] m p. intros _ H. discriminate.
- intros. apply Nle_lteq. apply Nle_lteq in H. destruct H; [left|right].
- now apply Nmult_lt_mono_l.
- congruence.
-Qed.
-
 (** 0 is the least natural number *)
 
 Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
@@ -567,9 +564,10 @@ Qed.
 (** Power *)
 
 Definition Npow n p :=
-  match p with
-    | N0 => Npos 1
-    | Npos p => Piter_op Nmult p n
+  match p, n with
+    | N0, _ => Npos 1
+    | _, N0 => N0
+    | Npos p, Npos q => Npos (Ppow q p)
   end.
 
 Infix "^" := Npow : N_scope.
@@ -579,53 +577,32 @@ Proof. reflexivity. Qed.
 
 Lemma Npow_succ_r : forall n p, n^(Nsucc p) = n * n^p.
 Proof.
- intros n p; destruct p; simpl.
- now rewrite Nmult_1_r.
- apply Piter_op_succ. apply Nmult_assoc.
+ intros [|q] [|p]; simpl; trivial; f_equal.
+ apply Ppow_succ_r.
 Qed.
 
 (** Base-2 logarithm *)
 
-Fixpoint Plog2_N (p:positive) : N :=
- match p with
-  | p~0 => Nsucc (Plog2_N p)
-  | p~1 => Nsucc (Plog2_N p)
-  | 1 => N0
- end%positive.
-
 Definition Nlog2 n :=
  match n with
-  | N0 => N0
-  | Npos p => Plog2_N p
+   | N0 => N0
+   | Npos 1 => N0
+   | Npos (p~0) => Npos (Psize_pos p)
+   | Npos (p~1) => Npos (Psize_pos p)
  end.
 
-Lemma Plog2_N_spec : forall p,
- (Npos 2)^(Plog2_N p) <= Npos p < (Npos 2)^(Nsucc (Plog2_N p)).
-Proof.
- induction p; simpl; try rewrite 2 Npow_succ_r.
- (* p~1 *)
- change (Npos p~1) with (Nsucc (Npos 2 * Npos p)).
- split; destruct IHp as [LE LT].
- apply Nle_trans with (Npos 2 * Npos p).
- now apply Nmult_le_mono_l.
- apply Nle_lteq. left.
- apply Ncompare_n_Sm. now right.
- apply Nle_succ_l. apply Nle_succ_l in LT.
- change (Nsucc (Nsucc (Npos 2 * Npos p))) with (Npos 2 * (Nsucc (Npos p))).
- now apply Nmult_le_mono_l.
- (* p~0 *)
- change (Npos p~0) with (Npos 2 * Npos p).
- split; destruct IHp.
- now apply Nmult_le_mono_l.
- now apply Nmult_lt_mono_l.
- (* 1 *)
- now split.
-Qed.
-
 Lemma Nlog2_spec : forall n, N0 < n ->
  (Npos 2)^(Nlog2 n) <= n < (Npos 2)^(Nsucc (Nlog2 n)).
 Proof.
- intros [|n] Hn. discriminate. apply Plog2_N_spec.
+ intros [|[p|p|]] H; discriminate H || clear H; simpl; split.
+ eapply Nle_trans with (Npos (p~0)).
+ apply Psize_pos_le.
+ apply Nle_lteq; left. exact (Pcompare_p_Sp (p~0)).
+ apply Psize_pos_gt.
+ apply Psize_pos_le.
+ apply Psize_pos_gt.
+ discriminate.
+ reflexivity.
 Qed.
 
 Lemma Nlog2_nonpos : forall n, n<=N0 -> Nlog2 n = N0.
@@ -643,8 +620,8 @@ Definition Neven n :=
   end.
 Definition Nodd n := negb (Neven n).
 
-Local Notation "1" := (Npos xH) : N_scope.
-Local Notation "2" := (Npos (xO xH)) : N_scope.
+Local Notation "1" := (Npos 1) : N_scope.
+Local Notation "2" := (Npos 2) : N_scope.
 
 Lemma Neven_spec : forall n, Neven n = true <-> exists m, n=2*m.
 Proof.
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 1992268ab..98e88c6a2 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -6,308 +6,542 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Bool Setoid Bvector BinPos BinNat.
+Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat
+ Pnat Nnat Ndiv_def.
+
+Local Open Scope positive_scope.
 
 (** Operation over bits of a [N] number. *)
 
-(** [xor] *)
+(** Logical [or] *)
+
+Fixpoint Por (p q : positive) : positive :=
+  match p, q with
+    | 1, q~0 => q~1
+    | 1, _ => q
+    | p~0, 1 => p~1
+    | _, 1 => p
+    | p~0, q~0 => (Por p q)~0
+    | p~0, q~1 => (Por p q)~1
+    | p~1, q~0 => (Por p q)~1
+    | p~1, q~1 => (Por p q)~1
+  end.
 
-Fixpoint Pxor (p1 p2:positive) : N :=
-  match p1, p2 with
-  | xH, xH => N0
-  | xH, xO p2 => Npos (xI p2)
-  | xH, xI p2 => Npos (xO p2)
-  | xO p1, xH => Npos (xI p1)
-  | xO p1, xO p2 => Ndouble (Pxor p1 p2)
-  | xO p1, xI p2 => Ndouble_plus_one (Pxor p1 p2)
-  | xI p1, xH => Npos (xO p1)
-  | xI p1, xO p2 => Ndouble_plus_one (Pxor p1 p2)
-  | xI p1, xI p2 => Ndouble (Pxor p1 p2)
+Definition Nor n m :=
+ match n, m with
+   | N0, _ => m
+   | _, N0 => n
+   | Npos p, Npos q => Npos (Por p q)
+ end.
+
+(** Logical [and] *)
+
+Fixpoint Pand (p q : positive) : N :=
+  match p, q with
+    | 1, q~0 => N0
+    | 1, _ => Npos 1
+    | p~0, 1 => N0
+    | _, 1 => Npos 1
+    | p~0, q~0 => Ndouble (Pand p q)
+    | p~0, q~1 => Ndouble (Pand p q)
+    | p~1, q~0 => Ndouble (Pand p q)
+    | p~1, q~1 => Ndouble_plus_one (Pand p q)
   end.
 
-Definition Nxor (n n':N) :=
-  match n, n' with
-  | N0, _ => n'
+Definition Nand n m :=
+ match n, m with
+  | N0, _ => N0
+  | _, N0 => N0
+  | Npos p, Npos q => Pand p q
+ end.
+
+(** Logical [diff] *)
+
+Fixpoint Pdiff (p q:positive) : N :=
+  match p, q with
+    | 1, q~0 => Npos 1
+    | 1, _ => N0
+    | _~0, 1 => Npos p
+    | p~1, 1 => Npos (p~0)
+    | p~0, q~0 => Ndouble (Pdiff p q)
+    | p~0, q~1 => Ndouble (Pdiff p q)
+    | p~1, q~1 => Ndouble (Pdiff p q)
+    | p~1, q~0 => Ndouble_plus_one (Pdiff p q)
+  end.
+
+Fixpoint Ndiff n m :=
+ match n, m with
+  | N0, _ => N0
   | _, N0 => n
-  | Npos p, Npos p' => Pxor p p'
+  | Npos p, Npos q => Pdiff p q
+ end.
+
+(** [xor] *)
+
+Fixpoint Pxor (p q:positive) : N :=
+  match p, q with
+    | 1, 1 => N0
+    | 1, q~0 => Npos (q~1)
+    | 1, q~1 => Npos (q~0)
+    | p~0, 1 => Npos (p~1)
+    | p~0, q~0 => Ndouble (Pxor p q)
+    | p~0, q~1 => Ndouble_plus_one (Pxor p q)
+    | p~1, 1 => Npos (p~0)
+    | p~1, q~0 => Ndouble_plus_one (Pxor p q)
+    | p~1, q~1 => Ndouble (Pxor p q)
+  end.
+
+Definition Nxor (n m:N) :=
+  match n, m with
+    | N0, _ => m
+    | _, N0 => n
+    | Npos p, Npos q => Pxor p q
+  end.
+
+(** For proving properties of these operations, we will use
+  an equivalence with functional streams of bit, cf [eqf] below *)
+
+(** Shift *)
+
+Definition Nshiftl_nat (a:N)(n:nat) := iter_nat n _ Ndouble a.
+
+Definition Nshiftr_nat (a:N)(n:nat) := iter_nat n _ Ndiv2 a.
+
+Definition Nshiftr a n :=
+  match n with
+    | N0 => a
+    | Npos p => iter_pos p _ Ndiv2 a
+  end.
+
+Definition Nshiftl a n :=
+  match a, n with
+    | _, N0 => a
+    | N0, _ => a
+    | Npos p, Npos q => Npos (iter_pos q _ xO p)
   end.
 
-Lemma Nxor_neutral_left : forall n:N, Nxor N0 n = n.
+(** Checking whether a particular bit is set on not *)
+
+Fixpoint Pbit (p:positive) : nat -> bool :=
+  match p with
+    | 1 => fun n => match n with
+                      | O => true
+                      | S _ => false
+                    end
+    | p~0 => fun n => match n with
+                        | O => false
+                        | S n' => Pbit p n'
+                      end
+    | p~1 => fun n => match n with
+                        | O => true
+                        | S n' => Pbit p n'
+                      end
+  end.
+
+Definition Nbit (a:N) :=
+  match a with
+    | N0 => fun _ => false
+    | Npos p => Pbit p
+  end.
+
+(** Same, but with index in N *)
+
+Fixpoint Ptestbit p n :=
+  match p, n with
+    | p~0, N0 => false
+    | _, N0 => true
+    | 1, _ => false
+    | p~0, _ => Ptestbit p (Npred n)
+    | p~1, _ => Ptestbit p (Npred n)
+  end.
+
+Definition Ntestbit a n :=
+  match a with
+    | N0 => false
+    | Npos p => Ptestbit p n
+  end.
+
+Local Close Scope positive_scope.
+Local Open Scope N_scope.
+
+(** Equivalence of Pbit and Ptestbit *)
+
+Lemma Ptestbit_Pbit :
+ forall p n, Ptestbit p (N_of_nat n) = Pbit p n.
 Proof.
-  trivial.
+ induction p as [p IH|p IH| ]; intros n; simpl.
+ rewrite <- N_of_pred, IH; destruct n; trivial.
+ rewrite <- N_of_pred, IH; destruct n; trivial.
+ destruct n; trivial.
 Qed.
 
-Lemma Nxor_neutral_right : forall n:N, Nxor n N0 = n.
+Lemma Ntestbit_Nbit : forall a n, Ntestbit a (N_of_nat n) = Nbit a n.
 Proof.
-  destruct n; trivial.
+ destruct a. trivial. apply Ptestbit_Pbit.
 Qed.
 
-Lemma Nxor_comm : forall n n':N, Nxor n n' = Nxor n' n.
+Lemma Pbit_Ptestbit :
+ forall p n, Pbit p (nat_of_N n) = Ptestbit p n.
 Proof.
-  destruct n; destruct n'; simpl; auto.
-  generalize p0; clear p0; induction p as [p Hrecp| p Hrecp| ]; simpl;
-   auto.
-  destruct p0; trivial; rewrite Hrecp; trivial.
-  destruct p0; trivial; rewrite Hrecp; trivial.
-  destruct p0 as [p| p| ]; simpl; auto.
+ intros; now rewrite <- Ptestbit_Pbit, N_of_nat_of_N.
 Qed.
 
-Lemma Nxor_nilpotent : forall n:N, Nxor n n = N0.
+Lemma Nbit_Ntestbit :
+ forall a n, Nbit a (nat_of_N n) = Ntestbit a n.
 Proof.
-  destruct n; trivial.
-  simpl. induction p as [p IHp| p IHp| ]; trivial.
-  simpl. rewrite IHp; reflexivity.
-  simpl. rewrite IHp; reflexivity.
+ destruct a. trivial. apply Pbit_Ptestbit.
 Qed.
 
-(** Checking whether a particular bit is set on not *)
+(** Equivalence of shifts, N and nat versions *)
 
-Fixpoint Pbit (p:positive) : nat -> bool :=
-  match p with
-  | xH => fun n:nat => match n with
-                       | O => true
-                       | S _ => false
-                       end
-  | xO p =>
-      fun n:nat => match n with
-                   | O => false
-                   | S n' => Pbit p n'
-                   end
-  | xI p => fun n:nat => match n with
-                         | O => true
-                         | S n' => Pbit p n'
-                         end
-  end.
+Lemma Nshiftr_nat_equiv :
+ forall a n, Nshiftr_nat a (nat_of_N n) = Nshiftr a n.
+Proof.
+ intros a [|n]; simpl; unfold Nshiftr_nat.
+ trivial.
+ symmetry. apply iter_nat_of_P.
+Qed.
 
-Definition Nbit (a:N) :=
-  match a with
-  | N0 => fun _ => false
-  | Npos p => Pbit p
-  end.
+Lemma Nshiftr_equiv_nat :
+ forall a n, Nshiftr a (N_of_nat n) = Nshiftr_nat a n.
+Proof.
+ intros. now rewrite <- Nshiftr_nat_equiv, nat_of_N_of_nat.
+Qed.
+
+Lemma Nshiftl_nat_equiv :
+ forall a n, Nshiftl_nat a (nat_of_N n) = Nshiftl a n.
+Proof.
+ intros [|a] [|n]; simpl; unfold Nshiftl_nat; trivial.
+ apply iter_nat_invariant; intros; now subst.
+ rewrite <- iter_nat_of_P. symmetry. now apply iter_pos_swap_gen.
+Qed.
+
+Lemma Nshiftl_equiv_nat :
+ forall a n, Nshiftl a (N_of_nat n) = Nshiftl_nat a n.
+Proof.
+ intros. now rewrite <- Nshiftl_nat_equiv, nat_of_N_of_nat.
+Qed.
+
+(** Correctness proofs for shifts *)
 
-(** Auxiliary results about streams of bits *)
+Lemma Nshiftl_mult_pow : forall a n, Nshiftl a n = a * 2^n.
+Proof.
+ intros [|a] [|n]; simpl; trivial.
+ now rewrite Pmult_1_r.
+ f_equal.
+ set (f x := Pmult x a).
+ rewrite Pmult_comm. fold (f (2^n))%positive.
+ change a with (f xH).
+ unfold Ppow. symmetry. now apply iter_pos_swap_gen.
+Qed.
+
+(*
+Lemma Nshiftr_div_pow : forall a n, Nshiftr a n = a / 2^n.
+*)
+
+(** Equality over functional streams of bits *)
 
 Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.
 
-Lemma eqf_sym : forall f f':nat -> bool, eqf f f' -> eqf f' f.
+Instance eqf_equiv : Equivalence eqf.
+Proof.
+ split; congruence.
+Qed.
+
+Local Infix "==" := eqf (at level 70, no associativity).
+
+(** If two numbers produce the same stream of bits, they are equal. *)
+
+Local Notation Step H := (fun n => H (S n)).
+
+Lemma Pbit_faithful_0 : forall p, ~(Pbit p == (fun _ => false)).
 Proof.
-  unfold eqf. intros. rewrite H. reflexivity.
+ induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O).
+  apply (IHp (Step H)).
 Qed.
 
-Lemma eqf_refl : forall f:nat -> bool, eqf f f.
+Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'.
 Proof.
-  unfold eqf. trivial.
+ induction p as [p IHp|p IHp| ]; intros [p'|p'|] H; trivial;
+  try discriminate (H O).
+ f_equal. apply (IHp _ (Step H)).
+ destruct (Pbit_faithful_0 _ (Step H)).
+ f_equal. apply (IHp _ (Step H)).
+ symmetry in H. destruct (Pbit_faithful_0 _ (Step H)).
 Qed.
 
-Lemma eqf_trans :
- forall f f' f'':nat -> bool, eqf f f' -> eqf f' f'' -> eqf f f''.
+Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'.
 Proof.
-  unfold eqf. intros. rewrite H. exact (H0 n).
+ intros [|p] [|p'] H; trivial.
+ symmetry in H. destruct (Pbit_faithful_0 _ H).
+ destruct (Pbit_faithful_0 _ H).
+ f_equal. apply Pbit_faithful, H.
 Qed.
 
+Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'.
+Proof.
+ split. apply Nbit_faithful. intros; now subst.
+Qed.
+
+
+(** Bit operations for functional streams of bits *)
+
+Definition orf (f g:nat -> bool) (n:nat) := (f n) || (g n).
+Definition andf (f g:nat -> bool) (n:nat) := (f n) && (g n).
+Definition difff (f g:nat -> bool) (n:nat) := (f n) && negb (g n).
 Definition xorf (f g:nat -> bool) (n:nat) := xorb (f n) (g n).
 
-Lemma xorf_eq :
- forall f f', eqf (xorf f f') (fun n => false) -> eqf f f'.
+Instance eqf_orf : Proper (eqf==>eqf==>eqf) orf.
 Proof.
-  unfold eqf, xorf. intros. apply xorb_eq, H.
+  unfold orf. congruence.
 Qed.
 
-Lemma xorf_assoc :
- forall f f' f'',
-   eqf (xorf (xorf f f') f'') (xorf f (xorf f' f'')).
+Instance eqf_andf : Proper (eqf==>eqf==>eqf) andf.
 Proof.
-  unfold eqf, xorf. intros. apply xorb_assoc.
+  unfold andf. congruence.
 Qed.
 
-Lemma eqf_xorf :
- forall f f' f'' f''',
-   eqf f f' -> eqf f'' f''' -> eqf (xorf f f'') (xorf f' f''').
+Instance eqf_difff : Proper (eqf==>eqf==>eqf) difff.
 Proof.
-  unfold eqf, xorf. intros. rewrite H. rewrite H0. reflexivity.
+  unfold difff. congruence.
 Qed.
 
-(** End of auxilliary results *)
+Instance eqf_xorf : Proper (eqf==>eqf==>eqf) xorf.
+Proof.
+  unfold xorf. congruence.
+Qed.
 
-(** This part is aimed at proving that if two numbers produce
-  the same stream of bits, then they are equal. *)
+(** We now describe the semantics of [Nxor] and other bitwise
+  operations in terms of bit streams. *)
 
-Lemma Nbit_faithful_1 : forall a:N, eqf (Nbit N0) (Nbit a) -> N0 = a.
+Lemma Pxor_semantics : forall p p',
+ Nbit (Pxor p p') == xorf (Pbit p) (Pbit p').
 Proof.
-  destruct a. trivial.
-  induction p as [p IHp| p IHp| ]; intro H.
-  absurd (N0 = Npos p). discriminate.
-  exact (IHp (fun n => H (S n))).
-  absurd (N0 = Npos p). discriminate.
-  exact (IHp (fun n => H (S n))).
-  absurd (false = true). discriminate.
-  exact (H 0).
+ induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl;
+  (specialize (IHp p'); destruct Pxor; trivial; apply (IHp n)) ||
+  (unfold xorf; now rewrite ?xorb_false_l, ?xorb_false_r).
 Qed.
 
-Lemma Nbit_faithful_2 :
- forall a:N, eqf (Nbit (Npos 1)) (Nbit a) -> Npos 1 = a.
+Lemma Nxor_semantics : forall a a',
+ Nbit (Nxor a a') == xorf (Nbit a) (Nbit a').
 Proof.
-  destruct a. intros. absurd (true = false). discriminate.
-  exact (H 0).
-  destruct p. intro H. absurd (N0 = Npos p). discriminate.
-  exact (Nbit_faithful_1 (Npos p) (fun n:nat => H (S n))).
-  intros. absurd (true = false). discriminate.
-  exact (H 0).
-  trivial.
+ intros [|p] [|p'] n; simpl; unfold xorf; trivial.
+ now rewrite xorb_false_l.
+ now rewrite xorb_false_r.
+ apply Pxor_semantics.
 Qed.
 
-Lemma Nbit_faithful_3 :
- forall (a:N) (p:positive),
-   (forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') ->
-   eqf (Nbit (Npos (xO p))) (Nbit a) -> Npos (xO p) = a.
+Lemma Por_semantics : forall p p',
+ Pbit (Por p p') == orf (Pbit p) (Pbit p').
 Proof.
-  destruct a; intros. cut (eqf (Nbit N0) (Nbit (Npos (xO p)))).
-  intro. rewrite (Nbit_faithful_1 (Npos (xO p)) H1). reflexivity.
-  unfold eqf. intro. unfold eqf in H0. rewrite H0. reflexivity.
-  destruct p. discriminate (H0 O).
-  rewrite (H p (fun n => H0 (S n))). reflexivity.
-  discriminate (H0 0).
+ induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial;
+  unfold orf; apply (IHp p' n) || now rewrite orb_false_r.
 Qed.
 
-Lemma Nbit_faithful_4 :
- forall (a:N) (p:positive),
-   (forall p':positive, eqf (Nbit (Npos p)) (Nbit (Npos p')) -> p = p') ->
-   eqf (Nbit (Npos (xI p))) (Nbit a) -> Npos (xI p) = a.
+Lemma Nor_semantics : forall a a',
+ Nbit (Nor a a') == orf (Nbit a) (Nbit a').
 Proof.
-  destruct a; intros. cut (eqf (Nbit N0) (Nbit (Npos (xI p)))).
-  intro. rewrite (Nbit_faithful_1 (Npos (xI p)) H1). reflexivity.
-  intro. rewrite H0. reflexivity.
-  destruct p. rewrite (H p (fun n:nat => H0 (S n))). reflexivity.
-  discriminate (H0 0).
-  cut (eqf (Nbit (Npos 1)) (Nbit (Npos (xI p0)))).
-  intro. discriminate (Nbit_faithful_1 (Npos p0) (fun n:nat => H1 (S n))).
-  intro. rewrite H0. reflexivity.
+ intros [|p] [|p'] n; simpl; unfold orf; trivial.
+ now rewrite orb_false_r.
+ apply Por_semantics.
 Qed.
 
-Lemma Nbit_faithful : forall a a':N, eqf (Nbit a) (Nbit a') -> a = a'.
+Lemma Pand_semantics : forall p p',
+ Nbit (Pand p p') == andf (Pbit p) (Pbit p').
 Proof.
-  destruct a. exact Nbit_faithful_1.
-  induction p. intros a' H. apply Nbit_faithful_4. intros.
-  assert (Npos p = Npos p') by exact (IHp (Npos p') H0).
-  inversion H1. reflexivity.
-  assumption.
-  intros. apply Nbit_faithful_3. intros.
-  assert (Npos p = Npos p') by exact (IHp (Npos p') H0).
-  inversion H1. reflexivity.
-  assumption.
-  exact Nbit_faithful_2.
+ induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl;
+  (specialize (IHp p'); destruct Pand; trivial; apply (IHp n)) ||
+  (unfold andf; now rewrite andb_false_r).
 Qed.
 
-(** We now describe the semantics of [Nxor] in terms of bit streams. *)
+Lemma Nand_semantics : forall a a',
+ Nbit (Nand a a') == andf (Nbit a) (Nbit a').
+Proof.
+ intros [|p] [|p'] n; simpl; unfold andf; trivial.
+ now rewrite andb_false_r.
+ apply Pand_semantics.
+Qed.
 
-Lemma Nxor_sem_1 : forall a':N, Nbit (Nxor N0 a') 0 = Nbit a' 0.
+Lemma Pdiff_semantics : forall p p',
+ Nbit (Pdiff p p') == difff (Pbit p) (Pbit p').
 Proof.
-  trivial.
+ induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl;
+  (specialize (IHp p'); destruct Pdiff; trivial; apply (IHp n)) ||
+  (unfold difff; simpl; now rewrite andb_true_r).
 Qed.
 
-Lemma Nxor_sem_2 :
- forall a':N, Nbit (Nxor (Npos 1) a') 0 = negb (Nbit a' 0).
+Lemma Ndiff_semantics : forall a a',
+ Nbit (Ndiff a a') == difff (Nbit a) (Nbit a').
 Proof.
-  intro. destruct a'. trivial.
-  destruct p; trivial.
+ intros [|p] [|p'] n; simpl; unfold difff; trivial.
+ simpl. now rewrite andb_true_r.
+ apply Pdiff_semantics.
 Qed.
 
-Lemma Nxor_sem_3 :
- forall (p:positive) (a':N),
-   Nbit (Nxor (Npos (xO p)) a') 0 = Nbit a' 0.
+Hint Rewrite Nxor_semantics Nor_semantics
+ Nand_semantics Ndiff_semantics : bitwise_semantics.
+
+Ltac bitwise_semantics :=
+ apply Nbit_faithful; autorewrite with bitwise_semantics;
+ intro n; unfold xorf, orf, andf, difff.
+
+(** Now, we can easily deduce properties of [Nxor] and others
+    from properties of [xorb] and others. *)
+
+Lemma Nxor_eq : forall a a', Nxor a a' = 0 -> a = a'.
 Proof.
-  intros. destruct a'. trivial.
-  simpl. destruct p0; trivial.
-  destruct (Pxor p p0); trivial.
-  destruct (Pxor p p0); trivial.
+ intros a a' H. bitwise_semantics. apply xorb_eq.
+ rewrite <- Nbit_faithful_iff, Nxor_semantics in H. apply H.
 Qed.
 
-Lemma Nxor_sem_4 :
- forall (p:positive) (a':N),
-   Nbit (Nxor (Npos (xI p)) a') 0 = negb (Nbit a' 0).
+Lemma Nxor_nilpotent : forall a, Nxor a a = 0.
 Proof.
-  intros. destruct a'. trivial.
-  simpl. destruct p0; trivial.
-  destruct (Pxor p p0); trivial.
-  destruct (Pxor p p0); trivial.
+ intros. bitwise_semantics. apply xorb_nilpotent.
 Qed.
 
-Lemma Nxor_sem_5 :
- forall a a':N, Nbit (Nxor a a') 0 = xorf (Nbit a) (Nbit a') 0.
+Lemma Nxor_0_l : forall n, Nxor 0 n = n.
 Proof.
-  destruct a; intro. change (Nbit a' 0 = xorb false (Nbit a' 0)). rewrite false_xorb. trivial.
-  destruct p. apply Nxor_sem_4.
-  change (Nbit (Nxor (Npos (xO p)) a') 0 = xorb false (Nbit a' 0)).
-  rewrite false_xorb. apply Nxor_sem_3. apply Nxor_sem_2.
+ trivial.
 Qed.
+Notation Nxor_neutral_left := Nxor_0_l (only parsing).
 
-Lemma Nxor_sem_6 :
- forall n:nat,
-   (forall a a':N, Nbit (Nxor a a') n = xorf (Nbit a) (Nbit a') n) ->
-   forall a a':N,
-     Nbit (Nxor a a') (S n) = xorf (Nbit a) (Nbit a') (S n).
+Lemma Nxor_0_r : forall n, Nxor n 0 = n.
 Proof.
-  intros.
-(* pose proof (fun p1 p2 => H (Npos p1) (Npos p2)) as H'. clear H. rename H' into H.*)
-  generalize (fun p1 p2 => H (Npos p1) (Npos p2)); clear H; intro H.
-  unfold xorf in *.
-  destruct a as [|p]. simpl Nbit; rewrite false_xorb. reflexivity.
-  destruct a' as [|p0].
-  simpl Nbit; rewrite xorb_false. reflexivity.
-  destruct p. destruct p0; simpl Nbit in *.
-  rewrite <- H; simpl; case (Pxor p p0); trivial.
-  rewrite <- H; simpl; case (Pxor p p0); trivial.
-  rewrite xorb_false. reflexivity.
-  destruct p0; simpl Nbit in *.
-  rewrite <- H; simpl; case (Pxor p p0); trivial.
-  rewrite <- H; simpl; case (Pxor p p0); trivial.
-  rewrite xorb_false. reflexivity.
-  simpl Nbit. rewrite false_xorb. destruct p0; trivial.
-Qed.
-
-Lemma Nxor_semantics :
- forall a a':N, eqf (Nbit (Nxor a a')) (xorf (Nbit a) (Nbit a')).
-Proof.
-  unfold eqf. intros; generalize a, a'. induction n.
-  apply Nxor_sem_5. apply Nxor_sem_6; assumption.
-Qed.
-
-(** Consequences:
-       - only equal numbers lead to a null xor
-       - xor is associative
-*)
+ destruct n; trivial.
+Qed.
+Notation Nxor_neutral_right := Nxor_0_r (only parsing).
 
-Lemma Nxor_eq : forall a a':N, Nxor a a' = N0 -> a = a'.
+Lemma Nxor_comm : forall a a', Nxor a a' = Nxor a' a.
 Proof.
-  intros. apply Nbit_faithful, xorf_eq. apply eqf_trans with (f' := Nbit (Nxor a a')).
-  apply eqf_sym, Nxor_semantics.
-  rewrite H. unfold eqf. trivial.
+ intros. bitwise_semantics. apply xorb_comm.
 Qed.
 
 Lemma Nxor_assoc :
- forall a a' a'':N, Nxor (Nxor a a') a'' = Nxor a (Nxor a' a'').
-Proof.
-  intros. apply Nbit_faithful.
-  apply eqf_trans with (xorf (xorf (Nbit a) (Nbit a')) (Nbit a'')).
-  apply eqf_trans with (xorf (Nbit (Nxor a a')) (Nbit a'')).
-  apply Nxor_semantics.
-  apply eqf_xorf. apply Nxor_semantics.
-  apply eqf_refl.
-  apply eqf_trans with (xorf (Nbit a) (xorf (Nbit a') (Nbit a''))).
-  apply xorf_assoc.
-  apply eqf_trans with (xorf (Nbit a) (Nbit (Nxor a' a''))).
-  apply eqf_xorf. apply eqf_refl.
-  apply eqf_sym, Nxor_semantics.
-  apply eqf_sym, Nxor_semantics.
+ forall a a' a'', Nxor (Nxor a a') a'' = Nxor a (Nxor a' a'').
+Proof.
+ intros. bitwise_semantics. apply xorb_assoc.
+Qed.
+
+Lemma Nor_0_l : forall n, Nor 0 n = n.
+Proof.
+ trivial.
+Qed.
+
+Lemma Nor_0_r : forall n, Nor n 0 = n.
+Proof.
+ destruct n; trivial.
+Qed.
+
+Lemma Nor_comm : forall a a', Nor a a' = Nor a' a.
+Proof.
+ intros. bitwise_semantics. apply orb_comm.
+Qed.
+
+Lemma Nor_assoc :
+ forall a a' a'', Nor a (Nor a' a'') = Nor (Nor a a') a''.
+Proof.
+ intros. bitwise_semantics. apply orb_assoc.
+Qed.
+
+Lemma Nor_diag : forall a, Nor a a = a.
+Proof.
+ intros. bitwise_semantics. apply orb_diag.
+Qed.
+
+Lemma Nand_0_l : forall n, Nand 0 n = 0.
+Proof.
+ trivial.
+Qed.
+
+Lemma Nand_0_r : forall n, Nand n 0 = 0.
+Proof.
+ destruct n; trivial.
+Qed.
+
+Lemma Nand_comm : forall a a', Nand a a' = Nand a' a.
+Proof.
+ intros. bitwise_semantics. apply andb_comm.
+Qed.
+
+Lemma Nand_assoc :
+ forall a a' a'', Nand a (Nand a' a'') = Nand (Nand a a') a''.
+Proof.
+ intros. bitwise_semantics. apply andb_assoc.
+Qed.
+
+Lemma Nand_diag : forall a, Nand a a = a.
+Proof.
+ intros. bitwise_semantics. apply andb_diag.
+Qed.
+
+Lemma Ndiff_0_l : forall n, Ndiff 0 n = 0.
+Proof.
+ trivial.
 Qed.
 
+Lemma Ndiff_0_r : forall n, Ndiff n 0 = n.
+Proof.
+ destruct n; trivial.
+Qed.
+
+Lemma Ndiff_diag : forall a, Ndiff a a = 0.
+Proof.
+ intros. bitwise_semantics. apply andb_negb_r.
+Qed.
+
+Lemma Nor_and_distr_l : forall a b c,
+ Nor (Nand a b) c = Nand (Nor a c) (Nor b c).
+Proof.
+ intros. bitwise_semantics. apply orb_andb_distrib_l.
+Qed.
+
+Lemma Nor_and_distr_r : forall a b c,
+ Nor a (Nand b c) = Nand (Nor a b) (Nor a c).
+Proof.
+ intros. bitwise_semantics. apply orb_andb_distrib_r.
+Qed.
+
+Lemma Nand_or_distr_l : forall a b c,
+ Nand (Nor a b) c = Nor (Nand a c) (Nand b c).
+Proof.
+ intros. bitwise_semantics. apply andb_orb_distrib_l.
+Qed.
+
+Lemma Nand_or_distr_r : forall a b c,
+ Nand a (Nor b c) = Nor (Nand a b) (Nand a c).
+Proof.
+ intros. bitwise_semantics. apply andb_orb_distrib_r.
+Qed.
+
+Lemma Ndiff_diff_l : forall a b c,
+ Ndiff (Ndiff a b) c = Ndiff a (Nor b c).
+Proof.
+ intros. bitwise_semantics. now rewrite negb_orb, andb_assoc.
+Qed.
+
+Lemma Nor_diff_and : forall a b,
+ Nor (Ndiff a b) (Nand a b) = a.
+Proof.
+ intros. bitwise_semantics.
+ now rewrite <- andb_orb_distrib_r, orb_comm, orb_negb_r, andb_true_r.
+Qed.
+
+Lemma Nand_diff : forall a b,
+ Nand (Ndiff a b) b = 0.
+Proof.
+ intros. bitwise_semantics.
+ now rewrite <-andb_assoc, (andb_comm (negb _)), andb_negb_r, andb_false_r.
+Qed.
+
+Local Close Scope N_scope.
+
 (** Checking whether a number is odd, i.e.
    if its lower bit is set. *)
 
 Definition Nbit0 (n:N) :=
   match n with
   | N0 => false
-  | Npos (xO _) => false
+  | Npos (_~0) => false
   | _ => true
   end.
 
@@ -358,7 +592,7 @@ Qed.
 Lemma Nxor_bit0 :
  forall a a':N, Nbit0 (Nxor a a') = xorb (Nbit0 a) (Nbit0 a').
 Proof.
-  intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' 0).
+  intros. rewrite <- Nbit0_correct, (Nxor_semantics a a' O).
   unfold xorf. rewrite Nbit0_correct, Nbit0_correct. reflexivity.
 Qed.
 
@@ -554,7 +788,7 @@ Qed.
 (** Number of digits in a number *)
 
 Definition Nsize (n:N) : nat := match n with
-  | N0 => 0%nat
+  | N0 => O
   | Npos p => Psize p
  end.
 
@@ -719,18 +953,40 @@ induction n; simpl in *; intros; destruct p; auto with arith.
 inversion H; inversion H1.
 Qed.
 
-(** Xor is the same in the two worlds. *)
+(** Binary bitwise operations are the same in the two worlds. *)
 
 Lemma Nxor_BVxor : forall n (bv bv' : Bvector n),
   Bv2N _ (BVxor _ bv bv') = Nxor (Bv2N _ bv) (Bv2N _ bv').
 Proof.
-induction n.
-intros.
+induction n; intros bv bv'.
+rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto.
+rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto.
+rewrite IHn.
+destruct (Vhead bool n bv), (Vhead bool n bv'),
+ (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv'));
+ simpl; auto.
+Qed.
+
+Lemma Nor_BVor : forall n (bv bv' : Bvector n),
+  Bv2N _ (BVor _ bv bv') = Nor (Bv2N _ bv) (Bv2N _ bv').
+Proof.
+induction n; intros bv bv'.
 rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto.
-intros.
 rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto.
 rewrite IHn.
-destruct (Vhead bool n bv); destruct (Vhead bool n bv');
- destruct (Bv2N n (Vtail bool n bv)); destruct (Bv2N n (Vtail bool n bv')); simpl; auto.
+destruct (Vhead bool n bv), (Vhead bool n bv'),
+ (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv'));
+ simpl; auto.
 Qed.
 
+Lemma Nand_BVand : forall n (bv bv' : Bvector n),
+  Bv2N _ (BVand _ bv bv') = Nand (Bv2N _ bv) (Bv2N _ bv').
+Proof.
+induction n; intros bv bv'.
+rewrite (V0_eq _ bv), (V0_eq _ bv'); simpl; auto.
+rewrite (VSn_eq _ _ bv), (VSn_eq _ _ bv'); simpl; auto.
+rewrite IHn.
+destruct (Vhead bool n bv), (Vhead bool n bv'),
+ (Bv2N n (Vtail bool n bv)), (Bv2N n (Vtail bool n bv'));
+ simpl; auto.
+Qed.
diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v
index 93fdfff7a..05ca4a550 100644
--- a/theories/NArith/Nnat.v
+++ b/theories/NArith/Nnat.v
@@ -6,149 +6,86 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-Require Import Arith_base.
-Require Import Compare_dec.
-Require Import Sumbool.
-Require Import Div2.
-Require Import Min.
-Require Import Max.
-Require Import BinPos.
-Require Import BinNat.
-Require Import BinInt.
-Require Import Pnat.
-Require Import Znat.
-
-(** Translation from [N] to [nat] and back. *)
-
-Definition nat_of_N (a:N) :=
-  match a with
-  | N0 => 0%nat
-  | Npos p => nat_of_P p
-  end.
-
-Definition N_of_nat (n:nat) :=
-  match n with
-  | O => N0
-  | S n' => Npos (P_of_succ_nat n')
-  end.
+Require Import Arith_base Compare_dec Sumbool Div2 Min Max.
+Require Import BinPos BinNat Pnat.
 
 Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a.
 Proof.
   destruct a as [| p]. reflexivity.
-  simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *.
-  rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H.
+  simpl. elim (nat_of_P_is_S p). intros n H. rewrite H. simpl.
+  rewrite <- nat_of_P_of_succ_nat in H.
   rewrite nat_of_P_inj with (1 := H). reflexivity.
 Qed.
 
 Lemma nat_of_N_of_nat : forall n:nat, nat_of_N (N_of_nat n) = n.
 Proof.
   induction n. trivial.
-  intros. simpl in |- *. apply nat_of_P_o_P_of_succ_nat_eq_succ.
+  intros. simpl. apply nat_of_P_of_succ_nat.
 Qed.
 
-(** Interaction of this translation and usual operations. *)
-
-Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a).
+Lemma nat_of_N_inj : forall n n', nat_of_N n = nat_of_N n' -> n = n'.
 Proof.
-  destruct a; simpl nat_of_N; auto.
-  apply nat_of_P_xO.
+  intros n n' H.
+  rewrite <- (N_of_nat_of_N n), <- (N_of_nat_of_N n'). now f_equal.
 Qed.
 
-Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n).
+Lemma N_of_nat_inj : forall n n', N_of_nat n = N_of_nat n' -> n = n'.
 Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  rewrite <- nat_of_Ndouble.
-  apply N_of_nat_of_N.
+  intros n n' H.
+  rewrite <- (nat_of_N_of_nat n), <- (nat_of_N_of_nat n'). now f_equal.
 Qed.
 
-Lemma nat_of_Ndouble_plus_one :
-  forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)).
+Hint Rewrite nat_of_N_of_nat N_of_nat_of_N : Nnat.
+
+(** Interaction of this translation and usual operations. *)
+
+Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a).
 Proof.
-  destruct a; simpl nat_of_N; auto.
-  apply nat_of_P_xI.
+  destruct a; simpl nat_of_N; trivial. apply nat_of_P_xO.
 Qed.
 
-Lemma N_of_double_plus_one :
-  forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n).
+Lemma nat_of_Ndouble_plus_one :
+  forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)).
 Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  rewrite <- nat_of_Ndouble_plus_one.
-  apply N_of_nat_of_N.
+  destruct a; simpl nat_of_N; trivial. apply nat_of_P_xI.
 Qed.
 
 Lemma nat_of_Nsucc : forall a, nat_of_N (Nsucc a) = S (nat_of_N a).
 Proof.
   destruct a; simpl.
   apply nat_of_P_xH.
-  apply nat_of_P_succ_morphism.
-Qed.
-
-Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n).
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  rewrite <- nat_of_Nsucc.
-  apply N_of_nat_of_N.
+  apply Psucc_S.
 Qed.
 
 Lemma nat_of_Nplus :
   forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a').
 Proof.
   destruct a; destruct a'; simpl; auto.
-  apply nat_of_P_plus_morphism.
+  apply Pplus_plus.
 Qed.
 
-Lemma N_of_plus :
-  forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n').
+Lemma nat_of_Nmult :
+  forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a').
 Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nplus.
-  apply N_of_nat_of_N.
+  destruct a; destruct a'; simpl; auto.
+  apply Pmult_mult.
 Qed.
 
 Lemma nat_of_Nminus :
   forall a a', nat_of_N (Nminus a a') = ((nat_of_N a)-(nat_of_N a'))%nat.
 Proof.
-  destruct a; destruct a'; simpl; auto with arith.
-  case_eq (Pcompare p p0 Eq); simpl; intros.
-  rewrite (Pcompare_Eq_eq _ _ H); auto with arith.
-  rewrite Pminus_mask_diag. simpl. apply minus_n_n.
-  rewrite Pminus_mask_Lt. pose proof (nat_of_P_lt_Lt_compare_morphism _ _ H). simpl.
-  symmetry; apply not_le_minus_0. auto with arith. assumption.
-  pose proof (Pminus_mask_Gt p p0 H) as H1. destruct H1 as [q [H1 _]]. rewrite H1; simpl.
-  replace q with (Pminus p p0) by (unfold Pminus; now rewrite H1).
-  apply nat_of_P_minus_morphism; auto.
-Qed.
-
-Lemma N_of_minus :
-  forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n').
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nminus.
-  apply N_of_nat_of_N.
-Qed.
-
-Lemma nat_of_Nmult :
-  forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a').
-Proof.
-  destruct a; destruct a'; simpl; auto.
-  apply nat_of_P_mult_morphism.
+  intros [|a] [|a']; simpl; auto with arith.
+  destruct (Pcompare_spec a a').
+  subst. now rewrite Pminus_mask_diag, <- minus_n_n.
+  rewrite Pminus_mask_Lt by trivial. apply Plt_lt in H.
+  simpl; symmetry; apply not_le_minus_0; auto with arith.
+  destruct (Pminus_mask_Gt a a' (ZC2 _ _ H)) as (q & -> & Hq & _).
+  simpl. apply plus_minus. now rewrite <- Hq, Pplus_plus.
 Qed.
 
-Lemma N_of_mult :
-  forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n').
+Lemma nat_of_Npred : forall a, nat_of_N (Npred a) = pred (nat_of_N a).
 Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nmult.
-  apply N_of_nat_of_N.
+ intros. rewrite pred_of_minus, Npred_minus. apply nat_of_Nminus.
 Qed.
 
 Lemma nat_of_Ndiv2 :
@@ -162,205 +99,92 @@ Proof.
   rewrite div2_double; auto.
 Qed.
 
-Lemma N_of_div2 :
-  forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n).
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  rewrite <- nat_of_Ndiv2.
-  apply N_of_nat_of_N.
-Qed.
-
 Lemma nat_of_Ncompare :
  forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a').
 Proof.
-  destruct a; destruct a'; simpl.
-  reflexivity.
-  assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P.
-  destruct nat_of_P; [inversion NZ|auto].
-  assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P.
-  destruct nat_of_P; [inversion NZ|auto].
-  apply nat_of_P_compare_morphism.
-Qed.
-
-Lemma N_of_nat_compare :
- forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n').
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  symmetry; apply nat_of_Ncompare.
-Qed.
-
-Lemma nat_of_Nmin :
-  forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a').
-Proof.
-  intros; unfold Nmin; rewrite nat_of_Ncompare.
-  rewrite nat_compare_equiv; unfold nat_compare_alt.
-  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|];
-    simpl; intros; symmetry; auto with arith.
-  apply min_l; rewrite e; auto with arith.
-Qed.
-
-Lemma N_of_min :
-  forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n').
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nmin.
-  apply N_of_nat_of_N.
+  destruct a; destruct a'; simpl; trivial.
+  now destruct (nat_of_P_is_S p) as (n,->).
+  now destruct (nat_of_P_is_S p) as (n,->).
+  apply Pcompare_nat_compare.
 Qed.
 
 Lemma nat_of_Nmax :
   forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a').
 Proof.
-  intros; unfold Nmax; rewrite nat_of_Ncompare.
-  rewrite nat_compare_equiv; unfold nat_compare_alt.
-  destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|];
-    simpl; intros; symmetry; auto with arith.
-  apply max_r; rewrite e; auto with arith.
-Qed.
-
-Lemma N_of_max :
-  forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n').
-Proof.
-  intros.
-  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
-  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
-  rewrite <- nat_of_Nmax.
-  apply N_of_nat_of_N.
+  intros; unfold Nmax; rewrite nat_of_Ncompare. symmetry.
+  case nat_compare_spec; intros H; try rewrite H; auto with arith.
 Qed.
 
-(** Properties concerning [Z_of_N] *)
-
-Lemma Z_of_nat_of_N : forall n:N, Z_of_nat (nat_of_N n) = Z_of_N n.
-Proof.
-  destruct n; simpl; auto; symmetry; apply Zpos_eq_Z_of_nat_o_nat_of_P.
-Qed.
-
-Lemma Z_of_N_eq : forall n m, n = m -> Z_of_N n = Z_of_N m.
-Proof.
- intros; f_equal; assumption.
-Qed.
-
-Lemma Z_of_N_eq_rev : forall n m, Z_of_N n = Z_of_N m -> n = m.
-Proof.
- intros [|n] [|m]; simpl; intros; try discriminate; congruence.
-Qed.
-
-Lemma Z_of_N_eq_iff : forall n m, n = m <-> Z_of_N n = Z_of_N m.
-Proof.
- split; [apply Z_of_N_eq | apply Z_of_N_eq_rev].
-Qed.
-
-Lemma Z_of_N_le : forall n m, (n<=m)%N -> (Z_of_N n <= Z_of_N m)%Z.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_le_rev : forall n m, (Z_of_N n <= Z_of_N m)%Z -> (n<=m)%N.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_le_iff : forall n m, (n<=m)%N <-> (Z_of_N n <= Z_of_N m)%Z.
-Proof.
- split; [apply Z_of_N_le | apply Z_of_N_le_rev].
-Qed.
-
-Lemma Z_of_N_lt : forall n m, (n<m)%N -> (Z_of_N n < Z_of_N m)%Z.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_lt_rev : forall n m, (Z_of_N n < Z_of_N m)%Z -> (n<m)%N.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_lt_iff : forall n m, (n<m)%N <-> (Z_of_N n < Z_of_N m)%Z.
-Proof.
- split; [apply Z_of_N_lt | apply Z_of_N_lt_rev].
-Qed.
-
-Lemma Z_of_N_ge : forall n m, (n>=m)%N -> (Z_of_N n >= Z_of_N m)%Z.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_ge_rev : forall n m, (Z_of_N n >= Z_of_N m)%Z -> (n>=m)%N.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
-
-Lemma Z_of_N_ge_iff : forall n m, (n>=m)%N <-> (Z_of_N n >= Z_of_N m)%Z.
-Proof.
- split; [apply Z_of_N_ge | apply Z_of_N_ge_rev].
-Qed.
-
-Lemma Z_of_N_gt : forall n m, (n>m)%N -> (Z_of_N n > Z_of_N m)%Z.
+Lemma nat_of_Nmin :
+  forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a').
 Proof.
- intros [|n] [|m]; simpl; auto.
+  intros; unfold Nmin; rewrite nat_of_Ncompare. symmetry.
+  case nat_compare_spec; intros H; try rewrite H; auto with arith.
 Qed.
 
-Lemma Z_of_N_gt_rev : forall n m, (Z_of_N n > Z_of_N m)%Z -> (n>m)%N.
-Proof.
- intros [|n] [|m]; simpl; auto.
-Qed.
+Hint Rewrite nat_of_Ndouble nat_of_Ndouble_plus_one
+ nat_of_Nsucc nat_of_Nplus nat_of_Nmult nat_of_Nminus
+ nat_of_Npred nat_of_Ndiv2 nat_of_Nmax nat_of_Nmin : Nnat.
 
-Lemma Z_of_N_gt_iff : forall n m, (n>m)%N <-> (Z_of_N n > Z_of_N m)%Z.
+Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n).
 Proof.
- split; [apply Z_of_N_gt | apply Z_of_N_gt_rev].
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_of_nat : forall n:nat, Z_of_N (N_of_nat n) = Z_of_nat n.
+Lemma N_of_double_plus_one :
+  forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n).
 Proof.
- destruct n; simpl; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_pos : forall p:positive, Z_of_N (Npos p) = Zpos p.
+Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n).
 Proof.
- destruct p; simpl; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_abs : forall z:Z, Z_of_N (Zabs_N z) = Zabs z.
+Lemma N_of_pred : forall n, N_of_nat (pred n) = Npred (N_of_nat n).
 Proof.
- destruct z; simpl; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_le_0 : forall n, (0 <= Z_of_N n)%Z.
+Lemma N_of_plus :
+  forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n').
 Proof.
- destruct n; intro; discriminate.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_plus : forall n m:N, Z_of_N (n+m) = (Z_of_N n + Z_of_N m)%Z.
+Lemma N_of_minus :
+  forall n n', N_of_nat (n-n') = Nminus (N_of_nat n) (N_of_nat n').
 Proof.
- destruct n; destruct m; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_mult : forall n m:N, Z_of_N (n*m) = (Z_of_N n * Z_of_N m)%Z.
+Lemma N_of_mult :
+  forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n').
 Proof.
- destruct n; destruct m; auto.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_minus : forall n m:N, Z_of_N (n-m) = Zmax 0 (Z_of_N n - Z_of_N m).
+Lemma N_of_div2 :
+  forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n).
 Proof.
- intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nminus; apply inj_minus.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_succ : forall n:N, Z_of_N (Nsucc n) = Zsucc (Z_of_N n).
+Lemma N_of_nat_compare :
+ forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n').
 Proof.
- intros; do 2 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nsucc; apply inj_S.
+  intros. rewrite nat_of_Ncompare. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_min : forall n m:N, Z_of_N (Nmin n m) = Zmin (Z_of_N n) (Z_of_N m).
+Lemma N_of_min :
+  forall n n', N_of_nat (min n n') = Nmin (N_of_nat n) (N_of_nat n').
 Proof.
- intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmin; apply inj_min.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
 
-Lemma Z_of_N_max : forall n m:N, Z_of_N (Nmax n m) = Zmax (Z_of_N n) (Z_of_N m).
+Lemma N_of_max :
+  forall n n', N_of_nat (max n n') = Nmax (N_of_nat n) (N_of_nat n').
 Proof.
- intros; do 3 rewrite <- Z_of_nat_of_N; rewrite nat_of_Nmax; apply inj_max.
+  intros. apply nat_of_N_inj. now autorewrite with Nnat.
 Qed.
-