proposition: Theorem ww_lsl_n_spec: forall w, [[w]] < [|b|] * [|b|] -> [[ww_lsl_n w]] = 2 ^ [|n|] * [[w]].
proof: Proof. intros w2 H; unfold ww_lsl_n. case n_spec; intros Hp Hp1. assert (F0: forall x, 2 * x = x + x) by auto with zarith. assert (F1: [|n|] < Zpos (ZnZ.digits w_op)). case (Zle_or_lt (Zpos (ZnZ.digits w_op)) [|n|]). 2: auto. intros H1; contradict Hp1; apply Zle_not_lt; unfold base. apply Z.le_trans with (2 ^ [|n|] * 1). 2: auto with zarith. rewrite Zmult_1_r; apply Zpower_le_monotone; auto with zarith. assert (F2: [|n|] < Zpos (xO (ZnZ.digits w_op))). rewrite (Zpos_xO (ZnZ.digits w_op)). rewrite F0. pattern [|n|]; rewrite <- Zplus_0_r. apply Zplus_lt_compat; auto with zarith. change ([[DoubleLift.ww_add_mul_div w0 wWW wW0 w0W ww_compare w_add_mul_div ww_sub w_zdigits low (w0W n) w2 W0]] = 2 ^ [|n|] * [[w2]]). rewrite (DoubleLift.spec_ww_add_mul_div ). 2: auto with zarith. 2: apply ZnZ.spec_to_Z; auto. 2: refine (spec_ww_to_Z _ _ _); auto. 2: apply ZnZ.spec_to_Z; auto. 2: apply ZnZ.spec_WW; auto. 2: apply ZnZ.spec_WO; auto. 2: apply ZnZ.spec_OW; auto. 2: refine (spec_ww_compare _ _ _ _ _ _ _); auto. 2: apply ZnZ.spec_to_Z; auto. 2: apply ZnZ.spec_compare; auto. 2: apply ZnZ.spec_add_mul_div; auto. 2: refine (spec_ww_sub _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _); auto. 2: apply ZnZ.spec_to_Z; auto. 2: apply ZnZ.spec_WW; auto. 2: apply ZnZ.spec_opp_c; auto. 2: apply ZnZ.spec_opp; auto. 2: apply ZnZ.spec_opp_carry; auto. 2: apply ZnZ.spec_sub_c; auto. 2: apply ZnZ.spec_sub; auto. 2: apply ZnZ.spec_sub_carry; auto. 2: apply ZnZ.spec_zdigits; auto. replace ([[w0W n]]) with [|n|]. change [[W0]] with 0. rewrite Zdiv_0_l; auto with zarith. rewrite Zplus_0_r; rewrite Zmod_small; auto with zarith. split; auto with zarith. case spec_ww_to_Z with (w_digits := w_digits) (w_to_Z := w_to_Z) (x:=w2); auto with zarith. apply ZnZ.spec_to_Z; auto. apply Z.lt_trans with ([|b|] * [|b|] * 2 ^ [|n|]); auto with zarith. apply Zmult_lt_compat_r; auto with zarith. rewrite <- Zmult_assoc. unfold base; unfold base in Hp. unfold ww_digits,w_digits;rewrite (Zpos_xO (ZnZ.digits w_op)); rewrite F0; auto with zarith. rewrite Zpower_exp; auto with zarith. apply Zmult_lt_compat; auto with zarith. case (ZnZ.spec_to_Z b); auto with zarith. split; auto with zarith. rewrite Zmult_comm; auto with zarith. unfold w_digits;auto with zarith. generalize (ZnZ.spec_OW n). unfold ww_to_Z, w_digits; auto. intros x; case x; simpl. unfold w_to_Z, w_digits, w0; rewrite ZnZ.spec_0; auto. intros w3 w4; rewrite Zplus_comm. rewrite Z_mod_plus; auto with zarith. rewrite Zmod_small; auto with zarith. case (ZnZ.spec_to_Z w4); auto with zarith. unfold base; auto with zarith. unfold ww_to_Z, w_digits, w_to_Z, w0W; auto. rewrite ZnZ.spec_OW; auto with zarith. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux