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

3 files changed, 94 insertions, 34 deletions

diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v
index de6619598..bf03cf020 100644
--- a/theories/Numbers/Integer/Abstract/ZBits.v
+++ b/theories/Numbers/Integer/Abstract/ZBits.v
@@ -51,15 +51,68 @@ Qed.
 Definition b2z (b:bool) := if b then 1 else 0.
 Local Coercion b2z : 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 : 0<=n ->
+ testbit (2*a+b) (succ n) = testbit a n.
+Proof.
+ destruct b; simpl; rewrite ?add_0_r.
+ now apply testbit_odd_succ.
+ now apply testbit_even_succ.
+Qed.
+
 (** Alternative caracterisations of [testbit] *)
 
-Lemma testbit_spec' : forall a n, 0<=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 : 0<=n -> a.[n] == (a / 2^n) mod 2.
 Proof.
- intros a n Hn.
- destruct (testbit_spec a n Hn) as (l & h & H & EQ). fold (b2z a.[n]) in EQ.
- apply mod_unique with h. left. destruct a.[n]; split; simpl; order'.
- symmetry. apply div_unique with l. now left.
- now rewrite add_comm, mul_comm, (add_comm (2*h)).
+ intro Hn. revert a. apply le_ind with (4:=Hn).
+ solve_proper.
+ 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.
+ left. destruct b; split; simpl; order'.
+ clear n Hn. intros n Hn IH a.
+ destruct (exists_div2 a) as (a' & b & H). rewrite H at 1.
+ rewrite testbit_succ_r, IH by trivial. f_equiv.
+ rewrite pow_succ_r, <- div_div by order_pos. f_equiv.
+ apply div_unique with b; trivial.
+ left. destruct b; split; simpl; 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 : 0<=n ->
+  exists l h, 0<=l<2^n /\ a == l + (a.[n] + 2*h)*2^n.
+Proof.
+ intro Hn. exists (a mod 2^n). exists (a / 2^n / 2). split.
+ apply mod_pos_bound; order_pos.
+ 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' by trivial. apply div_mod. order'.
 Qed.
 
 Lemma testbit_true : forall a n, 0<=n ->
@@ -85,16 +138,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.
- destruct (le_gt_cases 0 n), (le_gt_cases 0 n'); try order.
- now rewrite 2 testbit_eqb, Ha, Hn by trivial.
- now rewrite 2 testbit_neg_r by trivial.
-Qed.
-
 (** Results about the injection [b2z] *)
 
 Lemma b2z_inj : forall (a0 b0:bool), a0 == b0 -> a0 = b0.
@@ -126,7 +169,7 @@ Proof.
  intros a0. rewrite <- (add_b2z_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,
  0<=l<2^n -> a == l + (a0 + 2*h)*2^n -> a.[n] = a0.
@@ -195,9 +238,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' by order. 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.
@@ -205,13 +251,9 @@ Proof.
  intros a. rewrite testbit_eqb by order. 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 by order.
- 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; try split; order'.
+ intros a. rewrite testbit_spec' by order. now nzsimpl.
 Qed.
 
 (** Hence testing a bit is equivalent to shifting and testing parity *)
diff --git a/theories/Numbers/Integer/Binary/ZBinary.v b/theories/Numbers/Integer/Binary/ZBinary.v
index cad5152d7..366418035 100644
--- a/theories/Numbers/Integer/Binary/ZBinary.v
+++ b/theories/Numbers/Integer/Binary/ZBinary.v
@@ -193,7 +193,11 @@ Definition rem := Zrem.
 
 (** Bitwise operations *)
 
-Definition testbit_spec := Ztestbit_spec.
+Program Instance testbit_wd : Proper (eq==>eq==>Logic.eq) Ztestbit.
+Definition testbit_odd_0 := Ztestbit_odd_0.
+Definition testbit_even_0 := Ztestbit_even_0.
+Definition testbit_odd_succ := Ztestbit_odd_succ.
+Definition testbit_even_succ := Ztestbit_even_succ.
 Definition testbit_neg_r := Ztestbit_neg_r.
 Definition shiftr_spec := Zshiftr_spec.
 Definition shiftl_spec_low := Zshiftl_spec_low.
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
index 2c46be4c7..cf38adf3a 100644
--- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
+++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v
@@ -411,14 +411,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. intros H.
- destruct (Ztestbit_spec [a] [n] H) as (l & h & Hl & EQ).
- exists (of_Z l), (of_Z h).
- destruct Ztestbit; zify; now split.
+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.