proposition: Theorem spec_w_div32 : forall a1 a2 a3 b1 b2, wB/2 <= [|b1|] -> [[WW a1 a2]] < [[WW b1 b2]] -> let (q,r) := w_div32 a1 a2 a3 b1 b2 in [|a1|] * wwB + [|a2|] * wB + [|a3|] = [|q|] * ([|b1|] * wB + [|b2|]) + [[r]] /\ 0 <= [[r]] < [|b1|] * wB + [|b2|].
proof: Proof. intros a1 a2 a3 b1 b2 Hle Hlt. assert (U:= lt_0_wB w_digits); assert (U1:= lt_0_wwB w_digits). Spec_w_to_Z a1;Spec_w_to_Z a2;Spec_w_to_Z a3;Spec_w_to_Z b1;Spec_w_to_Z b2. rewrite wwB_wBwB; rewrite Z.pow_2_r; rewrite Z.mul_assoc;rewrite <- Z.mul_add_distr_r. change (w_div32 a1 a2 a3 b1 b2) with (w_div32_body a1 a2 a3 b1 b2). unfold w_div32_body. rewrite spec_compare. case Z.compare_spec; intro Hcmp. simpl in Hlt. rewrite Hcmp in Hlt;assert ([|a2|] < [|b2|]). lia. assert ([[WW (w_sub a2 b2) a3]] = ([|a2|]-[|b2|])*wB + [|a3|] + wwB). simpl;rewrite spec_sub. assert ([|a2|] - [|b2|] = wB*(-1) + ([|a2|] - [|b2|] + wB)). ring. assert (0 <= [|a2|] - [|b2|] + wB < wB). lia. rewrite <-(Zmod_unique ([|a2|]-[|b2|]) wB (-1) ([|a2|]-[|b2|]+wB) H1 H0). rewrite wwB_wBwB;ring. assert (U2 := wB_pos w_digits). eapply spec_ww_add_c_cont with (P := fun (x y:zn2z w) (res:w*zn2z w) => let (q, r) := res in ([|a1|] * wB + [|a2|]) * wB + [|a3|] = [|q|] * ([|b1|] * wB + [|b2|]) + [[r]] /\ 0 <= [[r]] < [|b1|] * wB + [|b2|]);eauto. rewrite H0;intros r. repeat (rewrite spec_ww_add;eauto || rewrite spec_w_Bm1 || rewrite spec_w_Bm2); simpl ww_to_Z;try rewrite Z.mul_1_l;intros H1. assert (0<= ([[r]] + ([|b1|] * wB + [|b2|])) - wwB < [|b1|] * wB + [|b2|]). Spec_ww_to_Z r; split. 2: zarith. rewrite H1. assert (H12:= wB_div2 Hle). assert (wwB <= 2 * [|b1|] * wB). rewrite wwB_wBwB; rewrite Z.pow_2_r; zarith. assert (-wwB < ([|a2|] - [|b2|]) * wB + [|a3|] < 0). split. apply Z.lt_le_trans with (([|a2|] - [|b2|]) * wB). 2: zarith. rewrite wwB_wBwB;replace (-(wB^2)) with (-wB*wB);[ | ring]. apply Z.mul_lt_mono_pos_r;zarith. apply Z.le_lt_trans with (([|a2|] - [|b2|]) * wB + (wB -1)). zarith. replace ( ([|a2|] - [|b2|]) * wB + (wB - 1)) with (([|a2|] - [|b2|] + 1) * wB + - 1);[ | ring]. enough (([|a2|] - [|b2|] + 1) * wB <= 0) by zarith. replace 0 with (0*wB);zarith. replace (([|a2|] - [|b2|]) * wB + [|a3|] + wwB + ([|b1|] * wB + [|b2|]) + ([|b1|] * wB + [|b2|]) - wwB) with (([|a2|] - [|b2|]) * wB + [|a3|] + 2*[|b1|] * wB + 2*[|b2|]); [zarith | ring]. rewrite <- (Zmod_unique ([[r]] + ([|b1|] * wB + [|b2|])) wwB 1 ([[r]] + ([|b1|] * wB + [|b2|]) - wwB)). 3: zarith. split. rewrite H1;rewrite Hcmp;ring. trivial. Spec_ww_to_Z (WW b1 b2). simpl in HH4;zarith. rewrite H0;intros r;repeat (rewrite spec_w_Bm1 || rewrite spec_w_Bm2); simpl ww_to_Z;try rewrite Z.mul_1_l;intros H1. assert ([[r]]=([|a2|]-[|b2|])*wB+[|a3|]+([|b1|]*wB+[|b2|])). zarith. split. rewrite H2;rewrite Hcmp;ring. split. Spec_ww_to_Z r;zarith. rewrite H2. enough (([|a2|] - [|b2|]) * wB + [|a3|] < 0) by zarith. apply Z.le_lt_trans with (([|a2|] - [|b2|]) * wB + (wB -1)). zarith. replace ( ([|a2|] - [|b2|]) * wB + (wB - 1)) with (([|a2|] - [|b2|] + 1) * wB + - 1);[ | ring ]. enough (([|a2|] - [|b2|] + 1) * wB <= 0) by zarith. replace 0 with (0*wB);zarith. assert (Hdiv21 := spec_div21 a2 Hle Hcmp); destruct (w_div21 a1 a2 b1) as (q, r);destruct Hdiv21. rewrite H. assert (Hq := spec_to_Z q). generalize (spec_ww_sub_c (w_WW r a3) (w_mul_c q b2)); destruct (ww_sub_c (w_WW r a3) (w_mul_c q b2)) as [r1|r1];repeat (rewrite spec_w_WW || rewrite spec_mul_c); unfold interp_carry;intros H1. rewrite H1. split. ring. split. rewrite <- H1;destruct (spec_ww_to_Z w_digits w_to_Z spec_to_Z r1);trivial. apply Z.le_lt_trans with ([|r|] * wB + [|a3|]). assert ( 0 <= [|q|] * [|b2|]);zarith. apply beta_lex_inv;zarith. assert ([[r1]] = [|r|] * wB + [|a3|] - [|q|] * [|b2|] + wwB). rewrite <- H1;ring. Spec_ww_to_Z r1; assert (0 <= [|r|]*wB). zarith. assert (0 < [|q|] * [|b2|]). zarith. assert (0 < [|q|]). apply Zmult_lt_0_reg_r_2 with [|b2|];zarith. eapply spec_ww_add_c_cont with (P := fun (x y:zn2z w) (res:w*zn2z w) => let (q0, r0) := res in ([|q|] * [|b1|] + [|r|]) * wB + [|a3|] = [|q0|] * ([|b1|] * wB + [|b2|]) + [[r0]] /\ 0 <= [[r0]] < [|b1|] * wB + [|b2|]);eauto. intros r2;repeat (rewrite spec_pred || rewrite spec_ww_add;eauto); simpl ww_to_Z;intros H7. assert (0 < [|q|] - 1). assert (H6 : 1 <= [|q|]) by zarith. Z.le_elim H6. zarith. rewrite <- H6 in H2;rewrite H2 in H7. assert (0 < [|b1|]*wB). apply Z.mul_pos_pos;zarith. Spec_ww_to_Z r2. zarith. rewrite (Zmod_small ([|q|] -1)) by zarith. rewrite (Zmod_small ([|q|] -1 -1)) by zarith. assert ([[r2]] + ([|b1|] * wB + [|b2|]) = wwB * 1 + ([|r|] * wB + [|a3|] - [|q|] * [|b2|] + 2 * ([|b1|] * wB + [|b2|]))). rewrite H7;rewrite H2;ring. assert ([|r|]*wB + [|a3|] - [|q|]*[|b2|] + 2 * ([|b1|]*wB + [|b2|]) < [|b1|]*wB + [|b2|]). Spec_ww_to_Z r2;lia. Spec_ww_to_Z (WW b1 b2). simpl in HH5. assert (0 <= [|r|]*wB + [|a3|] - [|q|]*[|b2|] + 2 * ([|b1|]*wB + [|b2|]) < wwB). split. 2: lia. replace (2*([|b1|]*wB+[|b2|])) with ((2*[|b1|])*wB+2*[|b2|]). 2:ring. assert (H12:= wB_div2 Hle). assert (wwB <= 2 * [|b1|] * wB). rewrite wwB_wBwB; rewrite Z.pow_2_r; zarith. lia. rewrite <- (Zmod_unique ([[r2]] + ([|b1|] * wB + [|b2|])) wwB 1 ([|r|] * wB + [|a3|] - [|q|] * [|b2|] + 2*([|b1|] * wB + [|b2|])) H10 H8). split. ring. zarith. intros r2;repeat (rewrite spec_pred);simpl ww_to_Z;intros H7. rewrite (Zmod_small ([|q|] -1)) by zarith. split. replace [[r2]] with ([[r1]] + ([|b1|] * wB + [|b2|]) -wwB). rewrite H2; ring. rewrite <- H7; ring. Spec_ww_to_Z r2;Spec_ww_to_Z r1. lia. simpl in Hlt. assert ([|a1|] * wB + [|a2|] <= [|b1|] * wB + [|b2|]). zarith. assert (H1 := beta_lex _ _ _ _ _ H HH0 HH3). rewrite spec_w_0;simpl;zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub