Numbers: simplier spec for testbit

 We now specify testbit by some initial and recursive equations.
 The previous spec (via a complex split of the number in
 low and high parts) is now a derived property in {N,Z}Bits.v
 This way, proofs of implementations are quite simplier.
 Note that these new specs doesn't imply anymore that testbit is a
 morphism, we have to add this as a extra spec (but this lead
 to trivial proofs when implementing).

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

4 files changed, 119 insertions, 76 deletions

diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v
index f5b900532..ce720c38c 100644
--- a/theories/Numbers/Natural/Abstract/NBits.v
+++ b/theories/Numbers/Natural/Abstract/NBits.v
@@ -48,17 +48,67 @@ Qed.
 Definition b2n (b:bool) := if b then 1 else 0.
 Local Coercion b2n : bool >-> t.
 
+Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b.
+Proof.
+ elim (Even_or_Odd a); [intros (a',H)| intros (a',H)].
+ exists a'. exists false. now nzsimpl.
+ exists a'. exists true. now simpl.
+Qed.
+
+(** We can compact [testbit_odd_0] [testbit_even_0]
+    [testbit_even_succ] [testbit_odd_succ] in only two lemmas. *)
+
+Lemma testbit_0_r a (b:bool) : testbit (2*a+b) 0 = b.
+Proof.
+ destruct b; simpl; rewrite ?add_0_r.
+ apply testbit_odd_0.
+ apply testbit_even_0.
+Qed.
+
+Lemma testbit_succ_r a (b:bool) n :
+ testbit (2*a+b) (succ n) = testbit a n.
+Proof.
+ destruct b; simpl; rewrite ?add_0_r.
+ apply testbit_odd_succ, le_0_l.
+ apply testbit_even_succ, le_0_l.
+Qed.
+
 (** Alternative caracterisations of [testbit] *)
 
-Lemma testbit_spec' : forall a n, a.[n] == (a / 2^n) mod 2.
+(** This concise equation could have been taken as specification
+   for testbit in the interface, but it would have been hard to
+   implement with little initial knowledge about div and mod *)
+
+Lemma testbit_spec' a n : a.[n] == (a / 2^n) mod 2.
 Proof.
- intros a n.
- destruct (testbit_spec a n) as (l & h & (_,H) & EQ).
- apply le_0_l.
- fold (b2n a.[n]) in EQ.
- apply mod_unique with h. destruct a.[n]; order'.
- symmetry. apply div_unique with l; trivial.
- now rewrite add_comm, mul_comm, (add_comm (2*h)).
+ revert a. induct n.
+ intros a. nzsimpl.
+ destruct (exists_div2 a) as (a' & b & H). rewrite H at 1.
+ rewrite testbit_0_r. apply mod_unique with a'; trivial.
+ destruct b; order'.
+ intros n IH a.
+ destruct (exists_div2 a) as (a' & b & H). rewrite H at 1.
+ rewrite testbit_succ_r, IH. f_equiv.
+ rewrite pow_succ_r', <- div_div by order_nz. f_equiv.
+ apply div_unique with b; trivial.
+ destruct b; order'.
+Qed.
+
+(** This caracterisation that uses only basic operations and
+   power was initially taken as specification for testbit.
+   We describe [a] as having a low part and a high part, with
+   the corresponding bit in the middle. This caracterisation
+   is moderatly complex to implement, but also moderately
+   usable... *)
+
+Lemma testbit_spec a n :
+  exists l h, 0<=l<2^n /\ a == l + (a.[n] + 2*h)*2^n.
+Proof.
+ exists (a mod 2^n). exists (a / 2^n / 2). split.
+ split; [apply le_0_l | apply mod_upper_bound; order_nz].
+ rewrite add_comm, mul_comm, (add_comm a.[n]).
+ rewrite (div_mod a (2^n)) at 1 by order_nz. do 2 f_equiv.
+ rewrite testbit_spec'. apply div_mod. order'.
 Qed.
 
 Lemma testbit_true : forall a n,
@@ -82,13 +132,6 @@ Proof.
  apply eq_true_iff_eq. now rewrite testbit_true, eqb_eq.
 Qed.
 
-(** testbit is hence a morphism *)
-
-Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
-Proof.
- intros a a' Ha n n' Hn. now rewrite 2 testbit_eqb, Ha, Hn.
-Qed.
-
 (** Results about the injection [b2n] *)
 
 Lemma b2n_inj : forall (a0 b0:bool), a0 == b0 -> a0 = b0.
@@ -119,7 +162,7 @@ Proof.
  intros a0. rewrite <- (add_b2n_double_bit0 a0 0) at 2. now nzsimpl.
 Qed.
 
-(** The initial specification of testbit is complete *)
+(** The specification of testbit by low and high parts is complete *)
 
 Lemma testbit_unique : forall a n (a0:bool) l h,
  l<2^n -> a == l + (a0 + 2*h)*2^n -> a.[n] = a0.
@@ -140,9 +183,12 @@ Qed.
 
 (** Various ways to refer to the lowest bit of a number *)
 
-Lemma bit0_mod : forall a, a.[0] == a mod 2.
+Lemma bit0_odd : forall a, a.[0] = odd a.
 Proof.
- intros a. rewrite testbit_spec'. now nzsimpl.
+ intros. symmetry.
+ destruct (exists_div2 a) as (a' & b & EQ).
+ rewrite EQ, testbit_0_r, add_comm, odd_add_mul_2.
+ destruct b; simpl; apply odd_1 || apply odd_0.
 Qed.
 
 Lemma bit0_eqb : forall a, a.[0] = eqb (a mod 2) 1.
@@ -150,12 +196,9 @@ Proof.
  intros a. rewrite testbit_eqb. now nzsimpl.
 Qed.
 
-Lemma bit0_odd : forall a, a.[0] = odd a.
+Lemma bit0_mod : forall a, a.[0] == a mod 2.
 Proof.
- intros. rewrite bit0_eqb.
- apply eq_true_iff_eq. rewrite eqb_eq, odd_spec. split.
- intros H. exists (a/2). rewrite <- H. apply div_mod. order'.
- intros (b,H). rewrite H, add_comm, mul_comm, mod_add, mod_small; order'.
+ intros a. rewrite testbit_spec'. now nzsimpl.
 Qed.
 
 (** Hence testing a bit is equivalent to shifting and testing parity *)
diff --git a/theories/Numbers/Natural/Binary/NBinary.v b/theories/Numbers/Natural/Binary/NBinary.v
index 82380e9b4..bd59ef494 100644
--- a/theories/Numbers/Natural/Binary/NBinary.v
+++ b/theories/Numbers/Natural/Binary/NBinary.v
@@ -180,7 +180,11 @@ Proof. intros. now destruct (Ngcd a b). Qed.
 
 (** Bitwise Operations *)
 
-Definition testbit_spec a n (_:0<=n) := Ntestbit_spec a n.
+Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) Ntestbit.
+Definition testbit_odd_0 := Ntestbit_odd_0.
+Definition testbit_even_0 := Ntestbit_even_0.
+Definition testbit_odd_succ a n (_:0<=n) := Ntestbit_odd_succ a n.
+Definition testbit_even_succ a n (_:0<=n) := Ntestbit_even_succ a n.
 Lemma testbit_neg_r a n (H:n<0) : Ntestbit a n = false.
 Proof. now destruct n. Qed.
 Definition shiftl_spec_low := Nshiftl_spec_low.
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 98809fbf8..0cf9ae441 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -403,38 +403,27 @@ Proof.
  now induction n.
 Qed.
 
-Lemma testbit_spec : forall a n,
- exists l h, 0<=l<2^n /\
-  a = l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
-Proof.
- intros a n. revert a. induction n; intros a; simpl testbit.
- exists 0. exists (div2 a).
- split. simpl.  unfold lt. now split.
- case_eq (odd a); intros EQ; simpl.
- rewrite mult_1_r, <- plus_n_O.
-  now apply odd_double, Odd_equiv, odd_spec.
- rewrite mult_1_r, <- plus_n_O. apply even_double.
-  destruct (Even.even_or_odd a) as [H|H]; trivial.
-  apply Odd_equiv, odd_spec in H. rewrite H in EQ; discriminate.
- destruct (IHn (div2 a)) as (l & h & (_,H) & EQ).
- destruct (Even.even_or_odd a) as [EV|OD].
- exists (double l). exists h.
- split. split. apply le_O_n.
- unfold double; simpl. rewrite <- plus_n_O. now apply plus_lt_compat.
- pattern a at 1. rewrite (even_double a EV).
- pattern (div2 a) at 1. rewrite EQ.
- rewrite !double_twice, mult_plus_distr_l. f_equal.
- rewrite mult_assoc, (mult_comm 2), <- mult_assoc. f_equal.
- exists (S (double l)). exists h.
- split. split. apply le_O_n.
- red. red in H.
- unfold double; simpl. rewrite <- plus_n_O, plus_n_Sm, <- plus_Sn_m.
- now apply plus_le_compat.
- rewrite plus_Sn_m.
- pattern a at 1. rewrite (odd_double a OD). f_equal.
- pattern (div2 a) at 1. rewrite EQ.
- rewrite !double_twice, mult_plus_distr_l. f_equal.
- rewrite mult_assoc, (mult_comm 2), <- mult_assoc. f_equal.
+Lemma testbit_odd_0 a : testbit (2*a+1) 0 = true.
+Proof.
+ unfold testbit. rewrite odd_spec. now exists a.
+Qed.
+
+Lemma testbit_even_0 a : testbit (2*a) 0 = false.
+Proof.
+ unfold testbit, odd. rewrite (proj2 (even_spec _)); trivial.
+ now exists a.
+Qed.
+
+Lemma testbit_odd_succ a n : testbit (2*a+1) (S n) = testbit a n.
+Proof.
+ unfold testbit; fold testbit.
+ rewrite <- plus_n_Sm, <- plus_n_O. f_equal.
+ apply div2_double_plus_one.
+Qed.
+
+Lemma testbit_even_succ a n : testbit (2*a) (S n) = testbit a n.
+Proof.
+ unfold testbit; fold testbit. f_equal. apply div2_double.
 Qed.
 
 Lemma shiftr_spec : forall a n m,
@@ -749,7 +738,11 @@ Definition lor := lor.
 Definition ldiff := ldiff.
 Definition div2 := div2.
 
-Definition testbit_spec a n (_:0<=n) := testbit_spec a n.
+Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
+Definition testbit_odd_0 := testbit_odd_0.
+Definition testbit_even_0 := testbit_even_0.
+Definition testbit_odd_succ a n (_:0<=n) := testbit_odd_succ a n.
+Definition testbit_even_succ a n (_:0<=n) := testbit_even_succ a n.
 Lemma testbit_neg_r a n (H:n<0) : testbit a n = false.
 Proof. inversion H. Qed.
 Definition shiftl_spec_low := shiftl_spec_low.
diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 8ee48ba55..cef8c3819 100644
--- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
+++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
@@ -337,25 +337,28 @@ Qed.
 
 (** Bitwise operations *)
 
-Lemma testbit_spec : forall a n, 0<=n ->
-  exists l h, (0<=l /\ l<2^n) /\
-    a == l + ((if testbit a n then 1 else 0) + 2*h)*2^n.
-Proof.
- intros a n _. zify.
- assert (Ha := spec_pos a).
- assert (Hn := spec_pos n).
- destruct (Ntestbit_spec (Zabs_N [a]) (Zabs_N [n])) as (l & h & (_,Hl) & EQ).
- exists (of_N l), (of_N h).
- zify.
- apply Z_of_N_lt in Hl.
- apply Z_of_N_eq in EQ.
- revert Hl EQ.
- rewrite <- Ztestbit_of_N.
- rewrite Z_of_N_plus, Z_of_N_mult, <- !Zpower_Npow, Z_of_N_plus,
-  Z_of_N_mult, !Z_of_N_abs, !Zabs_eq by trivial.
- simpl (Z_of_N 2).
- repeat split; trivial using Z_of_N_le_0.
- destruct Ztestbit; now zify.
+Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit.
+
+Lemma testbit_odd_0 : forall a, testbit (2*a+1) 0 = true.
+Proof.
+ intros. zify. apply Ztestbit_odd_0.
+Qed.
+
+Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false.
+Proof.
+ intros. zify. apply Ztestbit_even_0.
+Qed.
+
+Lemma testbit_odd_succ : forall a n, 0<=n ->
+ testbit (2*a+1) (succ n) = testbit a n.
+Proof.
+ intros a n. zify. apply Ztestbit_odd_succ.
+Qed.
+
+Lemma testbit_even_succ : forall a n, 0<=n ->
+ testbit (2*a) (succ n) = testbit a n.
+Proof.
+ intros a n. zify. apply Ztestbit_even_succ.
 Qed.
 
 Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false.