diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-28 23:30:32 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-06-28 23:30:32 +0000 |
commit | e97cd3c0cab1eb022b15d65bb33483055ce4cc28 (patch) | |
tree | e1fb56c8f3d5d83f68d55e6abdbb3486d137f9e2 /theories/Numbers | |
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')
-rw-r--r-- | theories/Numbers/Integer/BigZ/ZMake.v | 20 | ||||
-rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v | 26 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 26 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 13 | ||||
-rw-r--r-- | theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v | 66 |
5 files changed, 82 insertions, 69 deletions
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index cb16e1291..0142b36be 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -678,17 +678,17 @@ Module Make (N:NType) <: ZType. destruct (norm_pos x) as [x'|x']; specialize (H x' (eq_refl _)) || clear H. - Lemma spec_testbit: forall x p, testbit x p = Ztestbit (to_Z x) (to_Z p). + Lemma spec_testbit: forall x p, testbit x p = Z.testbit (to_Z x) (to_Z p). Proof. intros x p. unfold testbit. destr_norm_pos p; simpl. destr_norm_pos x; simpl. apply N.spec_testbit. rewrite N.spec_testbit, N.spec_pred, Zmax_r by auto with zarith. symmetry. apply Z.bits_opp. apply N.spec_pos. - symmetry. apply Ztestbit_neg_r; auto with zarith. + symmetry. apply Z.testbit_neg_r; auto with zarith. Qed. - Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Zshiftl (to_Z x) (to_Z p). + Lemma spec_shiftl: forall x p, to_Z (shiftl x p) = Z.shiftl (to_Z x) (to_Z p). Proof. intros x p. unfold shiftl. destr_norm_pos x; destruct p as [p|p]; simpl; @@ -703,13 +703,13 @@ Module Make (N:NType) <: ZType. now rewrite Zlnot_alt1, Z.lnot_shiftr, Zlnot_alt2. Qed. - Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Zshiftr (to_Z x) (to_Z p). + Lemma spec_shiftr: forall x p, to_Z (shiftr x p) = Z.shiftr (to_Z x) (to_Z p). Proof. intros. unfold shiftr. rewrite spec_shiftl, spec_opp. apply Z.shiftl_opp_r. Qed. - Lemma spec_land: forall x y, to_Z (land x y) = Zand (to_Z x) (to_Z y). + Lemma spec_land: forall x y, to_Z (land x y) = Z.land (to_Z x) (to_Z y). Proof. intros x y. unfold land. destr_norm_pos x; destr_norm_pos y; simpl; @@ -720,7 +720,7 @@ Module Make (N:NType) <: ZType. now rewrite Z.lnot_lor, !Zlnot_alt2. Qed. - Lemma spec_lor: forall x y, to_Z (lor x y) = Zor (to_Z x) (to_Z y). + Lemma spec_lor: forall x y, to_Z (lor x y) = Z.lor (to_Z x) (to_Z y). Proof. intros x y. unfold lor. destr_norm_pos x; destr_norm_pos y; simpl; @@ -731,7 +731,7 @@ Module Make (N:NType) <: ZType. now rewrite Z.lnot_land, !Zlnot_alt2. Qed. - Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Zdiff (to_Z x) (to_Z y). + Lemma spec_ldiff: forall x y, to_Z (ldiff x y) = Z.ldiff (to_Z x) (to_Z y). Proof. intros x y. unfold ldiff. destr_norm_pos x; destr_norm_pos y; simpl; @@ -742,7 +742,7 @@ Module Make (N:NType) <: ZType. now rewrite 2 Z.ldiff_land, Zlnot_alt2, Z.land_comm, Zlnot_alt3. Qed. - Lemma spec_lxor: forall x y, to_Z (lxor x y) = Zxor (to_Z x) (to_Z y). + Lemma spec_lxor: forall x y, to_Z (lxor x y) = Z.lxor (to_Z x) (to_Z y). Proof. intros x y. unfold lxor. destr_norm_pos x; destr_norm_pos y; simpl; @@ -753,9 +753,9 @@ Module Make (N:NType) <: ZType. now rewrite <- Z.lxor_lnot_lnot, !Zlnot_alt2. Qed. - Lemma spec_div2: forall x, to_Z (div2 x) = Zdiv2 (to_Z x). + Lemma spec_div2: forall x, to_Z (div2 x) = Z.div2 (to_Z x). Proof. - intros x. unfold div2. now rewrite spec_shiftr, Zdiv2_spec, spec_1. + intros x. unfold div2. now rewrite spec_shiftr, Z.div2_spec, spec_1. Qed. End Make. diff --git a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v index f40928566..eaab13c2a 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSigZAxioms.v @@ -445,77 +445,77 @@ 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. + intros. zify. apply Z.testbit_odd_0. Qed. Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false. Proof. - intros. zify. apply Ztestbit_even_0. + intros. zify. apply Z.testbit_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. + intros a n. zify. apply Z.testbit_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. + intros a n. zify. apply Z.testbit_even_succ. Qed. Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false. Proof. - intros a n. zify. apply Ztestbit_neg_r. + intros a n. zify. apply Z.testbit_neg_r. Qed. Lemma shiftr_spec : forall a n m, 0<=m -> testbit (shiftr a n) m = testbit a (m+n). Proof. - intros a n m. zify. apply Zshiftr_spec. + intros a n m. zify. apply Z.shiftr_spec. Qed. Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m -> testbit (shiftl a n) m = testbit a (m-n). Proof. intros a n m. zify. intros Hn H. - now apply Zshiftl_spec_high. + now apply Z.shiftl_spec_high. Qed. Lemma shiftl_spec_low : forall a n m, m<n -> testbit (shiftl a n) m = false. Proof. - intros a n m. zify. intros H. now apply Zshiftl_spec_low. + intros a n m. zify. intros H. now apply Z.shiftl_spec_low. Qed. Lemma land_spec : forall a b n, testbit (land a b) n = testbit a n && testbit b n. Proof. - intros a n m. zify. now apply Zand_spec. + intros a n m. zify. now apply Z.land_spec. Qed. Lemma lor_spec : forall a b n, testbit (lor a b) n = testbit a n || testbit b n. Proof. - intros a n m. zify. now apply Zor_spec. + intros a n m. zify. now apply Z.lor_spec. Qed. Lemma ldiff_spec : forall a b n, testbit (ldiff a b) n = testbit a n && negb (testbit b n). Proof. - intros a n m. zify. now apply Zdiff_spec. + intros a n m. zify. now apply Z.ldiff_spec. Qed. Lemma lxor_spec : forall a b n, testbit (lxor a b) n = xorb (testbit a n) (testbit b n). Proof. - intros a n m. zify. now apply Zxor_spec. + intros a n m. zify. now apply Z.lxor_spec. Qed. Lemma div2_spec : forall a, div2 a == shiftr a 1. Proof. - intros a. zify. now apply Zdiv2_spec. + intros a. zify. now apply Z.div2_spec. Qed. End ZTypeIsZAxioms. 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 := diff --git a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v index 225c0853e..a1f4ea9a2 100644 --- a/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v +++ b/theories/Numbers/Natural/SpecViaZ/NSigNAxioms.v @@ -11,7 +11,7 @@ Require Import ZArith OrdersFacts Nnat Ndigits NAxioms NDiv NSig. (** * The interface [NSig.NType] implies the interface [NAxiomsSig] *) -Module NTypeIsNAxioms (Import N : NType'). +Module NTypeIsNAxioms (Import NN : NType'). Hint Rewrite spec_0 spec_1 spec_2 spec_succ spec_add spec_mul spec_pred spec_sub @@ -54,7 +54,7 @@ Definition N_of_Z z := of_N (Zabs_N z). Section Induction. -Variable A : N.t -> Prop. +Variable A : NN.t -> Prop. Hypothesis A_wd : Proper (eq==>iff) A. Hypothesis A0 : A 0. Hypothesis AS : forall n, A n <-> A (succ n). @@ -161,7 +161,7 @@ Proof. intros. zify. apply Z.compare_antisym. Qed. -Include BoolOrderFacts N N N [no inline]. +Include BoolOrderFacts NN NN NN [no inline]. Instance compare_wd : Proper (eq ==> eq ==> Logic.eq) compare. Proof. @@ -371,83 +371,83 @@ 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. + intros. zify. apply Z.testbit_odd_0. Qed. Lemma testbit_even_0 : forall a, testbit (2*a) 0 = false. Proof. - intros. zify. apply Ztestbit_even_0. + intros. zify. apply Z.testbit_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. + intros a n. zify. apply Z.testbit_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. + intros a n. zify. apply Z.testbit_even_succ. Qed. Lemma testbit_neg_r : forall a n, n<0 -> testbit a n = false. Proof. - intros a n. zify. apply Ztestbit_neg_r. + intros a n. zify. apply Z.testbit_neg_r. Qed. Lemma shiftr_spec : forall a n m, 0<=m -> testbit (shiftr a n) m = testbit a (m+n). Proof. - intros a n m. zify. apply Zshiftr_spec. + intros a n m. zify. apply Z.shiftr_spec. Qed. Lemma shiftl_spec_high : forall a n m, 0<=m -> n<=m -> testbit (shiftl a n) m = testbit a (m-n). Proof. - intros a n m. zify. intros Hn H. rewrite Zmax_r by auto with zarith. - now apply Zshiftl_spec_high. + intros a n m. zify. intros Hn H. rewrite Z.max_r by auto with zarith. + now apply Z.shiftl_spec_high. Qed. Lemma shiftl_spec_low : forall a n m, m<n -> testbit (shiftl a n) m = false. Proof. - intros a n m. zify. intros H. now apply Zshiftl_spec_low. + intros a n m. zify. intros H. now apply Z.shiftl_spec_low. Qed. Lemma land_spec : forall a b n, testbit (land a b) n = testbit a n && testbit b n. Proof. - intros a n m. zify. now apply Zand_spec. + intros a n m. zify. now apply Z.land_spec. Qed. Lemma lor_spec : forall a b n, testbit (lor a b) n = testbit a n || testbit b n. Proof. - intros a n m. zify. now apply Zor_spec. + intros a n m. zify. now apply Z.lor_spec. Qed. Lemma ldiff_spec : forall a b n, testbit (ldiff a b) n = testbit a n && negb (testbit b n). Proof. - intros a n m. zify. now apply Zdiff_spec. + intros a n m. zify. now apply Z.ldiff_spec. Qed. Lemma lxor_spec : forall a b n, testbit (lxor a b) n = xorb (testbit a n) (testbit b n). Proof. - intros a n m. zify. now apply Zxor_spec. + intros a n m. zify. now apply Z.lxor_spec. Qed. Lemma div2_spec : forall a, div2 a == shiftr a 1. Proof. - intros a. zify. now apply Zdiv2_spec. + intros a. zify. now apply Z.div2_spec. Qed. (** Recursion *) -Definition recursion (A : Type) (a : A) (f : N.t -> A -> A) (n : N.t) := - Nrect (fun _ => A) a (fun n a => f (N.of_N n) a) (N.to_N n). +Definition recursion (A : Type) (a : A) (f : NN.t -> A -> A) (n : NN.t) := + Nrect (fun _ => A) a (fun n a => f (NN.of_N n) a) (NN.to_N n). Implicit Arguments recursion [A]. Instance recursion_wd (A : Type) (Aeq : relation A) : @@ -456,7 +456,7 @@ Proof. unfold eq. intros a a' Eaa' f f' Eff' x x' Exx'. unfold recursion. -unfold N.to_N. +unfold NN.to_N. rewrite <- Exx'; clear x' Exx'. replace (Zabs_N [x]) with (N_of_nat (Zabs_nat [x])). induction (Zabs_nat [x]). @@ -468,30 +468,30 @@ change (nat_of_P p) with (nat_of_N (Npos p)); apply N_of_nat_of_N. Qed. Theorem recursion_0 : - forall (A : Type) (a : A) (f : N.t -> A -> A), recursion a f 0 = a. + forall (A : Type) (a : A) (f : NN.t -> A -> A), recursion a f 0 = a. Proof. -intros A a f; unfold recursion, N.to_N; rewrite N.spec_0; simpl; auto. +intros A a f; unfold recursion, NN.to_N; rewrite NN.spec_0; simpl; auto. Qed. Theorem recursion_succ : - forall (A : Type) (Aeq : relation A) (a : A) (f : N.t -> A -> A), + forall (A : Type) (Aeq : relation A) (a : A) (f : NN.t -> A -> A), Aeq a a -> Proper (eq==>Aeq==>Aeq) f -> forall n, Aeq (recursion a f (succ n)) (f n (recursion a f n)). Proof. -unfold N.eq, recursion; intros A Aeq a f EAaa f_wd n. -replace (N.to_N (succ n)) with (Nsucc (N.to_N n)). +unfold NN.eq, recursion; intros A Aeq a f EAaa f_wd n. +replace (NN.to_N (succ n)) with (N.succ (NN.to_N n)). rewrite Nrect_step. apply f_wd; auto. -unfold N.to_N. -rewrite N.spec_of_N, Z_of_N_abs, Zabs_eq; auto. - apply N.spec_pos. +unfold NN.to_N. +rewrite NN.spec_of_N, Z_of_N_abs, Zabs_eq; auto. + apply NN.spec_pos. fold (recursion a f n). apply recursion_wd; auto. red; auto. -unfold N.to_N. +unfold NN.to_N. -rewrite N.spec_succ. +rewrite NN.spec_succ. change ([n]+1)%Z with (Zsucc [n]). apply Z_of_N_eq_rev. rewrite Z_of_N_succ. @@ -503,6 +503,6 @@ Qed. End NTypeIsNAxioms. -Module NType_NAxioms (N : NType) - <: NAxiomsSig <: OrderFunctions N <: HasMinMax N - := N <+ NTypeIsNAxioms. +Module NType_NAxioms (NN : NType) + <: NAxiomsSig <: OrderFunctions NN <: HasMinMax NN + := NN <+ NTypeIsNAxioms. |