Move a part of PeanoNat to Natural

There is still an issue with `div2_double` and `div2_succ_double`.
It's not possible to factor these because there are different such
lemmas in `PeanoNat` and `BinNat`.
So we settle for `div2_even` and `div2_odd'` in `NBits`.
`div2_even` will appear twice (the other name is `div2_double`) in
`PeanoNat`. Maybe this is not a big problem?

The naming convention in Numbers is now (mostly) that
- `even` after an operation name means (2 * n)
- `odd` after an operation name means (2 * n + 1)
- `even` as a prefix means it is about the boolean operation `even`
- `same` for `odd`

Unfortunately this clashes with `div2_odd`, hence the name `div2_odd'`.

There are still some questions about the `div2` inequalities (some new
in `NBits`, some imported from `PeanoNat`); some of which are very
similar.

theories/Arith/PeanoNat.v

@@ -624,6 +624,65 @@ Proof. apply le_0_l. Qed.
 
 (** ** Bitwise operations *)
 
+Definition double_S : forall n, double (S n) = S (S (double n))
+                    := fun n => add_succ_r (S n) n.
+
+Definition double_add : forall n m, double (n + m) = double n + double m
+                      := fun n m => add_shuffle1 n m n m.
+
+Lemma double_twice : forall n, double n = 2*n.
+Proof. simpl; intros; now rewrite add_0_r. Qed.
+
+(* We use a Module Type to hide intermediate lemmas we will get from Natural
+   anyway. *)
+Module Type PrivateBitwiseSpec.
+  (* needed to implement Numbers.NatInt.NZBitsSpec *)
+  Parameter testbit_odd_0 : forall a : nat, testbit (add (mul 2 a) 1) 0 = true.
+  Parameter testbit_even_0 : forall a : nat, testbit (mul 2 a) 0 = false.
+  Parameter testbit_odd_succ : forall a n : nat, le 0 n ->
+    testbit (add (mul 2 a) 1) (succ n) = testbit a n.
+  Parameter testbit_even_succ : forall a n : nat, le 0 n ->
+    testbit (mul 2 a) (succ n) = testbit a n.
+  Parameter testbit_neg_r : forall a n : nat, lt n 0 -> testbit a n = false.
+  Parameter shiftr_spec : forall a n m : nat, le 0 m ->
+    testbit (shiftr a n) m = testbit a (add m n).
+  Parameter shiftl_spec_high :
+    forall a n m : nat, le 0 m ->
+    le n m -> testbit (shiftl a n) m = testbit a (sub m n).
+  Parameter shiftl_spec_low :
+    forall a n m : nat, lt m n -> testbit (shiftl a n) m = false.
+  Parameter land_spec :
+    forall a b n : nat, testbit (land a b) n = testbit a n && testbit b n.
+  Parameter lor_spec :
+    forall a b n : nat, testbit (lor a b) n = testbit a n || testbit b n.
+  Parameter ldiff_spec :
+    forall a b n : nat,
+    testbit (ldiff a b) n = testbit a n && negb (testbit b n).
+  Parameter lxor_spec :
+    forall a b n : nat, testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
+  Parameter div2_spec :
+    forall a : nat, eq (div2 a) (shiftr a 1).
+  (* not yet generalized to Numbers.Natural.Abstract *)
+  Parameter div2_double : forall n, div2 (2*n) = n.
+  Parameter div2_succ_double : forall n, div2 (S (2*n)) = n.
+  Parameter div2_bitwise : forall op n a b,
+    div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).
+  Parameter odd_bitwise : forall op n a b,
+    odd (bitwise op (S n) a b) = op (odd a) (odd b).
+  Parameter 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).
+  Parameter 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).
+End PrivateBitwiseSpec.
+
+(* The following module has to be included (it semmes that importing it is not
+   enough to implement NZBitsSpec), therefore it has to be "Private", otherwise,
+   its lemmas will appear twice in [Search]es *)
+
+Module PrivateImplementsBitwiseSpec : PrivateBitwiseSpec.
+
 Lemma div2_double n : div2 (2*n) = n.
 Proof.
   induction n; trivial.
@@ -664,21 +723,15 @@ Proof.
     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.
-
-Definition double_S : forall n, double (S n) = S (S (double n))
-                    := fun n => add_succ_r (S n) n.
-
-Definition double_add : forall n m, double (n + m) = double n + double m
-                      := fun n m => add_shuffle1 n m n m.
-
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Lemma testbit_0_l : forall n, testbit 0 n = false.
 Proof. now intro n; induction n. Qed.
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.
 Proof. unfold testbit; rewrite odd_spec; now exists a. Qed.
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Lemma testbit_even_0 a : testbit (2*a) 0 = false.
 Proof.
   unfold testbit, odd.
@@ -716,6 +769,7 @@ Proof.
     now apply IHn.
 Qed.
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Lemma shiftl_spec_low : forall a n m, m<n ->
   testbit (shiftl a n) m = false.
 Proof.
@@ -731,6 +785,7 @@ Proof.
     now apply succ_le_mono.
 Qed.
 
+(* not yet generalized, part of the interface at this point *)
 Lemma div2_bitwise : forall op n a b,
   div2 (bitwise op (S n) a b) = bitwise op n (div2 a) (div2 b).
 Proof.
@@ -740,6 +795,7 @@ Proof.
   - now rewrite add_0_l, div2_double.
 Qed.
 
+(* not yet generalized, part of the interface at this point *)
 Lemma odd_bitwise : forall op n a b,
   odd (bitwise op (S n) a b) = op (odd a) (odd b).
 Proof.
@@ -752,6 +808,7 @@ Proof.
     rewrite add_0_l; eexists; eauto.
 Qed.
 
+(* not yet generalized, part of the interface at this point *)
 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).
@@ -766,6 +823,7 @@ Proof.
       apply IHn; now apply div2_decr.
 Qed.
 
+(* not yet generalized, part of the interface at this point *)
 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).
@@ -780,14 +838,17 @@ Proof.
       apply IHn; now apply div2_decr.
 Qed.
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 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.
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 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.
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Lemma lor_spec a b n :
   testbit (lor a b) n = testbit a n || testbit b n.
 Proof.
@@ -803,6 +864,7 @@ Proof.
     + now apply lt_le_incl in H; rewrite max_l.
 Qed.
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Lemma lxor_spec a b n :
   testbit (lxor a b) n = xorb (testbit a n) (testbit b n).
 Proof.
@@ -818,18 +880,29 @@ Proof.
     + now apply lt_le_incl in H; rewrite max_l.
 Qed.
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Lemma div2_spec a : div2 a = shiftr a 1.
 Proof. reflexivity. Qed.
 
 (** Aliases with extra dummy hypothesis, to fulfil the interface *)
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ' a n.
+
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ' a n.
+
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Lemma testbit_neg_r a n (H:n<0) : testbit a n = false.
 Proof. inversion H. Qed.
 
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Definition shiftl_spec_high a n m (_:0<=m) := shiftl_specif_high a n m.
+
+(* needed to implement Coq.Numbers.NatInt.NZBitsSpec *)
 Definition shiftr_spec a n m (_:0<=m) := shiftr_specif a n m.
+End PrivateImplementsBitwiseSpec.
+Include PrivateImplementsBitwiseSpec.
 
 Lemma div_0_r a : a / 0 = 0.
 Proof. reflexivity. Qed.

theories/Numbers/NatInt/NZParity.v

@@ -268,16 +268,16 @@ Qed.
 
 (** Parity of [2 * n] and [2 * n + 1] *)
 
-Lemma even_double : forall n, even (2 * n) = true.
+Lemma even_even : forall n, even (2 * n) = true.
 Proof. intros n; apply even_spec; exists n; reflexivity. Qed.
 
-Lemma odd_double : forall n, odd (2 * n) = false.
-Proof. intros n; rewrite <-(negb_even), even_double; reflexivity. Qed.
+Lemma odd_even : forall n, odd (2 * n) = false.
+Proof. intros n; rewrite <-(negb_even), even_even; reflexivity. Qed.
 
-Lemma odd_succ_double : forall n, odd (2 * n + 1) = true.
+Lemma odd_odd : forall n, odd (2 * n + 1) = true.
 Proof. intros n; rewrite odd_spec; exists n; reflexivity. Qed.
 
-Lemma even_succ_double : forall n, even (2 * n + 1) = false.
-Proof. intros n; rewrite <-(negb_odd), odd_succ_double; reflexivity. Qed.
+Lemma even_odd : forall n, even (2 * n + 1) = false.
+Proof. intros n; rewrite <-(negb_odd), odd_odd; reflexivity. Qed.
 
 End NZParityProp.

theories/Numbers/Natural/Abstract/NBits.v

@@ -99,6 +99,13 @@ Proof.
  - apply testbit_even_succ, le_0_l.
 Qed.
 
+(** Specification without useless condition on the bit number *)
+Lemma testbit_odd_succ' a n : testbit (2*a+1) (S n) = testbit a n.
+Proof. apply testbit_odd_succ; exact (le_0_l n). Qed.
+
+Lemma testbit_even_succ' a n : testbit (2*a) (S n) = testbit a n.
+Proof. apply testbit_even_succ; exact (le_0_l n). Qed.
+
 (** Alternative characterisations of [testbit] *)
 
 (** This concise equation could have been taken as specification
@@ -573,6 +580,21 @@ Proof.
  intros. rewrite div2_spec, shiftr_div_pow2. now nzsimpl.
 Qed.
 
+Lemma div2_0 : div2 0 == 0.
+Proof.
+  rewrite div2_div, div_0_l by (rewrite two_succ; exact (neq_succ_0 _)).
+  reflexivity.
+Qed.
+
+Lemma div2_1 : div2 1 == 0.
+Proof. rewrite div2_div, div_small by (exact lt_1_2); reflexivity. Qed.
+
+Lemma div2_le_mono : forall a b, a <= b -> div2 a <= div2 b.
+Proof.
+  intros a b H; rewrite 2!div2_div; apply div_le_mono; [| exact H].
+  rewrite two_succ; exact (neq_succ_0 1).
+Qed.
+
 #[global]
 Instance div2_wd : Proper (eq==>eq) div2.
 Proof.
@@ -621,9 +643,7 @@ Proof.
     intros H'; contradict H'; rewrite H; reflexivity.
   }
   destruct (zero_or_succ b) as [| [c ->]]; [| clear b]. {
-    intros _; rewrite H; setoid_replace (S 0) with (2 * 0 + 1)
-      by (rewrite mul_0_r, add_0_l, one_succ; reflexivity).
-    rewrite div2_odd', mul_0_r, add_0_l; exact lt_0_1.
+    intros _; rewrite H, <-one_succ, div2_1; exact lt_0_1.
   }
   intros _; rewrite (div2_odd (S (S c))) at 2.
   rewrite <-(mul_1_l (div2 _)) at 1; apply lt_lt_add_r, mul_lt_mono_pos_r;
@@ -633,6 +653,29 @@ Proof.
   apply ->succ_le_mono; apply ->succ_le_mono; exact (le_0_l _).
 Qed.
 
+Lemma le_div2 n : div2 (S n) <= n.
+Proof.
+  destruct (zero_or_succ n) as [-> | [k ->]]; [| clear n]. {
+    rewrite <-one_succ, div2_1; exact (le_0_l 0).
+  }
+  apply div2_le_upper_bound.
+  setoid_replace (2 * (S k)) with (S k + S k); cycle 1. {
+    rewrite two_succ, <-(add_1_r 1), mul_add_distr_r, mul_1_l; reflexivity.
+  }
+  rewrite add_succ_r; apply ->succ_le_mono; exact (le_add_r _ _).
+Qed.
+
+Lemma lt_div2 n : 0 < n -> div2 n < n.
+Proof. intros H%lt_neq%neq_sym; exact (lt_div2_diag_l _ H). Qed.
+
+Lemma div2_decr a n : a <= S n -> div2 a <= n.
+Proof.
+  destruct (zero_or_succ a) as [-> | [b ->]]; [intros _ | clear a]. {
+    rewrite div2_0; exact (le_0_l _).
+  }
+  intros H%div2_le_mono; apply le_trans with (1 := H); exact (le_div2 n).
+Qed.
+
 (** Properties of [lxor] and others, directly deduced
     from properties of [xorb] and others. *)
 
@@ -810,9 +853,7 @@ Proof. intros a b; rewrite land_even_l, div2_odd'; reflexivity. Qed.
 
 Lemma land_odd_odd :
   forall a b, land (2 * a + 1) (2 * b + 1) == 2 * (land a b) + 1.
-Proof.
-  intros a b; rewrite land_odd_l, div2_odd', odd_succ_double; reflexivity.
-Qed.
+Proof. intros a b; rewrite land_odd_l, div2_odd', odd_odd; reflexivity. Qed.
 
 Lemma land_le_l :
   forall a b, land a b <= a.
@@ -890,9 +931,7 @@ Proof. intros a b; rewrite ldiff_even_l, div2_even; reflexivity. Qed.
 
 Lemma ldiff_odd_even :
   forall a b, ldiff (2 * a + 1) (2 * b) == 2 * (ldiff a b) + 1.
-Proof.
-  intros a b; rewrite ldiff_even_r, div2_odd', odd_succ_double; reflexivity.
-Qed.
+Proof. intros a b; rewrite ldiff_even_r, div2_odd', odd_odd; reflexivity. Qed.
 
 Lemma ldiff_even_odd : forall a b, ldiff (2 * a) (2 * b + 1) == 2 * ldiff a b.
 Proof. intros a b; rewrite ldiff_even_l, div2_odd'; reflexivity. Qed.