diff options
| -rw-r--r-- | theories/Numbers/Cyclic/Int31/Cyclic31.v | 315 |
1 files changed, 291 insertions, 24 deletions
diff --git a/theories/Numbers/Cyclic/Int31/Cyclic31.v b/theories/Numbers/Cyclic/Int31/Cyclic31.v index e5975efa4..c1e444fb7 100644 --- a/theories/Numbers/Cyclic/Int31/Cyclic31.v +++ b/theories/Numbers/Cyclic/Int31/Cyclic31.v @@ -156,6 +156,12 @@ Section Basics. Proof. destruct x; simpl; auto. Qed. + + Lemma firstl_firstr : + forall x, firstl x = firstr (nshiftr (pred size) x). + Proof. + destruct x; simpl; auto. + Qed. (** More advanced results about [nshiftr] *) @@ -462,6 +468,42 @@ Section Basics. apply phibis_aux_bounded; auto. Qed. + Lemma phibis_aux_lowerbound : + forall n x, firstr (nshiftr n x) = D1 -> + (2 ^ Z_of_nat n <= phibis_aux (S n) x)%Z. + Proof. + induction n. + intros. + unfold nshiftr in H; simpl in *. + unfold phibis_aux, recrbis_aux. + rewrite H, Zdouble_plus_one_mult; omega. + + intros. + remember (S n) as m. + unfold phibis_aux, recrbis_aux; fold recrbis_aux; + fold (phibis_aux m (shiftr x)). + subst m. + rewrite inj_S, Zpower_Zsucc; auto with zarith. + assert (2^(Z_of_nat n) <= phibis_aux (S n) (shiftr x))%Z. + apply IHn. + rewrite <- nshiftr_S_tail; auto. + destruct (firstr x). + change (Zdouble (phibis_aux (S n) (shiftr x))) with + (2*(phibis_aux (S n) (shiftr x)))%Z. + omega. + rewrite Zdouble_plus_one_mult; omega. + Qed. + + Lemma phi_lowerbound : + forall x, firstl x = D1 -> (2^(Z_of_nat (pred size)) <= phi x)%Z. + Proof. + intros. + generalize (phibis_aux_lowerbound (pred size) x). + rewrite <- firstl_firstr. + change (S (pred size)) with size; auto. + rewrite phibis_aux_equiv; auto. + Qed. + (** * Equivalence modulo [2^n] *) Section EqShiftL. @@ -1539,17 +1581,33 @@ Section Int31_Spec. change (Zabs_nat 1) with 1%nat; omega. Qed. - Lemma spec_add_mul_div : forall x y p, - [|p|] <= Zpos 31 -> - [| addmuldiv31 p x y |] = - ([|x|] * (2 ^ [|p|]) + - [|y|] / (2 ^ ((Zpos 31) - [|p|]))) mod wB. - Proof. - Admitted. (* TODO !! *) + Fixpoint addmuldiv31_alt n i j := + match n with + | O => i + | S n => addmuldiv31_alt n (sneakl (firstl j) i) (shiftl j) + end. -(* (* don't work yet (not enough information in IHn) *) + Lemma addmuldiv31_equiv : forall p x y, + addmuldiv31 p x y = addmuldiv31_alt (Zabs_nat [|p|]) x y. + Proof. + intros. unfold addmuldiv31. - intros; rewrite iter_int31_iter_nat. + rewrite iter_int31_iter_nat. + set (n:=Zabs_nat [|p|]); clearbody n; clear p. + revert x y; induction n. + simpl; auto. + intros. + simpl addmuldiv31_alt. + replace (S n) with (n+1)%nat by (rewrite plus_comm; auto). + rewrite iter_nat_plus; simpl; auto. + Qed. + + Lemma spec_add_mul_div : forall x y p, [|p|] <= Zpos 31 -> + [| addmuldiv31 p x y |] = + ([|x|] * (2 ^ [|p|]) + [|y|] / (2 ^ ((Zpos 31) - [|p|]))) mod wB. + Proof. + intros. + rewrite addmuldiv31_equiv. assert ([|p|] = Z_of_nat (Zabs_nat [|p|])). rewrite inj_Zabs_nat; symmetry; apply Zabs_eq. destruct (phi_bounded p); auto. @@ -1557,29 +1615,54 @@ Section Int31_Spec. set (n := Zabs_nat [|p|]) in *; clearbody n. assert (n <= 31)%nat. rewrite inj_le_iff; auto with zarith. - clear H. + clear p H; revert x y. induction n. - simpl. + simpl; intros. change (Zpower_pos 2 31) with (2^31). rewrite Zmult_1_r. replace ([|y|] / 2^31) with 0. rewrite Zplus_0_r. symmetry; apply Zmod_small; apply phi_bounded. symmetry; apply Zdiv_small; apply phi_bounded. + + simpl addmuldiv31_alt; intros. + rewrite IHn; [ | omega ]. + case_eq (firstl y); intros. + + rewrite phi_twice, Zdouble_mult. + rewrite phi_twice_firstl; auto. + change (Zdouble [|y|]) with (2*[|y|]). + rewrite inj_S, Zpower_Zsucc; auto with zarith. + rewrite Zplus_mod; rewrite Zmult_mod_idemp_l; rewrite <- Zplus_mod. + f_equal. + apply Zplus_eq_compat. + ring. + replace (31-Z_of_nat n) with (Zsucc(31-Zsucc(Z_of_nat n))) by ring. + rewrite Zpower_Zsucc, <- Zdiv_Zdiv; auto with zarith. + rewrite Zmult_comm, Z_div_mult; auto with zarith. - simpl iter_nat. - destruct (iter_nat n (int31 * int31) - (fun ij : int31 * int31 => - let (i, j) := ij in (sneakl (firstl j) i, shiftl j)) - (x, y)). - case_eq (firstl i0); intros; rewrite ?phi_twice,?phi_twice_plus_one; - rewrite ?Zdouble_mult, ?Zdouble_plus_one_mult; - rewrite IHn; try omega. + rewrite phi_twice_plus_one, Zdouble_plus_one_mult. + rewrite phi_twice; auto. + change (Zdouble [|y|]) with (2*[|y|]). rewrite inj_S, Zpower_Zsucc; auto with zarith. - rewrite Zmult_mod_idemp_r, Zmult_plus_distr_r. - -*) + rewrite Zplus_mod; rewrite Zmult_mod_idemp_l; rewrite <- Zplus_mod. + rewrite Zmult_plus_distr_l, Zmult_1_l, <- Zplus_assoc. + f_equal. + apply Zplus_eq_compat. + ring. + assert ((2*[|y|]) mod wB = 2*[|y|] - wB). + admit. + rewrite H1. + replace wB with (2^(Z_of_nat n)*2^(31-Z_of_nat n)) by + (rewrite <- Zpower_exp; auto with zarith; f_equal; unfold size; ring). + unfold Zminus; rewrite Zopp_mult_distr_l. + rewrite Z_div_plus; auto with zarith. + ring_simplify. + replace (31+-Z_of_nat n) with (Zsucc(31-Zsucc(Z_of_nat n))) by ring. + rewrite Zpower_Zsucc, <- Zdiv_Zdiv; auto with zarith. + rewrite Zmult_comm, Z_div_mult; auto with zarith. + Qed. Let w_pos_mod := int31_op.(znz_pos_mod). @@ -1627,9 +1710,106 @@ Section Int31_Spec. intros H'; rewrite <- H'. simpl; auto. Qed. + + Fixpoint head031_alt n x := + match n with + | O => 0%nat + | S n => match firstl x with + | D0 => S (head031_alt n (shiftl x)) + | D1 => 0%nat + end + end. + + Lemma head031_equiv : + forall x, [|head031 x|] = Z_of_nat (head031_alt size x). + Proof. + intros. + case_eq (iszero x); intros. + rewrite (iszero_eq0 _ H). + simpl; auto. + + unfold head031, recl. + change On with (phi_inv (Z_of_nat (31-size))). + replace (head031_alt size x) with + (head031_alt size x + (31 - size))%nat by (apply plus_0_r; auto). + assert (size <= 31)%nat by auto with arith. + + revert x H; induction size; intros. + simpl; auto. + unfold recl_aux; fold recl_aux. + unfold head031_alt; fold head031_alt. + rewrite H. + assert ([|phi_inv (Z_of_nat (31-S n))|] = Z_of_nat (31 - S n)). + rewrite phi_phi_inv. + apply Zmod_small. + split. + change 0 with (Z_of_nat O); apply inj_le; omega. + apply Zle_lt_trans with (Z_of_nat 31). + apply inj_le; omega. + compute; auto. + case_eq (firstl x); intros; auto. + rewrite plus_Sn_m, plus_n_Sm. + replace (S (31 - S n)) with (31 - n)%nat by omega. + rewrite <- IHn; [ | omega | ]. + f_equal; f_equal. + unfold add31. + rewrite H1. + f_equal. + change [|In|] with 1. + replace (31-n)%nat with (S (31 - S n))%nat by omega. + rewrite inj_S; ring. + + clear - H H2. + rewrite (sneakr_shiftl x) in H. + rewrite H2 in H. + case_eq (iszero (shiftl x)); intros; auto. + rewrite (iszero_eq0 _ H0) in H; discriminate. + Qed. + + Lemma phi_nz : forall x, 0 < [|x|] <-> x <> 0%int31. + Proof. + split; intros. + red; intro; subst x; discriminate. + assert ([|x|]<>0%Z). + contradict H. + rewrite <- (phi_inv_phi x); rewrite H; auto. + generalize (phi_bounded x); auto with zarith. + Qed. + Lemma spec_head0 : forall x, 0 < [|x|] -> wB/ 2 <= 2 ^ ([|head031 x|]) * [|x|] < wB. - Admitted. (* TODO !! *) + Proof. + intros. + rewrite head031_equiv. + assert (nshiftl size x = 0%int31). + apply nshiftl_size. + revert x H H0. + unfold size at 2 5. + induction size. + simpl Z_of_nat. + intros. + compute in H0; rewrite H0 in H; discriminate. + + intros. + simpl head031_alt. + case_eq (firstl x); intros. + rewrite (inj_S (head031_alt n (shiftl x))), Zpower_Zsucc; auto with zarith. + rewrite <- Zmult_assoc, Zmult_comm, <- Zmult_assoc, <-(Zmult_comm 2). + rewrite <- Zdouble_mult, <- (phi_twice_firstl _ H1). + apply IHn. + + rewrite phi_nz; rewrite phi_nz in H; contradict H. + change twice with shiftl in H. + rewrite (sneakr_shiftl x), H1, H; auto. + + rewrite <- nshiftl_S_tail; auto. + + change (2^(Z_of_nat 0)) with 1; rewrite Zmult_1_l. + generalize (phi_bounded x); unfold size; split; auto with zarith. + change (2^(Z_of_nat 31)/2) with (2^(Z_of_nat (pred size))). + apply phi_lowerbound; auto. + Qed. + Lemma spec_tail00: forall x, [|x|] = 0 -> [|tail031 x|] = Zpos 31. Proof. intros. @@ -1638,9 +1818,96 @@ Section Int31_Spec. intros H'; rewrite <- H'. simpl; auto. Qed. + + Fixpoint tail031_alt n x := + match n with + | O => 0%nat + | S n => match firstr x with + | D0 => S (tail031_alt n (shiftr x)) + | D1 => 0%nat + end + end. + + Lemma tail031_equiv : + forall x, [|tail031 x|] = Z_of_nat (tail031_alt size x). + Proof. + intros. + case_eq (iszero x); intros. + rewrite (iszero_eq0 _ H). + simpl; auto. + + unfold tail031, recr. + change On with (phi_inv (Z_of_nat (31-size))). + replace (tail031_alt size x) with + (tail031_alt size x + (31 - size))%nat by (apply plus_0_r; auto). + assert (size <= 31)%nat by auto with arith. + + revert x H; induction size; intros. + simpl; auto. + unfold recr_aux; fold recr_aux. + unfold tail031_alt; fold tail031_alt. + rewrite H. + assert ([|phi_inv (Z_of_nat (31-S n))|] = Z_of_nat (31 - S n)). + rewrite phi_phi_inv. + apply Zmod_small. + split. + change 0 with (Z_of_nat O); apply inj_le; omega. + apply Zle_lt_trans with (Z_of_nat 31). + apply inj_le; omega. + compute; auto. + case_eq (firstr x); intros; auto. + rewrite plus_Sn_m, plus_n_Sm. + replace (S (31 - S n)) with (31 - n)%nat by omega. + rewrite <- IHn; [ | omega | ]. + f_equal; f_equal. + unfold add31. + rewrite H1. + f_equal. + change [|In|] with 1. + replace (31-n)%nat with (S (31 - S n))%nat by omega. + rewrite inj_S; ring. + + clear - H H2. + rewrite (sneakl_shiftr x) in H. + rewrite H2 in H. + case_eq (iszero (shiftr x)); intros; auto. + rewrite (iszero_eq0 _ H0) in H; discriminate. + Qed. + Lemma spec_tail0 : forall x, 0 < [|x|] -> exists y, 0 <= y /\ [|x|] = (2 * y + 1) * (2 ^ [|tail031 x|]). - Admitted. (* TODO !! *) + Proof. + intros. + rewrite tail031_equiv. + assert (nshiftr size x = 0%int31). + apply nshiftr_size. + revert x H H0. + induction size. + simpl Z_of_nat. + intros. + compute in H0; rewrite H0 in H; discriminate. + + intros. + simpl tail031_alt. + case_eq (firstr x); intros. + rewrite (inj_S (tail031_alt n (shiftr x))), Zpower_Zsucc; auto with zarith. + destruct (IHn (shiftr x)) as {y,Hy1,Hy2}. + + rewrite phi_nz; rewrite phi_nz in H; contradict H. + rewrite (sneakl_shiftr x), H1, H; auto. + + rewrite <- nshiftr_S_tail; auto. + + exists y; split; auto. + rewrite phi_eqn1; auto. + rewrite Zdouble_mult, Hy2; ring. + + exists [|shiftr x|]. + split. + generalize (phi_bounded (shiftr x)); auto with zarith. + rewrite phi_eqn2; auto. + rewrite Zdouble_plus_one_mult; simpl; ring. + Qed. (* Sqrt *) |