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

1 files changed, 22 insertions, 19 deletions

diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v
index 8ee48ba55a..cef8c38198 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.