Numbers and bitwise functions.

 See NatInt/NZBits.v for the common axiomatization of bitwise functions
 over naturals / integers. Some specs aren't pretty, but easier to
 prove, see alternate statements in property functors {N,Z}Bits.
 Negative numbers are considered via the two's complement convention.

 We provide implementations for N (in Ndigits.v), for nat (quite dummy,
 just for completeness), for Z (new file Zdigits_def), for BigN
 (for the moment partly by converting to N, to be improved soon)
 and for BigZ.

 NOTA: For BigN.shiftl and BigN.shiftr, the two arguments are now in
 the reversed order (for consistency with the rest of the world):
 for instance BigN.shiftl 1 10 is 2^10.

 NOTA2: Zeven.Zdiv2 is _not_ doing (Zdiv _ 2), but rather (Zquot _ 2)
 on negative numbers. For the moment I've kept it intact, and have
 just added a Zdiv2' which is truly equivalent to (Zdiv _ 2).
 To reorganize someday ?

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

3 files changed, 317 insertions, 167 deletions

diff --git a/theories/NArith/BinNat.v b/theories/NArith/BinNat.v
index 51c5b462b..81e2e06e4 100644
--- a/theories/NArith/BinNat.v
+++ b/theories/NArith/BinNat.v
@@ -27,6 +27,13 @@ Arguments Scope Npos [positive_scope].
 
 Local Open Scope N_scope.
 
+(** Some local ad-hoc notation, since no interpretation of numerical
+  constants is available yet. *)
+
+Local Notation "0" := N0 : N_scope.
+Local Notation "1" := (Npos 1) : N_scope.
+Local Notation "2" := (Npos 2) : N_scope.
+
 Definition Ndiscr : forall n:N, { p:positive | n = Npos p } + { n = N0 }.
 Proof.
  destruct n; auto.
@@ -37,42 +44,59 @@ Defined.
 
 Definition Ndouble_plus_one x :=
   match x with
-  | N0 => Npos 1
-  | Npos p => Npos (xI p)
+  | 0 => Npos 1
+  | Npos p => Npos p~1
   end.
 
 (** Operation x -> 2*x *)
 
 Definition Ndouble n :=
   match n with
-  | N0 => N0
-  | Npos p => Npos (xO p)
+  | 0 => 0
+  | Npos p => Npos p~0
   end.
 
 (** Successor *)
 
 Definition Nsucc n :=
   match n with
-  | N0 => Npos 1
+  | 0 => Npos 1
   | Npos p => Npos (Psucc p)
   end.
 
 (** Predecessor *)
 
 Definition Npred (n : N) := match n with
-| N0 => N0
+| 0 => 0
 | Npos p => match p with
-  | xH => N0
+  | xH => 0
   | _ => Npos (Ppred p)
   end
 end.
 
+(** The successor of a N can be seen as a positive *)
+
+Definition Nsucc_pos (n : N) : positive :=
+ match n with
+   | N0 => 1%positive
+   | Npos p => Psucc p
+ end.
+
+(** Similarly, the predecessor of a positive, seen as a N *)
+
+Definition Ppred_N (p:positive) : N :=
+ match p with
+   | 1 => N0
+   | p~1 => Npos (p~0)
+   | p~0 => Npos (Pdouble_minus_one p)
+ end%positive.
+
 (** Addition *)
 
 Definition Nplus n m :=
   match n, m with
-  | N0, _ => m
-  | _, N0 => n
+  | 0, _ => m
+  | _, 0 => n
   | Npos p, Npos q => Npos (p + q)
   end.
 
@@ -82,12 +106,12 @@ Infix "+" := Nplus : N_scope.
 
 Definition Nminus (n m : N) :=
 match n, m with
-| N0, _ => N0
-| n, N0 => n
+| 0, _ => 0
+| n, 0 => n
 | Npos n', Npos m' =>
   match Pminus_mask n' m' with
   | IsPos p => Npos p
-  | _ => N0
+  | _ => 0
   end
 end.
 
@@ -97,8 +121,8 @@ Infix "-" := Nminus : N_scope.
 
 Definition Nmult n m :=
   match n, m with
-  | N0, _ => N0
-  | _, N0 => N0
+  | 0, _ => 0
+  | _, 0 => 0
   | Npos p, Npos q => Npos (p * q)
   end.
 
@@ -108,7 +132,7 @@ Infix "*" := Nmult : N_scope.
 
 Definition Neqb n m :=
  match n, m with
-  | N0, N0 => true
+  | 0, 0 => true
   | Npos n, Npos m => Peqb n m
   | _,_ => false
  end.
@@ -117,9 +141,9 @@ Definition Neqb n m :=
 
 Definition Ncompare n m :=
   match n, m with
-  | N0, N0 => Eq
-  | N0, Npos m' => Lt
-  | Npos n', N0 => Gt
+  | 0, 0 => Eq
+  | 0, Npos m' => Lt
+  | Npos n', 0 => Gt
   | Npos n', Npos m' => (n' ?= m')%positive Eq
   end.
 
@@ -162,7 +186,7 @@ Definition nat_of_N (a:N) :=
 
 Definition N_of_nat (n:nat) :=
   match n with
-  | O => N0
+  | O => 0
   | S n' => Npos (P_of_succ_nat n')
   end.
 
@@ -178,43 +202,43 @@ Defined.
 
 Lemma N_ind_double :
  forall (a:N) (P:N -> Prop),
-   P N0 ->
+   P 0 ->
    (forall a, P a -> P (Ndouble a)) ->
    (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
 Proof.
-  intros; elim a. trivial.
-  simple induction p. intros.
-  apply (H1 (Npos p0)); trivial.
-  intros; apply (H0 (Npos p0)); trivial.
-  intros; apply (H1 N0); assumption.
+ intros a P P0 P2 PS2. destruct a as [|p]. trivial.
+ induction p as [p IHp|p IHp| ].
+ now apply (PS2 (Npos p)).
+ now apply (P2 (Npos p)).
+ now apply (PS2 0).
 Qed.
 
 Lemma N_rec_double :
  forall (a:N) (P:N -> Set),
-   P N0 ->
+   P 0 ->
    (forall a, P a -> P (Ndouble a)) ->
    (forall a, P a -> P (Ndouble_plus_one a)) -> P a.
 Proof.
-  intros; elim a. trivial.
-  simple induction p. intros.
-  apply (H1 (Npos p0)); trivial.
-  intros; apply (H0 (Npos p0)); trivial.
-  intros; apply (H1 N0); assumption.
+ intros a P P0 P2 PS2. destruct a as [|p]. trivial.
+ induction p as [p IHp|p IHp| ].
+ now apply (PS2 (Npos p)).
+ now apply (P2 (Npos p)).
+ now apply (PS2 0).
 Qed.
 
 (** Peano induction on binary natural numbers *)
 
 Definition Nrect
-  (P : N -> Type) (a : P N0)
+  (P : N -> Type) (a : P 0)
     (f : forall n : N, P n -> P (Nsucc n)) (n : N) : P n :=
 let f' (p : positive) (x : P (Npos p)) := f (Npos p) x in
 let P' (p : positive) := P (Npos p) in
 match n return (P n) with
-| N0 => a
-| Npos p => Prect P' (f N0 a) f' p
+| 0 => a
+| Npos p => Prect P' (f 0 a) f' p
 end.
 
-Theorem Nrect_base : forall P a f, Nrect P a f N0 = a.
+Theorem Nrect_base : forall P a f, Nrect P a f 0 = a.
 Proof.
 intros P a f; simpl; reflexivity.
 Qed.
@@ -229,7 +253,7 @@ Definition Nind (P : N -> Prop) := Nrect P.
 
 Definition Nrec (P : N -> Set) := Nrect P.
 
-Theorem Nrec_base : forall P a f, Nrec P a f N0 = a.
+Theorem Nrec_base : forall P a f, Nrec P a f 0 = a.
 Proof.
 intros P a f; unfold Nrec; apply Nrect_base.
 Qed.
@@ -248,14 +272,43 @@ case_eq (Psucc p); try (intros q H; rewrite <- H; now rewrite Ppred_succ).
 intro H; false_hyp H Psucc_not_one.
 Qed.
 
+Theorem Npred_minus : forall n, Npred n = Nminus n (Npos 1).
+Proof.
+ intros [|[p|p|]]; trivial.
+Qed.
+
+Lemma Nsucc_pred : forall n, n<>0 -> Nsucc (Npred n) = n.
+Proof.
+ intros [|n] H; (now destruct H) || clear H.
+ rewrite Npred_minus. simpl. destruct n; simpl; trivial.
+ f_equal; apply Psucc_o_double_minus_one_eq_xO.
+Qed.
+
+(** Properties of mixed successor and predecessor. *)
+
+Lemma Ppred_N_spec : forall p, Ppred_N p = Npred (Npos p).
+Proof.
+ now destruct p.
+Qed.
+
+Lemma Nsucc_pos_spec : forall n, Npos (Nsucc_pos n) = Nsucc n.
+Proof.
+ now destruct n.
+Qed.
+
+Lemma Ppred_Nsucc : forall n, Ppred_N (Nsucc_pos n) = n.
+Proof.
+ intros. now rewrite Ppred_N_spec, Nsucc_pos_spec, Npred_succ.
+Qed.
+
 (** Properties of addition *)
 
-Theorem Nplus_0_l : forall n:N, N0 + n = n.
+Theorem Nplus_0_l : forall n:N, 0 + n = n.
 Proof.
 reflexivity.
 Qed.
 
-Theorem Nplus_0_r : forall n:N, n + N0 = n.
+Theorem Nplus_0_r : forall n:N, n + 0 = n.
 Proof.
 destruct n; reflexivity.
 Qed.
@@ -285,7 +338,7 @@ destruct n, m.
   simpl; rewrite Pplus_succ_permute_l; reflexivity.
 Qed.
 
-Theorem Nsucc_0 : forall n : N, Nsucc n <> N0.
+Theorem Nsucc_0 : forall n : N, Nsucc n <> 0.
 Proof.
 now destruct n.
 Qed.
@@ -308,7 +361,7 @@ Qed.
 
 (** Properties of subtraction. *)
 
-Lemma Nminus_N0_Nle : forall n n' : N, n - n' = N0 <-> n <= n'.
+Lemma Nminus_N0_Nle : forall n n' : N, n - n' = 0 <-> n <= n'.
 Proof.
 intros [| p] [| q]; unfold Nle; simpl;
 split; intro H; try easy.
@@ -319,7 +372,7 @@ subst. now rewrite Pminus_mask_diag.
 now rewrite Pminus_mask_Lt.
 Qed.
 
-Theorem Nminus_0_r : forall n : N, n - N0 = n.
+Theorem Nminus_0_r : forall n : N, n - 0 = n.
 Proof.
 now destruct n.
 Qed.
@@ -332,14 +385,9 @@ simpl. rewrite Pminus_mask_succ_r, Pminus_mask_carry_spec.
 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 *)
 
-Theorem Nmult_0_l : forall n:N, N0 * n = N0.
+Theorem Nmult_0_l : forall n:N, 0 * n = 0.
 Proof.
 reflexivity.
 Qed.
@@ -386,7 +434,7 @@ Proof.
 intros. rewrite ! (Nmult_comm p); apply Nmult_plus_distr_r.
 Qed.
 
-Theorem Nmult_reg_r : forall n m p:N, p <> N0 -> n * p = m * p -> n = m.
+Theorem Nmult_reg_r : forall n m p:N, p <> 0 -> n * p = m * p -> n = m.
 Proof.
 destruct p; intros Hp H.
 contradiction Hp; reflexivity.
@@ -405,6 +453,11 @@ Qed.
 
 (** Properties of comparison *)
 
+Lemma Nle_0 : forall n, 0<=n.
+Proof.
+ now destruct n.
+Qed.
+
 Lemma Ncompare_refl : forall n, (n ?= n) = Eq.
 Proof.
 destruct n; simpl; auto.
@@ -524,7 +577,7 @@ Qed.
 
 (** 0 is the least natural number *)
 
-Theorem Ncompare_0 : forall n : N, Ncompare n N0 <> Lt.
+Theorem Ncompare_0 : forall n : N, Ncompare n 0 <> Lt.
 Proof.
 destruct n; discriminate.
 Qed.
@@ -533,8 +586,8 @@ Qed.
 
 Definition Ndiv2 (n:N) :=
   match n with
-  | N0 => N0
-  | Npos 1 => N0
+  | 0 => 0
+  | Npos 1 => 0
   | Npos (p~0) => Npos p
   | Npos (p~1) => Npos p
   end.
@@ -565,14 +618,14 @@ Qed.
 
 Definition Npow n p :=
   match p, n with
-    | N0, _ => Npos 1
-    | _, N0 => N0
+    | 0, _ => Npos 1
+    | _, 0 => 0
     | Npos p, Npos q => Npos (Ppow q p)
   end.
 
 Infix "^" := Npow : N_scope.
 
-Lemma Npow_0_r : forall n, n ^ N0 = Npos 1.
+Lemma Npow_0_r : forall n, n ^ 0 = Npos 1.
 Proof. reflexivity. Qed.
 
 Lemma Npow_succ_r : forall n p, n^(Nsucc p) = n * n^p.
@@ -585,13 +638,13 @@ Qed.
 
 Definition Nlog2 n :=
  match n with
-   | N0 => N0
-   | Npos 1 => N0
+   | 0 => 0
+   | Npos 1 => 0
    | Npos (p~0) => Npos (Psize_pos p)
    | Npos (p~1) => Npos (Psize_pos p)
  end.
 
-Lemma Nlog2_spec : forall n, N0 < n ->
+Lemma Nlog2_spec : forall n, 0 < n ->
  (Npos 2)^(Nlog2 n) <= n < (Npos 2)^(Nsucc (Nlog2 n)).
 Proof.
  intros [|[p|p|]] H; discriminate H || clear H; simpl; split.
@@ -605,7 +658,7 @@ Proof.
  reflexivity.
 Qed.
 
-Lemma Nlog2_nonpos : forall n, n<=N0 -> Nlog2 n = N0.
+Lemma Nlog2_nonpos : forall n, n<=0 -> Nlog2 n = 0.
 Proof.
  intros [|n] Hn. reflexivity. now destruct Hn.
 Qed.
@@ -614,19 +667,16 @@ Qed.
 
 Definition Neven n :=
   match n with
-    | N0 => true
+    | 0 => true
     | Npos (xO _) => true
     | _ => false
   end.
 Definition Nodd n := negb (Neven n).
 
-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.
  destruct n.
- split. now exists N0.
+ split. now exists 0.
  trivial.
  destruct p; simpl; split; trivial; try discriminate.
  intros (m,H). now destruct m.
@@ -642,5 +692,5 @@ Proof.
  destruct p; simpl; split; trivial; try discriminate.
  exists (Npos p). reflexivity.
  intros (m,H). now destruct m.
- exists N0. reflexivity.
+ exists 0. reflexivity.
 Qed.
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 98e88c6a2..0dd2fceaa 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Import Bool Morphisms Setoid Bvector BinPos BinNat Wf_nat
- Pnat Nnat Ndiv_def.
+ Pnat Nnat Ndiv_def Compare_dec Lt Minus.
 
 Local Open Scope positive_scope.
 
@@ -192,12 +192,79 @@ Proof.
  destruct a. trivial. apply Pbit_Ptestbit.
 Qed.
 
+(** Correctness proof for [Ntestbit].
+
+    Ideally, we would say that (Ntestbit a n) is (a/2^n) mod 2
+    but that requires results about division we don't have yet.
+    Instead, we use a longer but simplier specification, and
+    obtain the nice equation later as a derived property.
+*)
+
+Lemma Nsuccdouble_bounds : forall n p, n<p -> 1+2*n<2*p.
+Proof.
+ intros [|n] [|p] H; try easy.
+ change (n<p)%positive in H. apply Ple_succ_l in H.
+ change (n~1 < p~0)%positive. apply Ple_succ_l. exact H.
+Qed.
+
+Lemma Ntestbit_spec : forall a n,
+  exists l, exists h, 0<=l<2^n /\
+    a = l + ((if Ntestbit a n then 1 else 0) + 2*h)*2^n.
+Proof.
+ intros [|a] n.
+ exists 0. exists 0. simpl; repeat split; now destruct n.
+ revert n. induction a as [a IH|a IH| ]; destruct n.
+ (* a~1, n=0 *)
+ exists 0. exists (Npos a). simpl. repeat split; now rewrite ?Pmult_1_r.
+ (* a~1 n>0 *)
+ destruct (IH (Npred (Npos p))) as (l & h & (_,H) & EQ). clear IH.
+ exists (1+2*l). exists h.
+ set (b := if Ntestbit (Npos a) (Npred (Npos p)) then 1 else 0) in EQ.
+ change (if Ntestbit _ _ then 1 else 0) with b.
+ rewrite <- (Nsucc_pred (Npos p)), Npow_succ_r by discriminate.
+ set (p' := Npred (Npos p)) in *.
+ split. split. apply Nle_0. now apply Nsuccdouble_bounds.
+ change (Npos a~1) with (1+2*(Npos a)). rewrite EQ.
+ rewrite <-Nplus_assoc. f_equal.
+ rewrite Nmult_plus_distr_l. f_equal.
+ now rewrite !Nmult_assoc, (Nmult_comm 2).
+ (* a~0 n=0 *)
+ exists 0. exists (Npos a). simpl. repeat split; now rewrite ?Pmult_1_r.
+ (* a~0 n>0 *)
+ destruct (IH (Npred (Npos p))) as (l & h & (_,H) & EQ). clear IH.
+ exists (2*l). exists h.
+ set (b := if Ntestbit (Npos a) (Npred (Npos p)) then 1 else 0) in EQ.
+ change (if Ntestbit _ _ then 1 else 0) with b.
+ rewrite <- (Nsucc_pred (Npos p)), !Npow_succ_r by discriminate.
+ set (p' := Npred (Npos p)) in *.
+ split. split. apply Nle_0. now destruct l, (2^p').
+ change (Npos a~0) with (2*(Npos a)). rewrite EQ.
+ rewrite Nmult_plus_distr_l. f_equal.
+ now rewrite !Nmult_assoc, (Nmult_comm 2).
+ (* 1 n=0 *)
+ exists 0. exists 0. simpl. now repeat split.
+ (* 1 n>0 *)
+ exists 1. exists 0. simpl. repeat split. easy. now apply Ppow_gt_1.
+Qed.
+
 (** Equivalence of shifts, N and nat versions *)
 
+Lemma Nshiftr_nat_S : forall a n,
+ Nshiftr_nat a (S n) = Ndiv2 (Nshiftr_nat a n).
+Proof.
+ reflexivity.
+Qed.
+
+Lemma Nshiftl_nat_S : forall a n,
+ Nshiftl_nat a (S n) = Ndouble (Nshiftl_nat a n).
+Proof.
+ reflexivity.
+Qed.
+
 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.
+ intros a [|n]; simpl. unfold Nshiftr_nat.
  trivial.
  symmetry. apply iter_nat_of_P.
 Qed.
@@ -224,166 +291,199 @@ Qed.
 
 (** Correctness proofs for shifts *)
 
-Lemma Nshiftl_mult_pow : forall a n, Nshiftl a n = a * 2^n.
+Lemma Nshiftr_nat_spec : forall a n m,
+  Nbit (Nshiftr_nat a n) m = Nbit a (m+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.
+ induction n; intros m.
+ now rewrite <- plus_n_O.
+ simpl. rewrite <- plus_n_Sm, <- plus_Sn_m, <- IHn, Nshiftr_nat_S.
+ destruct (Nshiftr_nat a n) as [|[p|p|]]; simpl; trivial.
 Qed.
 
-(*
-Lemma Nshiftr_div_pow : forall a n, Nshiftr a n = a / 2^n.
-*)
-
-(** Equality over functional streams of bits *)
+Lemma Nshiftr_spec : forall a n m,
+ Ntestbit (Nshiftr a n) m = Ntestbit a (m+n).
+Proof.
+ intros.
+ rewrite <- Nshiftr_nat_equiv, <- !Nbit_Ntestbit, nat_of_Nplus.
+ apply Nshiftr_nat_spec.
+Qed.
 
-Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.
+Lemma Nshiftl_nat_spec_high : forall a n m, (n<=m)%nat ->
+  Nbit (Nshiftl_nat a n) m = Nbit a (m-n).
+Proof.
+ induction n; intros m H.
+ now rewrite <- minus_n_O.
+ destruct m. inversion H. apply le_S_n in H.
+ simpl. rewrite <- IHn, Nshiftl_nat_S; trivial.
+ destruct (Nshiftl_nat a n) as [|[p|p|]]; simpl; trivial.
+Qed.
 
-Instance eqf_equiv : Equivalence eqf.
+Lemma Nshiftl_spec_high : forall a n m, n<=m ->
+ Ntestbit (Nshiftl a n) m = Ntestbit a (m-n).
 Proof.
- split; congruence.
+ intros.
+ rewrite <- Nshiftl_nat_equiv, <- !Nbit_Ntestbit, nat_of_Nminus.
+ apply Nshiftl_nat_spec_high.
+ apply nat_compare_le. now rewrite <- nat_of_Ncompare.
 Qed.
 
-Local Infix "==" := eqf (at level 70, no associativity).
+Lemma Nshiftl_nat_spec_low : forall a n m, (m<n)%nat ->
+ Nbit (Nshiftl_nat a n) m = false.
+Proof.
+ induction n; intros m H. inversion H.
+ rewrite Nshiftl_nat_S.
+ destruct m.
+ destruct (Nshiftl_nat a n); trivial.
+ specialize (IHn m (lt_S_n _ _ H)).
+ destruct (Nshiftl_nat a n); trivial.
+Qed.
 
-(** If two numbers produce the same stream of bits, they are equal. *)
+Lemma Nshiftl_spec_low : forall a n m, m<n ->
+ Ntestbit (Nshiftl a n) m = false.
+Proof.
+ intros.
+ rewrite <- Nshiftl_nat_equiv, <- Nbit_Ntestbit.
+ apply Nshiftl_nat_spec_low.
+ apply nat_compare_lt. now rewrite <- nat_of_Ncompare.
+Qed.
 
-Local Notation Step H := (fun n => H (S n)).
+(** Semantics of bitwise operations *)
 
-Lemma Pbit_faithful_0 : forall p, ~(Pbit p == (fun _ => false)).
+Lemma Pxor_semantics : forall p p' n,
+ Nbit (Pxor p p') n = xorb (Pbit p n) (Pbit p' n).
 Proof.
- induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O).
-  apply (IHp (Step H)).
+ induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl;
+  (specialize (IHp p'); destruct Pxor; trivial; apply (IHp n)) ||
+  now destruct Pbit.
 Qed.
 
-Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'.
+Lemma Nxor_semantics : forall a a' n,
+ Nbit (Nxor a a') n = xorb (Nbit a n) (Nbit a' n).
 Proof.
- 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)).
+ intros [|p] [|p'] n; simpl; trivial.
+ now destruct Pbit.
+ now destruct Pbit.
+ apply Pxor_semantics.
 Qed.
 
-Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'.
+Lemma Nxor_spec : forall a a' n,
+ Ntestbit (Nxor a a') n = xorb (Ntestbit a n) (Ntestbit a' n).
 Proof.
- intros [|p] [|p'] H; trivial.
- symmetry in H. destruct (Pbit_faithful_0 _ H).
- destruct (Pbit_faithful_0 _ H).
- f_equal. apply Pbit_faithful, H.
+ intros. rewrite <- !Nbit_Ntestbit. apply Nxor_semantics.
 Qed.
 
-Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'.
+Lemma Por_semantics : forall p p' n,
+ Pbit (Por p p') n = (Pbit p n) || (Pbit p' n).
 Proof.
- split. apply Nbit_faithful. intros; now subst.
+ induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial;
+  apply (IHp p' n) || now rewrite orb_false_r.
 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).
-
-Instance eqf_orf : Proper (eqf==>eqf==>eqf) orf.
+Lemma Nor_semantics : forall a a' n,
+ Nbit (Nor a a') n = (Nbit a n) || (Nbit a' n).
 Proof.
-  unfold orf. congruence.
+ intros [|p] [|p'] n; simpl; trivial.
+ now rewrite orb_false_r.
+ apply Por_semantics.
 Qed.
 
-Instance eqf_andf : Proper (eqf==>eqf==>eqf) andf.
+Lemma Nor_spec : forall a a' n,
+ Ntestbit (Nor a a') n = (Ntestbit a n) || (Ntestbit a' n).
 Proof.
-  unfold andf. congruence.
+ intros. rewrite <- !Nbit_Ntestbit. apply Nor_semantics.
 Qed.
 
-Instance eqf_difff : Proper (eqf==>eqf==>eqf) difff.
+Lemma Pand_semantics : forall p p' n,
+ Nbit (Pand p p') n = (Pbit p n) && (Pbit p' n).
 Proof.
-  unfold difff. congruence.
+ induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl;
+  (specialize (IHp p'); destruct Pand; trivial; apply (IHp n)) ||
+  now rewrite andb_false_r.
 Qed.
 
-Instance eqf_xorf : Proper (eqf==>eqf==>eqf) xorf.
+Lemma Nand_semantics : forall a a' n,
+ Nbit (Nand a a') n = (Nbit a n) && (Nbit a' n).
 Proof.
-  unfold xorf. congruence.
+ intros [|p] [|p'] n; simpl; trivial.
+ now rewrite andb_false_r.
+ apply Pand_semantics.
 Qed.
 
-(** We now describe the semantics of [Nxor] and other bitwise
-  operations in terms of bit streams. *)
-
-Lemma Pxor_semantics : forall p p',
- Nbit (Pxor p p') == xorf (Pbit p) (Pbit p').
+Lemma Nand_spec : forall a a' n,
+ Ntestbit (Nand a a') n = (Ntestbit a n) && (Ntestbit a' n).
 Proof.
- 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).
+ intros. rewrite <- !Nbit_Ntestbit. apply Nand_semantics.
 Qed.
 
-Lemma Nxor_semantics : forall a a',
- Nbit (Nxor a a') == xorf (Nbit a) (Nbit a').
+Lemma Pdiff_semantics : forall p p' n,
+ Nbit (Pdiff p p') n = (Pbit p n) && negb (Pbit p' n).
 Proof.
- intros [|p] [|p'] n; simpl; unfold xorf; trivial.
- now rewrite xorb_false_l.
- now rewrite xorb_false_r.
- apply Pxor_semantics.
+ induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial; simpl;
+  (specialize (IHp p'); destruct Pdiff; trivial; apply (IHp n)) ||
+  now rewrite andb_true_r.
 Qed.
 
-Lemma Por_semantics : forall p p',
- Pbit (Por p p') == orf (Pbit p) (Pbit p').
+Lemma Ndiff_semantics : forall a a' n,
+ Nbit (Ndiff a a') n = (Nbit a n) && negb (Nbit a' n).
 Proof.
- induction p as [p IHp|p IHp|]; intros [p'|p'|] [|n]; trivial;
-  unfold orf; apply (IHp p' n) || now rewrite orb_false_r.
+ intros [|p] [|p'] n; simpl; trivial.
+ simpl. now rewrite andb_true_r.
+ apply Pdiff_semantics.
 Qed.
 
-Lemma Nor_semantics : forall a a',
- Nbit (Nor a a') == orf (Nbit a) (Nbit a').
+Lemma Ndiff_spec : forall a a' n,
+ Ntestbit (Ndiff a a') n = (Ntestbit a n) && negb (Ntestbit a' n).
 Proof.
- intros [|p] [|p'] n; simpl; unfold orf; trivial.
- now rewrite orb_false_r.
- apply Por_semantics.
+ intros. rewrite <- !Nbit_Ntestbit. apply Ndiff_semantics.
 Qed.
 
-Lemma Pand_semantics : forall p p',
- Nbit (Pand p p') == andf (Pbit p) (Pbit p').
+
+(** Equality over functional streams of bits *)
+
+Definition eqf (f g:nat -> bool) := forall n:nat, f n = g n.
+
+Program Instance eqf_equiv : Equivalence eqf.
+
+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.
- 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).
+ induction p as [p IHp|p IHp| ]; intros H; try discriminate (H O).
+  apply (IHp (Step H)).
 Qed.
 
-Lemma Nand_semantics : forall a a',
- Nbit (Nand a a') == andf (Nbit a) (Nbit a').
+Lemma Pbit_faithful : forall p p', Pbit p == Pbit p' -> p = p'.
 Proof.
- intros [|p] [|p'] n; simpl; unfold andf; trivial.
- now rewrite andb_false_r.
- apply Pand_semantics.
+ 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 Pdiff_semantics : forall p p',
- Nbit (Pdiff p p') == difff (Pbit p) (Pbit p').
+Lemma Nbit_faithful : forall n n', Nbit n == Nbit n' -> n = n'.
 Proof.
- 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).
+ 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 Ndiff_semantics : forall a a',
- Nbit (Ndiff a a') == difff (Nbit a) (Nbit a').
+Lemma Nbit_faithful_iff : forall n n', Nbit n == Nbit n' <-> n = n'.
 Proof.
- intros [|p] [|p'] n; simpl; unfold difff; trivial.
- simpl. now rewrite andb_true_r.
- apply Pdiff_semantics.
+ split. apply Nbit_faithful. intros; now subst.
 Qed.
 
 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.
+ apply Nbit_faithful; intro n; autorewrite with bitwise_semantics.
 
 (** Now, we can easily deduce properties of [Nxor] and others
     from properties of [xorb] and others. *)
@@ -391,7 +491,7 @@ Ltac bitwise_semantics :=
 Lemma Nxor_eq : forall a a', Nxor a a' = 0 -> a = a'.
 Proof.
  intros a a' H. bitwise_semantics. apply xorb_eq.
- rewrite <- Nbit_faithful_iff, Nxor_semantics in H. apply H.
+ now rewrite <- Nxor_semantics, H.
 Qed.
 
 Lemma Nxor_nilpotent : forall a, Nxor a a = 0.
@@ -593,7 +693,7 @@ 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' O).
-  unfold xorf. rewrite Nbit0_correct, Nbit0_correct. reflexivity.
+  rewrite Nbit0_correct, Nbit0_correct. reflexivity.
 Qed.
 
 Lemma Nxor_div2 :
@@ -601,7 +701,7 @@ Lemma Nxor_div2 :
 Proof.
   intros. apply Nbit_faithful. unfold eqf. intro.
   rewrite (Nxor_semantics (Ndiv2 a) (Ndiv2 a') n), Ndiv2_correct, (Nxor_semantics a a' (S n)).
-  unfold xorf. rewrite 2! Ndiv2_correct.
+  rewrite 2! Ndiv2_correct.
   reflexivity.
 Qed.
 
diff --git a/theories/NArith/Ndist.v b/theories/NArith/Ndist.v
index 0b61718f8..9d399f5cd 100644
--- a/theories/NArith/Ndist.v
+++ b/theories/NArith/Ndist.v
@@ -301,7 +301,7 @@ Proof.
   cut (forall a'':N, Nxor (Npos p) a' = a'' -> Nbit a'' k = false).
   intros. apply H1. reflexivity.
   intro a''. case a''. intro. reflexivity.
-  intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k). unfold xorf in |- *.
+  intros. rewrite <- H1. rewrite (Nxor_semantics (Npos p) a' k).
   rewrite
    (Nplength_zeros (Npos p) (Pplength p)
       (refl_equal (Nplength (Npos p))) k H0).