proposition: Lemma spec_mul_aux : forall xh xl yh yl wc (cc:zn2z w) hh ll, [[hh]] = [|xh|] * [|yh|] -> [[ll]] = [|xl|] * [|yl|] -> [|wc|]*wB^2 + [[cc]] = [|xh|] * [|yl|] + [|xl|] * [|yh|] -> [||match cc with | W0 => WW (ww_add hh (w_W0 wc)) ll | WW cch ccl => match ww_add_c (w_W0 ccl) ll with | C0 l => WW (ww_add hh (w_WW wc cch)) l | C1 l => WW (ww_add_carry hh (w_WW wc cch)) l end end||] = ([|xh|] * wB + [|xl|]) * ([|yh|] * wB + [|yl|]).
proof: Proof. intros;assert (U1 := wB_pos w_digits). replace (([|xh|] * wB + [|xl|]) * ([|yh|] * wB + [|yl|])) with ([|xh|]*[|yh|]*wB^2 + ([|xh|]*[|yl|] + [|xl|]*[|yh|])*wB + [|xl|]*[|yl|]). 2:ring. rewrite <- H1;rewrite <- H;rewrite <- H0. assert (H2 := sum_mul_carry _ _ _ _ _ _ H1). destruct cc as [ | cch ccl]; simpl zn2z_to_Z; simpl ww_to_Z. rewrite spec_ww_add;rewrite spec_w_W0;rewrite Zmod_small; rewrite wwB_wBwB. ring. rewrite <- (Z.add_0_r ([|wc|]*wB));rewrite H;apply mult_add_ineq3;zarith. simpl ww_to_Z in H1. assert (U:=spec_to_Z cch). assert ([|wc|]*wB + [|cch|] <= 2*wB - 3). destruct (Z_le_gt_dec ([|wc|]*wB + [|cch|]) (2*wB - 3)) as [Hle|Hgt];trivial. assert ([|xh|] * [|yl|] + [|xl|] * [|yh|] <= (2*wB - 4)*wB + 2). ring_simplify ((2*wB - 4)*wB + 2). assert (H4 := Zmult_lt_b _ _ _ (spec_to_Z xh) (spec_to_Z yl)). assert (H5 := Zmult_lt_b _ _ _ (spec_to_Z xl) (spec_to_Z yh)). lia. generalize H3;clear H3;rewrite <- H1. rewrite Z.add_assoc; rewrite Z.pow_2_r; rewrite Z.mul_assoc; rewrite <- Z.mul_add_distr_r. assert (((2 * wB - 4) + 2)*wB <= ([|wc|] * wB + [|cch|])*wB). apply Z.mul_le_mono_nonneg;zarith. rewrite Z.mul_add_distr_r in H3. intros. assert (U2 := spec_to_Z ccl);lia. generalize (spec_ww_add_c (w_W0 ccl) ll);destruct (ww_add_c (w_W0 ccl) ll) as [l|l];unfold interp_carry;rewrite spec_w_W0;try rewrite Z.mul_1_l; simpl zn2z_to_Z; try rewrite spec_ww_add;try rewrite spec_ww_add_carry;rewrite spec_w_WW; rewrite Zmod_small;rewrite wwB_wBwB;intros. rewrite H4;ring. rewrite H;apply mult_add_ineq2;zarith. rewrite Z.add_assoc;rewrite Z.mul_add_distr_r. rewrite Z.mul_1_l;rewrite <- Z.add_assoc;rewrite H4;ring. repeat rewrite <- Z.add_assoc;rewrite H;apply mult_add_ineq2;zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase