diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-04 18:48:06 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-04 18:48:06 +0000 |
commit | 12c796fe185876021e2dfc7753b8f90ba9de31e0 (patch) | |
tree | 38eea7388cb9295f2169ad34eb1682578017aaee | |
parent | fdda04b92b7347f252d41aa76693ec221a07fe47 (diff) |
Ndigits: a Pshiftl_nat used in BigN (was double_digits there)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13764 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | theories/NArith/Ndigits.v | 25 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v | 21 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v | 1 | ||||
-rw-r--r-- | theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v | 115 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake.v | 6 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/NMake_gen.ml | 16 | ||||
-rw-r--r-- | theories/Numbers/Natural/BigN/Nbasic.v | 32 | ||||
-rw-r--r-- | theories/ZArith/Zdigits_def.v | 16 |
8 files changed, 121 insertions, 111 deletions
diff --git a/theories/NArith/Ndigits.v b/theories/NArith/Ndigits.v index a5d6b6730..0c660a44e 100644 --- a/theories/NArith/Ndigits.v +++ b/theories/NArith/Ndigits.v @@ -347,6 +347,31 @@ Proof. apply nat_compare_lt. now rewrite <- nat_of_Ncompare. Qed. +(** A left shift for positive numbers (used in BigN) *) + +Definition Pshiftl_nat (p:positive)(n:nat) := iter_nat n _ xO p. + +Lemma Pshiftl_nat_0 : forall p, Pshiftl_nat p 0 = p. +Proof. reflexivity. Qed. + +Lemma Pshiftl_nat_S : + forall p n, Pshiftl_nat p (S n) = xO (Pshiftl_nat p n). +Proof. reflexivity. Qed. + +Lemma Pshiftl_nat_N : + forall p n, Npos (Pshiftl_nat p n) = Nshiftl_nat (Npos p) n. +Proof. + unfold Pshiftl_nat, Nshiftl_nat. + induction n; simpl; auto. now rewrite <- IHn. +Qed. + +Lemma Pshiftl_nat_plus : forall n m p, + Pshiftl_nat p (m + n) = Pshiftl_nat (Pshiftl_nat p n) m. +Proof. + induction m; simpl; intros. reflexivity. + rewrite 2 Pshiftl_nat_S. now f_equal. +Qed. + (** Semantics of bitwise operations *) Lemma Pxor_semantics : forall p p' n, diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v index af113da2b..d92e818ff 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleBase.v @@ -10,12 +10,14 @@ Set Implicit Arguments. -Require Import ZArith. +Require Import ZArith Ndigits. Require Import BigNumPrelude. Require Import DoubleType. Local Open Scope Z_scope. +Local Infix "<<" := Pshiftl_nat (at level 30). + Section DoubleBase. Variable w : Type. Variable w_0 : w. @@ -68,13 +70,7 @@ Section DoubleBase. end end. - Fixpoint double_digits (n:nat) : positive := - match n with - | O => w_digits - | S n => xO (double_digits n) - end. - - Definition double_wB n := base (double_digits n). + Definition double_wB n := base (w_digits << n). Fixpoint double_to_Z (n:nat) : word w n -> Z := match n return word w n -> Z with @@ -291,11 +287,10 @@ Section DoubleBase. Lemma double_wB_wwB : forall n, double_wB n * double_wB n = double_wB (S n). Proof. intros n;unfold double_wB;simpl. - unfold base;rewrite (Zpos_xO (double_digits n)). - replace (2 * Zpos (double_digits n)) with - (Zpos (double_digits n) + Zpos (double_digits n)). + unfold base. rewrite Pshiftl_nat_S, (Zpos_xO (_ << _)). + replace (2 * Zpos (w_digits << n)) with + (Zpos (w_digits << n) + Zpos (w_digits << n)) by ring. symmetry; apply Zpower_exp;intro;discriminate. - ring. Qed. Lemma double_wB_pos: @@ -309,7 +304,7 @@ Section DoubleBase. Proof. clear spec_w_0 spec_w_1 spec_w_Bm1 w_0 w_1 w_Bm1. intros n; elim n; clear n; auto. - unfold double_wB, double_digits; auto with zarith. + unfold double_wB, "<<"; auto with zarith. intros n H1; rewrite <- double_wB_wwB. apply Zle_trans with (wB * 1). rewrite Zmult_1_r; apply Zle_refl. diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v index c6c8e8d99..0cb6848e3 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDiv.v @@ -1044,7 +1044,6 @@ Section DoubleDivGt. assert (H2:= @spec_double_divn1 w w_digits w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub w_to_Z spec_to_Z spec_w_zdigits spec_w_0 spec_w_WW spec_head0 spec_add_mul_div spec_div21 spec_compare spec_sub 1 (WW ah al) bl Hpos). - unfold double_to_Z,double_wB,double_digits in H2. destruct (double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW ah al) bl). diff --git a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v index 332def286..bf92bbb98 100644 --- a/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v +++ b/theories/Numbers/Cyclic/DoubleCyclic/DoubleDivn1.v @@ -10,13 +10,15 @@ Set Implicit Arguments. -Require Import ZArith. +Require Import ZArith Ndigits. Require Import BigNumPrelude. Require Import DoubleType. Require Import DoubleBase. Local Open Scope Z_scope. +Local Infix "<<" := Pshiftl_nat (at level 30). + Section GENDIVN1. Variable w : Type. @@ -155,14 +157,10 @@ Section GENDIVN1. | S n => double_divn1_p_aux n (double_divn1_p n) end. - Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (double_digits w_digits n). + Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (w_digits << n). Proof. -(* - induction n;simpl. destruct p_bounded;trivial. - case (spec_to_Z p); rewrite Zpos_xO;auto with zarith. -*) induction n;simpl. trivial. - case (spec_to_Z p); rewrite Zpos_xO;auto with zarith. + case (spec_to_Z p); rewrite Pshiftl_nat_S, Zpos_xO;auto with zarith. Qed. Lemma spec_double_divn1_p : forall n r h l, @@ -170,14 +168,14 @@ Section GENDIVN1. let (q,r') := double_divn1_p n r h l in [|r|] * double_wB w_digits n + ([!n|h!]*2^[|p|] + - [!n|l!] / (2^(Zpos(double_digits w_digits n) - [|p|]))) + [!n|l!] / (2^(Zpos(w_digits << n) - [|p|]))) mod double_wB w_digits n = [!n|q!] * [|b2p|] + [|r'|] /\ 0 <= [|r'|] < [|b2p|]. Proof. case (spec_to_Z p); intros HH0 HH1. induction n;intros. simpl (double_divn1_p 0 r h l). - unfold double_to_Z, double_wB, double_digits. + unfold double_to_Z, double_wB, "<<". rewrite <- spec_add_mul_divp. exact (spec_div21 (w_add_mul_div p h l) b2p_le H). simpl (double_divn1_p (S n) r h l). @@ -189,24 +187,24 @@ Section GENDIVN1. replace ([|r|] * (double_wB w_digits n * double_wB w_digits n) + (([!n|hh!] * double_wB w_digits n + [!n|hl!]) * 2 ^ [|p|] + ([!n|lh!] * double_wB w_digits n + [!n|ll!]) / - 2^(Zpos (double_digits w_digits (S n)) - [|p|])) mod + 2^(Zpos (w_digits << (S n)) - [|p|])) mod (double_wB w_digits n * double_wB w_digits n)) with (([|r|] * double_wB w_digits n + ([!n|hh!] * 2^[|p|] + - [!n|hl!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod + [!n|hl!] / 2^(Zpos (w_digits << n) - [|p|])) mod double_wB w_digits n) * double_wB w_digits n + ([!n|hl!] * 2^[|p|] + - [!n|lh!] / 2^(Zpos (double_digits w_digits n) - [|p|])) mod + [!n|lh!] / 2^(Zpos (w_digits << n) - [|p|])) mod double_wB w_digits n). generalize (IHn r hh hl H);destruct (double_divn1_p n r hh hl) as (qh,rh); intros (H3,H4);rewrite H3. assert ([|rh|] < [|b2p|]). omega. replace (([!n|qh!] * [|b2p|] + [|rh|]) * double_wB w_digits n + ([!n|hl!] * 2 ^ [|p|] + - [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod + [!n|lh!] / 2 ^ (Zpos (w_digits << n) - [|p|])) mod double_wB w_digits n) with ([!n|qh!] * [|b2p|] *double_wB w_digits n + ([|rh|]*double_wB w_digits n + ([!n|hl!] * 2 ^ [|p|] + - [!n|lh!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])) mod + [!n|lh!] / 2 ^ (Zpos (w_digits << n) - [|p|])) mod double_wB w_digits n)). 2:ring. generalize (IHn rh hl lh H0);destruct (double_divn1_p n rh hl lh) as (ql,rl); intros (H5,H6);rewrite H5. @@ -222,52 +220,52 @@ Section GENDIVN1. unfold double_wB,base. assert (UU:=p_lt_double_digits n). rewrite Zdiv_shift_r;auto with zarith. - 2:change (Zpos (double_digits w_digits (S n))) - with (2*Zpos (double_digits w_digits n));auto with zarith. - replace (2 ^ (Zpos (double_digits w_digits (S n)) - [|p|])) with - (2^(Zpos (double_digits w_digits n) - [|p|])*2^Zpos (double_digits w_digits n)). + 2:change (Zpos (w_digits << (S n))) + with (2*Zpos (w_digits << n));auto with zarith. + replace (2 ^ (Zpos (w_digits << (S n)) - [|p|])) with + (2^(Zpos (w_digits << n) - [|p|])*2^Zpos (w_digits << n)). rewrite Zdiv_mult_cancel_r;auto with zarith. rewrite Zmult_plus_distr_l with (p:= 2^[|p|]). pattern ([!n|hl!] * 2^[|p|]) at 2; - rewrite (shift_unshift_mod (Zpos(double_digits w_digits n))([|p|])([!n|hl!])); + rewrite (shift_unshift_mod (Zpos(w_digits << n))([|p|])([!n|hl!])); auto with zarith. rewrite Zplus_assoc. replace - ([!n|hh!] * 2^Zpos (double_digits w_digits n)* 2^[|p|] + - ([!n|hl!] / 2^(Zpos (double_digits w_digits n)-[|p|])* - 2^Zpos(double_digits w_digits n))) + ([!n|hh!] * 2^Zpos (w_digits << n)* 2^[|p|] + + ([!n|hl!] / 2^(Zpos (w_digits << n)-[|p|])* + 2^Zpos(w_digits << n))) with (([!n|hh!] *2^[|p|] + double_to_Z w_digits w_to_Z n hl / - 2^(Zpos (double_digits w_digits n)-[|p|])) - * 2^Zpos(double_digits w_digits n));try (ring;fail). + 2^(Zpos (w_digits << n)-[|p|])) + * 2^Zpos(w_digits << n));try (ring;fail). rewrite <- Zplus_assoc. rewrite <- (Zmod_shift_r ([|p|]));auto with zarith. replace - (2 ^ Zpos (double_digits w_digits n) * 2 ^ Zpos (double_digits w_digits n)) with - (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n))). - rewrite (Zmod_shift_r (Zpos (double_digits w_digits n)));auto with zarith. - replace (2 ^ (Zpos (double_digits w_digits n) + Zpos (double_digits w_digits n))) - with (2^Zpos(double_digits w_digits n) *2^Zpos(double_digits w_digits n)). + (2 ^ Zpos (w_digits << n) * 2 ^ Zpos (w_digits << n)) with + (2 ^ (Zpos (w_digits << n) + Zpos (w_digits << n))). + rewrite (Zmod_shift_r (Zpos (w_digits << n)));auto with zarith. + replace (2 ^ (Zpos (w_digits << n) + Zpos (w_digits << n))) + with (2^Zpos(w_digits << n) *2^Zpos(w_digits << n)). rewrite (Zmult_comm (([!n|hh!] * 2 ^ [|p|] + - [!n|hl!] / 2 ^ (Zpos (double_digits w_digits n) - [|p|])))). + [!n|hl!] / 2 ^ (Zpos (w_digits << n) - [|p|])))). rewrite Zmult_mod_distr_l;auto with zarith. ring. rewrite Zpower_exp;auto with zarith. - assert (0 < Zpos (double_digits w_digits n)). unfold Zlt;reflexivity. + assert (0 < Zpos (w_digits << n)). unfold Zlt;reflexivity. auto with zarith. apply Z_mod_lt;auto with zarith. rewrite Zpower_exp;auto with zarith. split;auto with zarith. apply Zdiv_lt_upper_bound;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace ([|p|] + (Zpos (double_digits w_digits n) - [|p|])) with - (Zpos(double_digits w_digits n));auto with zarith. + replace ([|p|] + (Zpos (w_digits << n) - [|p|])) with + (Zpos(w_digits << n));auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (double_digits w_digits (S n)) - [|p|]) with - (Zpos (double_digits w_digits n) - [|p|] + - Zpos (double_digits w_digits n));trivial. - change (Zpos (double_digits w_digits (S n))) with - (2*Zpos (double_digits w_digits n)). ring. + replace (Zpos (w_digits << (S n)) - [|p|]) with + (Zpos (w_digits << n) - [|p|] + + Zpos (w_digits << n));trivial. + change (Zpos (w_digits << (S n))) with + (2*Zpos (w_digits << n)). ring. Qed. Definition double_modn1_p_aux n (modn1 : w -> word w n -> word w n -> w) r h l:= @@ -304,20 +302,21 @@ Section GENDIVN1. end end. - Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (double_digits w_digits n). + Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (w_digits << n). Proof. induction n;simpl;auto with zarith. - change (Zpos (xO (double_digits w_digits n))) with - (2*Zpos (double_digits w_digits n)). - assert (0 < Zpos w_digits);auto with zarith. - exact (refl_equal Lt). + rewrite Pshiftl_nat_S. + change (Zpos (xO (w_digits << n))) with + (2*Zpos (w_digits << n)). + assert (0 < Zpos w_digits) by reflexivity. + auto with zarith. Qed. Lemma spec_high : forall n (x:word w n), - [|high n x|] = [!n|x!] / 2^(Zpos (double_digits w_digits n) - Zpos w_digits). + [|high n x|] = [!n|x!] / 2^(Zpos (w_digits << n) - Zpos w_digits). Proof. induction n;intros. - unfold high,double_digits,double_to_Z. + unfold high,double_to_Z. rewrite Pshiftl_nat_0. replace (Zpos w_digits - Zpos w_digits) with 0;try ring. simpl. rewrite <- (Zdiv_unique [|x|] 1 [|x|] 0);auto with zarith. assert (U2 := spec_double_digits n). @@ -329,18 +328,18 @@ Section GENDIVN1. assert (U1 := spec_double_to_Z w_digits w_to_Z spec_to_Z n w1). simpl [!S n|WW w0 w1!]. unfold double_wB,base;rewrite Zdiv_shift_r;auto with zarith. - replace (2 ^ (Zpos (double_digits w_digits (S n)) - Zpos w_digits)) with - (2^(Zpos (double_digits w_digits n) - Zpos w_digits) * - 2^Zpos (double_digits w_digits n)). + replace (2 ^ (Zpos (w_digits << (S n)) - Zpos w_digits)) with + (2^(Zpos (w_digits << n) - Zpos w_digits) * + 2^Zpos (w_digits << n)). rewrite Zdiv_mult_cancel_r;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (double_digits w_digits n) - Zpos w_digits + - Zpos (double_digits w_digits n)) with - (Zpos (double_digits w_digits (S n)) - Zpos w_digits);trivial. - change (Zpos (double_digits w_digits (S n))) with - (2*Zpos (double_digits w_digits n));ring. - change (Zpos (double_digits w_digits (S n))) with - (2*Zpos (double_digits w_digits n)); auto with zarith. + replace (Zpos (w_digits << n) - Zpos w_digits + + Zpos (w_digits << n)) with + (Zpos (w_digits << (S n)) - Zpos w_digits);trivial. + change (Zpos (w_digits << (S n))) with + (2*Zpos (w_digits << n));ring. + change (Zpos (w_digits << (S n))) with + (2*Zpos (w_digits << n)); auto with zarith. Qed. Definition double_divn1 (n:nat) (a:word w n) (b:w) := @@ -425,13 +424,13 @@ Section GENDIVN1. rewrite spec_add_mul_div in H7;auto with zarith. rewrite spec_0 in H7;rewrite Zmult_0_l in H7;rewrite Zplus_0_l in H7. assert (([|high n a|] / 2 ^ (Zpos w_digits - [|w_head0 b|])) mod wB - = [!n|a!] / 2^(Zpos (double_digits w_digits n) - [|w_head0 b|])). + = [!n|a!] / 2^(Zpos (w_digits << n) - [|w_head0 b|])). rewrite Zmod_small;auto with zarith. rewrite spec_high. rewrite Zdiv_Zdiv;auto with zarith. rewrite <- Zpower_exp;auto with zarith. - replace (Zpos (double_digits w_digits n) - Zpos w_digits + + replace (Zpos (w_digits << n) - Zpos w_digits + (Zpos w_digits - [|w_head0 b|])) - with (Zpos (double_digits w_digits n) - [|w_head0 b|]);trivial;ring. + with (Zpos (w_digits << n) - [|w_head0 b|]);trivial;ring. assert (H8 := Zpower_gt_0 2 (Zpos w_digits - [|w_head0 b|]));auto with zarith. split;auto with zarith. apply Zle_lt_trans with ([|high n a|]);auto with zarith. diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 105cf0620..23cfec5e9 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -64,7 +64,7 @@ Module Make (W0:CyclicType) <: NType. Proof. intros. change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))). - rewrite !digits_dom_op, !Pshiftl_Zpower. + rewrite !digits_dom_op, !Pshiftl_nat_Zpower. apply Zmult_le_compat_l; auto with zarith. apply Zpower_le_monotone2; auto with zarith. Qed. @@ -1050,7 +1050,7 @@ Module Make (W0:CyclicType) <: NType. unfold base. apply Zlt_le_trans with (1 := pheight_correct x). apply Zpower_le_monotone2; auto with zarith. - rewrite (digits_dom_op (_ _)), Pshiftl_Zpower. auto with zarith. + rewrite (digits_dom_op (_ _)), Pshiftl_nat_Zpower. auto with zarith. Qed. Definition of_N (x:N) : t := @@ -1392,7 +1392,7 @@ Module Make (W0:CyclicType) <: NType. forall x, Zpos (digits (double_size x)) = 2 * (Zpos (digits x)). Proof. intros x. rewrite ! digits_level, double_size_level. - rewrite 2 digits_dom_op, 2 Pshiftl_Zpower, + rewrite 2 digits_dom_op, 2 Pshiftl_nat_Zpower, inj_S, Zpower_Zsucc; auto with zarith. ring. Qed. diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml index 8779f4be3..b5cc4c51d 100644 --- a/theories/Numbers/Natural/BigN/NMake_gen.ml +++ b/theories/Numbers/Natural/BigN/NMake_gen.ml @@ -49,7 +49,7 @@ pr (** Remark: File automatically generated by NMake_gen.ml, DO NOT EDIT ! *) -Require Import BigNumPrelude ZArith CyclicAxioms +Require Import BigNumPrelude ZArith Ndigits CyclicAxioms DoubleType DoubleMul DoubleDivn1 DoubleCyclic Nbasic Wf_nat StreamMemo. @@ -248,10 +248,10 @@ pr Qed. Theorem digits_nmake : forall n ww (w_op: ZnZ.Ops ww), - ZnZ.digits (nmake_op _ w_op n) = Pshiftl (ZnZ.digits w_op) n. + ZnZ.digits (nmake_op _ w_op n) = Pshiftl_nat (ZnZ.digits w_op) n. Proof. induction n. auto. - intros ww ww_op; simpl Pshiftl. rewrite <- IHn; auto. + intros ww ww_op. rewrite Pshiftl_nat_S, <- IHn; auto. Qed. Theorem nmake_double: forall n ww (w_op: ZnZ.Ops ww), @@ -331,7 +331,7 @@ pr " (** * Digits *) Lemma digits_make_op_0 : forall n, - ZnZ.digits (make_op n) = Pshiftl (ZnZ.digits (dom_op Size)) (S n). + ZnZ.digits (make_op n) = Pshiftl_nat (ZnZ.digits (dom_op Size)) (S n). Proof. induction n. auto. @@ -341,15 +341,15 @@ pr " Qed. Lemma digits_make_op : forall n, - ZnZ.digits (make_op n) = Pshiftl (ZnZ.digits w0_op) (SizePlus (S n)). + ZnZ.digits (make_op n) = Pshiftl_nat (ZnZ.digits w0_op) (SizePlus (S n)). Proof. intros. rewrite digits_make_op_0. replace (SizePlus (S n)) with (S n + Size) by (rewrite <- plus_comm; auto). - rewrite Pshiftl_plus. auto. + rewrite Pshiftl_nat_plus. auto. Qed. Lemma digits_dom_op : forall n, - ZnZ.digits (dom_op n) = Pshiftl (ZnZ.digits w0_op) n. + ZnZ.digits (dom_op n) = Pshiftl_nat (ZnZ.digits w0_op) n. Proof. do_size (destruct n; try reflexivity). exact (digits_make_op n). @@ -358,7 +358,7 @@ pr " Lemma digits_dom_op_nmake : forall n m, ZnZ.digits (dom_op (m+n)) = ZnZ.digits (nmake_op _ (dom_op n) m). Proof. - intros. rewrite digits_nmake, 2 digits_dom_op. apply Pshiftl_plus. + intros. rewrite digits_nmake, 2 digits_dom_op. apply Pshiftl_nat_plus. Qed. (** * Conversion between [zn2z (dom_t n)] and [dom_t (S n)]. diff --git a/theories/Numbers/Natural/BigN/Nbasic.v b/theories/Numbers/Natural/BigN/Nbasic.v index 552002e44..94f6b32fd 100644 --- a/theories/Numbers/Natural/BigN/Nbasic.v +++ b/theories/Numbers/Natural/BigN/Nbasic.v @@ -8,7 +8,7 @@ (* Benjamin Gregoire, Laurent Thery, INRIA, 2007 *) (************************************************************************) -Require Import ZArith. +Require Import ZArith Ndigits. Require Import BigNumPrelude. Require Import Max. Require Import DoubleType. @@ -358,8 +358,8 @@ Section CompareRec. intros n (H0, H); split; auto. apply Zlt_le_trans with (1:= H). unfold double_wB, DoubleBase.double_wB; simpl. - rewrite base_xO. - set (u := base (double_digits wm_base n)). + rewrite Pshiftl_nat_S, base_xO. + set (u := base (Pshiftl_nat wm_base n)). assert (0 < u). unfold u, base; auto with zarith. replace (u^2) with (u * u); simpl; auto with zarith. @@ -480,30 +480,6 @@ End AddS. End SimplOp. -(** TODO : to migrate in NArith *) - - Notation Pshiftl := DoubleBase.double_digits. - - Lemma Pshiftl_plus : forall n m p, - Pshiftl p (m + n) = Pshiftl (Pshiftl p n) m. - Proof. - induction m; simpl; congruence. - Qed. - - Lemma Pshiftl_Zpower : forall n d, - Zpos (Pshiftl d n) = (Zpos d * 2 ^ Z_of_nat n)%Z. - Proof. - intros. - rewrite Zmult_comm. - induction n. simpl; auto. - transitivity (2 * (2 ^ Z_of_nat n * Zpos d))%Z. - rewrite <- IHn. auto. - rewrite Zmult_assoc. - rewrite <- Zpower_Zsucc, inj_S; auto with zarith. - Qed. - -(** END TODO *) - (** Abstract vision of a datatype of arbitrary-large numbers. Concrete operations can be derived from these generic fonctions, in particular from [iter_t] and [same_level]. @@ -518,7 +494,7 @@ Declare Instance dom_op n : ZnZ.Ops (dom_t n). Declare Instance dom_spec n : ZnZ.Specs (dom_op n). Axiom digits_dom_op : forall n, - ZnZ.digits (dom_op n) = Pshiftl (ZnZ.digits (dom_op 0)) n. + ZnZ.digits (dom_op n) = Pshiftl_nat (ZnZ.digits (dom_op 0)) n. (** The type [t] of arbitrary-large numbers, with abstract constructor [mk_t] and destructor [destr_t] and iterator [iter_t] *) diff --git a/theories/ZArith/Zdigits_def.v b/theories/ZArith/Zdigits_def.v index 028149eb8..618214357 100644 --- a/theories/ZArith/Zdigits_def.v +++ b/theories/ZArith/Zdigits_def.v @@ -418,3 +418,19 @@ Proof. now rewrite Nxor_spec, negb_xorb_l. now rewrite Nxor_spec, xorb_negb_negb. Qed. + +(** An additionnal proof concerning [Pshiftl_nat], used in BigN *) + +Lemma Pshiftl_nat_Zpower : forall n p, + Zpos (Pshiftl_nat p n) = Zpos p * 2 ^ Z_of_nat n. +Proof. + intros. + rewrite Zmult_comm. + induction n. simpl; auto. + transitivity (2 * (2 ^ Z_of_nat n * Zpos p)). + rewrite <- IHn. auto. + rewrite Zmult_assoc. + rewrite inj_S. + rewrite <- Zpower_succ_r; auto with zarith. + apply Zle_0_nat. +Qed. |