diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-20 11:53:58 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-20 11:53:58 +0000 |
commit | ddcbe6e926666cdc4bd5cd4a88d637efc338290c (patch) | |
tree | 75ebb40b14683b18bf454eed439deb60ef171d7b /theories | |
parent | c7c3fd68b065bcdee45585b2241c91360223b249 (diff) |
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
Diffstat (limited to 'theories')
-rw-r--r-- | theories/NArith/Ndigits.v | 77 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZBits.v | 92 | ||||
-rw-r--r-- | theories/Numbers/Integer/Binary/ZBinary.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 30 | ||||
-rw-r--r-- | theories/Numbers/NatInt/NZBits.v | 28 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NBits.v | 89 | ||||
-rw-r--r-- | theories/Numbers/Natural/Binary/NBinary.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Natural/Peano/NPeano.v | 59 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 41 | ||||
-rw-r--r-- | theories/ZArith/Zdigits_def.v | 110 |
10 files changed, 287 insertions, 251 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 *) 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. diff --git a/theories/Numbers/NatInt/NZBits.v b/theories/Numbers/NatInt/NZBits.v index a7539bc99..dc97eeb1a 100644 --- a/theories/Numbers/NatInt/NZBits.v +++ b/theories/Numbers/NatInt/NZBits.v @@ -24,26 +24,14 @@ End BitsNotation. Module Type Bits' (A:Typ) := Bits A <+ BitsNotation A. -(** For specifying [testbit], we do not rely on division and modulo, - since such a specification won't be easy to prove for particular - implementations: advanced properties of / and mod won't be - available at that moment. Instead, we decompose the number in - low and high part, with the considered bit in the middle. - - Interestingly, this specification also holds for negative numbers, - (with a positive low part and a negative high part), and this will - correspond to a two's complement representation. - - Moreover, we arbitrary choose false as result of [testbit] at - negative bit indexes (if they exist). -*) - Module Type NZBitsSpec - (Import A : NZOrdAxiomsSig')(Import B : Pow' A)(Import C : Bits' A). + (Import A : NZOrdAxiomsSig')(Import B : Bits' A). - Axiom testbit_spec : forall a n, 0<=n -> - exists l h, 0<=l<2^n /\ - a == l + ((if a.[n] then 1 else 0) + 2*h)*2^n. + Declare Instance testbit_wd : Proper (eq==>eq==>Logic.eq) testbit. + Axiom testbit_odd_0 : forall a, (2*a+1).[0] = true. + Axiom testbit_even_0 : forall a, (2*a).[0] = false. + Axiom testbit_odd_succ : forall a n, 0<=n -> (2*a+1).[S n] = a.[n]. + Axiom testbit_even_succ : forall a n, 0<=n -> (2*a).[S n] = a.[n]. Axiom testbit_neg_r : forall a n, n<0 -> a.[n] = false. Axiom shiftr_spec : forall a n m, 0<=m -> (a >> n).[m] = a.[m+n]. @@ -58,8 +46,8 @@ Module Type NZBitsSpec End NZBitsSpec. -Module Type NZBits (A:NZOrdAxiomsSig)(B:Pow A) := Bits A <+ NZBitsSpec A B. -Module Type NZBits' (A:NZOrdAxiomsSig)(B:Pow A) := Bits' A <+ NZBitsSpec A B. +Module Type NZBits (A:NZOrdAxiomsSig) := Bits A <+ NZBitsSpec A. +Module Type NZBits' (A:NZOrdAxiomsSig) := Bits' A <+ NZBitsSpec A. (** In the functor of properties will also be defined: - [setbit : t -> t -> t ] defined as [lor a (1<<n)]. 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. diff --git a/theories/ZArith/Zdigits_def.v b/theories/ZArith/Zdigits_def.v index 618214357..4e8e9fd93 100644 --- a/theories/ZArith/Zdigits_def.v +++ b/theories/ZArith/Zdigits_def.v @@ -96,74 +96,6 @@ Definition Zxor a b := | Zneg a, Zneg b => Z_of_N (Nxor (Ppred_N a) (Ppred_N b)) end. -(** Proofs of specifications *) - -Lemma Zdiv2_spec : forall a, Zdiv2 a = Zshiftr a 1. -Proof. - reflexivity. -Qed. - -Lemma Ztestbit_neg_r : forall a n, n<0 -> Ztestbit a n = false. -Proof. - now destruct n. -Qed. - -Lemma Ztestbit_spec : forall a n, 0<=n -> - exists l h, 0<=l<2^n /\ - a = l + ((if Ztestbit a n then 1 else 0) + 2*h)*2^n. -Proof. - intros a [ |n|n] Hn; (now destruct Hn) || clear Hn. - (* n = 0 *) - simpl Ztestbit. - exists 0. exists (Zdiv2 a). repeat split. easy. - now rewrite Zplus_0_l, Zmult_1_r, Zplus_comm, <- Zdiv2_odd_eqn. - (* n > 0 *) - destruct a. - (* ... a = 0 *) - exists 0. exists 0. repeat split; try easy. now rewrite Zpower_Ppow. - (* ... a > 0 *) - simpl Ztestbit. - destruct (Ntestbit_spec (Npos p) (Npos n)) as (l & h & (_,Hl) & EQ). - exists (Z_of_N l). exists (Z_of_N h). - simpl Npow in *; simpl Ntestbit in *. rewrite Zpower_Ppow. - repeat split. - apply Z_of_N_le_0. - rewrite <-Z_of_N_pos. now apply Z_of_N_lt. - rewrite <-Z_of_N_pos, EQ. - rewrite Z_of_N_plus, Z_of_N_mult. f_equal. f_equal. - destruct Ptestbit; now rewrite Z_of_N_plus, Z_of_N_mult. - (* ... a < 0 *) - simpl Ztestbit. - destruct (Ntestbit_spec (Ppred_N p) (Npos n)) as (l & h & (_,Hl) & EQ). - exists (2^Zpos n - (Z_of_N l) - 1). exists (-Z_of_N h - 1). - simpl Npow in *. rewrite Zpower_Ppow. - repeat split. - apply Zle_minus_le_0. - change 1 with (Zsucc 0). apply Zle_succ_l. - apply Zlt_plus_swap. simpl. rewrite <-Z_of_N_pos. now apply Z_of_N_lt. - apply Zlt_plus_swap. unfold Zminus. rewrite Zopp_involutive. - fold (Zsucc (Zpos (2^n))). apply Zlt_succ_r. - apply Zle_plus_swap. unfold Zminus. rewrite Zopp_involutive. - rewrite <- (Zplus_0_r (Zpos (2^n))) at 1. apply Zplus_le_compat_l. - apply Z_of_N_le_0. - apply Zopp_inj. unfold Zminus. - rewrite Zopp_neg, !Zopp_plus_distr, !Zopp_involutive. - rewrite Zopp_mult_distr_l, Zopp_plus_distr, Zopp_mult_distr_r, - Zopp_plus_distr, !Zopp_involutive. - rewrite Ppred_N_spec in EQ at 1. - apply (f_equal Nsucc) in EQ. rewrite Nsucc_pred in EQ by easy. - rewrite <-Z_of_N_pos, EQ. - rewrite Z_of_N_succ, Z_of_N_plus, Z_of_N_mult, Z_of_N_pos. unfold Zsucc. - rewrite <- (Zplus_assoc _ 1), (Zplus_comm 1), Zplus_assoc. f_equal. - rewrite (Zplus_comm (- _)), <- Zplus_assoc. f_equal. - change (- Zpos (2^n)) with ((-1)*(Zpos (2^n))). rewrite <- Zmult_plus_distr_l. - f_equal. - rewrite Z_of_N_plus, Z_of_N_mult. - rewrite Zmult_plus_distr_r, Zmult_1_r, (Zplus_comm _ 2), !Zplus_assoc. - rewrite (Zplus_comm _ 2), Zplus_assoc. change (2+-1) with 1. - f_equal. - now destruct Ntestbit. -Qed. (** Conversions between [Ztestbit] and [Ntestbit] *) @@ -198,11 +130,53 @@ Proof. now rewrite Zodd_bool_pred, <- Zodd_even_bool. Qed. +(** Proofs of specifications *) + +Lemma Zdiv2_spec : forall a, Zdiv2 a = Zshiftr a 1. +Proof. + reflexivity. +Qed. + Lemma Ztestbit_0_l : forall n, Ztestbit 0 n = false. Proof. now destruct n. Qed. +Lemma Ztestbit_neg_r : forall a n, n<0 -> Ztestbit a n = false. +Proof. + now destruct n. +Qed. + +Lemma Ztestbit_odd_0 a : Ztestbit (2*a+1) 0 = true. +Proof. + now destruct a as [|a|[a|a|]]. +Qed. + +Lemma Ztestbit_even_0 a : Ztestbit (2*a) 0 = false. +Proof. + now destruct a. +Qed. + +Lemma Ztestbit_odd_succ a n : 0<=n -> + Ztestbit (2*a+1) (Zsucc n) = Ztestbit a n. +Proof. + destruct n as [|n|n]; (now destruct 1) || intros _. + destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a. + unfold Ztestbit. rewrite <- Zpos_succ_morphism. + destruct a as [|a|[a|a|]]; simpl; trivial; + rewrite ?Ppred_succ; now destruct n. +Qed. + +Lemma Ztestbit_even_succ a n : 0<=n -> + Ztestbit (2*a) (Zsucc n) = Ztestbit a n. +Proof. + destruct n as [|n|n]; (now destruct 1) || intros _. + destruct a as [|[a|a|]|[a|a|]]; simpl; trivial. now destruct a. + unfold Ztestbit. rewrite <- Zpos_succ_morphism. + destruct a as [|a|[a|a|]]; simpl; trivial; + rewrite ?Ppred_succ; now destruct n. +Qed. + Lemma Ppred_div2_up : forall p, Ppred_N (Pdiv2_up p) = Ndiv2 (Ppred_N p). Proof. |