diff options
author | 2011-06-28 23:30:32 +0000 | |
---|---|---|
committer | 2011-06-28 23:30:32 +0000 | |
commit | e97cd3c0cab1eb022b15d65bb33483055ce4cc28 (patch) | |
tree | e1fb56c8f3d5d83f68d55e6abdbb3486d137f9e2 /theories/Numbers/Natural/BigN | |
parent | 00353bc0b970605ae092af594417a51a0cdf903f (diff) |
Deletion of useless Zdigits_def
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14247 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Numbers/Natural/BigN')
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 26 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 13 |
2 files changed, 26 insertions, 13 deletions
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 64b8ec844..a6eb6ae47 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -1330,7 +1330,7 @@ Module Make (W0:CyclicType) <: NType. generalize (ZnZ.spec_to_Z d); auto with zarith. Qed. - Lemma spec_shiftr: forall x p, [shiftr x p] = Zshiftr [x] [p]. + Lemma spec_shiftr: forall x p, [shiftr x p] = Z.shiftr [x] [p]. Proof. intros. now rewrite spec_shiftr_pow2, Z.shiftr_div_pow2 by apply spec_pos. @@ -1603,7 +1603,7 @@ Module Make (W0:CyclicType) <: NType. apply Zpower_le_monotone2; auto with zarith. Qed. - Lemma spec_shiftl: forall x p, [shiftl x p] = Zshiftl [x] [p]. + Lemma spec_shiftl: forall x p, [shiftl x p] = Z.shiftl [x] [p]. Proof. intros. now rewrite spec_shiftl_pow2, Z.shiftl_mul_pow2 by apply spec_pos. @@ -1613,7 +1613,7 @@ Module Make (W0:CyclicType) <: NType. Definition testbit x n := odd (shiftr x n). - Lemma spec_testbit: forall x p, testbit x p = Ztestbit [x] [p]. + Lemma spec_testbit: forall x p, testbit x p = Z.testbit [x] [p]. Proof. intros. unfold testbit. symmetry. rewrite spec_odd, spec_shiftr. apply Z.testbit_odd. @@ -1621,42 +1621,42 @@ Module Make (W0:CyclicType) <: NType. Definition div2 x := shiftr x one. - Lemma spec_div2: forall x, [div2 x] = Zdiv2 [x]. + Lemma spec_div2: forall x, [div2 x] = Z.div2 [x]. Proof. intros. unfold div2. symmetry. - rewrite spec_shiftr, spec_1. apply Zdiv2_spec. + rewrite spec_shiftr, spec_1. apply Z.div2_spec. Qed. (** TODO : provide efficient versions instead of just converting from/to N (see with Laurent) *) - Definition lor x y := of_N (Nor (to_N x) (to_N y)). - Definition land x y := of_N (Nand (to_N x) (to_N y)). - Definition ldiff x y := of_N (Ndiff (to_N x) (to_N y)). - Definition lxor x y := of_N (Nxor (to_N x) (to_N y)). + Definition lor x y := of_N (N.lor (to_N x) (to_N y)). + Definition land x y := of_N (N.land (to_N x) (to_N y)). + Definition ldiff x y := of_N (N.ldiff (to_N x) (to_N y)). + Definition lxor x y := of_N (N.lxor (to_N x) (to_N y)). - Lemma spec_land: forall x y, [land x y] = Zand [x] [y]. + Lemma spec_land: forall x y, [land x y] = Z.land [x] [y]. Proof. intros x y. unfold land. rewrite spec_of_N. unfold to_N. generalize (spec_pos x), (spec_pos y). destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). Qed. - Lemma spec_lor: forall x y, [lor x y] = Zor [x] [y]. + Lemma spec_lor: forall x y, [lor x y] = Z.lor [x] [y]. Proof. intros x y. unfold lor. rewrite spec_of_N. unfold to_N. generalize (spec_pos x), (spec_pos y). destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). Qed. - Lemma spec_ldiff: forall x y, [ldiff x y] = Zdiff [x] [y]. + Lemma spec_ldiff: forall x y, [ldiff x y] = Z.ldiff [x] [y]. Proof. intros x y. unfold ldiff. rewrite spec_of_N. unfold to_N. generalize (spec_pos x), (spec_pos y). destruct [x], [y]; trivial; (now destruct 1) || (now destruct 2). Qed. - Lemma spec_lxor: forall x y, [lxor x y] = Zxor [x] [y]. + Lemma spec_lxor: forall x y, [lxor x y] = Z.lxor [x] [y]. Proof. intros x y. unfold lxor. rewrite spec_of_N. unfold to_N. generalize (spec_pos x), (spec_pos y). diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index 94f6b32fd..dec8f1fe4 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -23,6 +23,19 @@ Implicit Arguments mk_zn2z_specs_karatsuba [t ops]. Implicit Arguments ZnZ.digits [t]. Implicit Arguments ZnZ.zdigits [t]. +Lemma Pshiftl_nat_Zpower : forall n p, + Zpos (Pos.shiftl_nat p n) = Zpos p * 2 ^ Z.of_nat n. +Proof. + intros. + rewrite Z.mul_comm. + induction n. simpl; auto. + transitivity (2 * (2 ^ Z.of_nat n * Zpos p)). + rewrite <- IHn. auto. + rewrite Z.mul_assoc. + rewrite inj_S. + rewrite <- Z.pow_succ_r; auto with zarith. +Qed. + (* To compute the necessary height *) Fixpoint plength (p: positive) : positive := |