diff options
Diffstat (limited to 'theories/Numbers')
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v | 4 | ||||
-rw-r--r-- | theories/Numbers/Integer/Abstract/ZBits.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Natural/Abstract/NBits.v | 3 | ||||
-rw-r--r-- | theories/Numbers/Rational/BigQ/QMake.v | 1 |
4 files changed, 10 insertions, 4 deletions
diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v index c30d38186..00a840520 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleCyclic.v @@ -285,7 +285,7 @@ Section Z_2nZ. (* ** Record of operators on 2 words *) - Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) := + Global Instance mk_zn2z_ops : ZnZ.Ops (zn2z t) | 1 := ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 @@ -305,7 +305,7 @@ Section Z_2nZ. sqrt2 sqrt. - Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) := + Global Instance mk_zn2z_ops_karatsuba : ZnZ.Ops (zn2z t) | 2 := ZnZ.MkOps _ww_digits _ww_zdigits to_Z ww_of_pos head0 tail0 W0 ww_1 ww_Bm1 diff --git a/theories/Numbers/Integer/Abstract/ZBits.v b/theories/Numbers/Integer/Abstract/ZBits.v index 39e9f02c5..92afbcb53 100644 --- a/theories/Numbers/Integer/Abstract/ZBits.v +++ b/theories/Numbers/Integer/Abstract/ZBits.v @@ -51,6 +51,8 @@ Qed. Definition b2z (b:bool) := if b then 1 else 0. Local Coercion b2z : bool >-> t. +Instance b2z_wd : Proper (Logic.eq ==> eq) b2z := _. + Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b. Proof. elim (Even_or_Odd a); [intros (a',H)| intros (a',H)]. @@ -84,8 +86,8 @@ Qed. Lemma testbit_spec' a n : 0<=n -> a.[n] == (a / 2^n) mod 2. Proof. - intro Hn. revert a. apply le_ind with (4:=Hn). - solve_proper. + 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. diff --git a/theories/Numbers/Natural/Abstract/NBits.v b/theories/Numbers/Natural/Abstract/NBits.v index ce720c38c..c66f003ec 100644 --- a/theories/Numbers/Natural/Abstract/NBits.v +++ b/theories/Numbers/Natural/Abstract/NBits.v @@ -48,6 +48,9 @@ Qed. Definition b2n (b:bool) := if b then 1 else 0. Local Coercion b2n : bool >-> t. +Instance b2n_proper : Proper (Logic.eq ==> eq) b2n. +Proof. solve_proper. Qed. + Lemma exists_div2 a : exists a' (b:bool), a == 2*a' + b. Proof. elim (Even_or_Odd a); [intros (a',H)| intros (a',H)]. diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v index 33267a518..995fbb9ee 100644 --- a/theories/Numbers/Rational/BigQ/QMake.v +++ b/theories/Numbers/Rational/BigQ/QMake.v @@ -94,6 +94,7 @@ Module Make (N:NType)(Z:ZType)(Import NZ:NType_ZType N Z) <: QType. Z.spec_gcd N.spec_gcd Zgcd_Zabs Zgcd_1 spec_Z_of_N spec_Zabs_N : nz. + Ltac nzsimpl := autorewrite with nz in *. Ltac qsimpl := try red; unfold to_Q; simpl; intros; |