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, 24 insertions, 53 deletions

diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v
index 0c660a44e..1f95b1cf7 100644
--- a/theories/NArith/Ndigits.v
+++ b/theories/NArith/Ndigits.v
@@ -192,59 +192,30 @@ 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 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.
+(** Correctness proofs for [Ntestbit]. *)
+
+Lemma Ntestbit_odd_0 a : Ntestbit (2*a+1) 0 = true.
+Proof.
+ now destruct a.
+Qed.
+
+Lemma Ntestbit_even_0 a : Ntestbit (2*a) 0 = false.
+Proof.
+ now destruct a.
+Qed.
+
+Lemma Ntestbit_odd_succ a n :
+ Ntestbit (2*a+1) (Nsucc n) = Ntestbit a n.
+Proof.
+ destruct a. simpl. now destruct n.
+ simpl. rewrite Npred_succ. now destruct n.
+Qed.
+
+Lemma Ntestbit_even_succ a n :
+ Ntestbit (2*a) (Nsucc n) = Ntestbit a n.
+Proof.
+ destruct a. trivial.
+ simpl. rewrite Npred_succ. now destruct n.
 Qed.
 
 (** Equivalence of shifts, N and nat versions *)