proposition: Lemma spec_ww_gcd_gt_aux_body : forall ah al bh bl n cont, [[WW bh bl]] <= 2^n -> [[WW ah al]] > [[WW bh bl]] -> (forall xh xl yh yl, [[WW xh xl]] > [[WW yh yl]] -> [[WW yh yl]] <= 2^(n-1) -> Zis_gcd [[WW xh xl]] [[WW yh yl]] [[cont xh xl yh yl]]) -> Zis_gcd [[WW ah al]] [[WW bh bl]] [[ww_gcd_gt_body cont ah al bh bl]].
proof: Proof. intros ah al bh bl n cont Hlog Hgt Hcont. change (ww_gcd_gt_body cont ah al bh bl) with (match w_compare w_0 bh with | Eq => match w_compare w_0 bl with | Eq => WW ah al | Lt => let m := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW ah al) bl in WW w_0 (w_gcd_gt bl m) | Gt => W0 end | Lt => let m := ww_mod_gt_aux ah al bh bl in match m with | W0 => WW bh bl | WW mh ml => match w_compare w_0 mh with | Eq => match w_compare w_0 ml with | Eq => WW bh bl | _ => let r := double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21 w_compare w_sub 1 (WW bh bl) ml in WW w_0 (w_gcd_gt ml r) end | Lt => let r := ww_mod_gt_aux bh bl mh ml in match r with | W0 => m | WW rh rl => cont mh ml rh rl end | Gt => W0 end end | Gt => W0 end). rewrite spec_compare, spec_w_0. case Z.compare_spec; intros Hbh. simpl ww_to_Z in *. rewrite <- Hbh. rewrite Z.mul_0_l;rewrite Z.add_0_l. rewrite spec_compare, spec_w_0. case Z.compare_spec; intros Hbl. rewrite <- Hbl;apply Zis_gcd_0. simpl;rewrite spec_w_0;rewrite Z.mul_0_l;rewrite Z.add_0_l. apply Zis_gcd_mod. zarith. change ([|ah|] * wB + [|al|]) with (double_to_Z w_digits w_to_Z 1 (WW ah al)). rewrite <- (@spec_double_modn1 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 Hbl). apply spec_gcd_gt. rewrite (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial. apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. Spec_w_to_Z bl;exfalso;lia. assert (H:= spec_ww_mod_gt_aux _ _ _ Hgt Hbh). assert (H2 : 0 < [[WW bh bl]]). simpl;Spec_w_to_Z bl. apply Z.lt_le_trans with ([|bh|]*wB). 2: zarith. apply Z.mul_pos_pos;zarith. apply Zis_gcd_mod;trivial. rewrite <- H. simpl in *;destruct (ww_mod_gt_aux ah al bh bl) as [ |mh ml]. simpl;apply Zis_gcd_0;zarith. rewrite spec_compare, spec_w_0; case Z.compare_spec; intros Hmh. simpl;rewrite <- Hmh;simpl. rewrite spec_compare, spec_w_0; case Z.compare_spec; intros Hml. rewrite <- Hml;simpl;apply Zis_gcd_0. simpl; rewrite spec_w_0; simpl. apply Zis_gcd_mod. zarith. change ([|bh|] * wB + [|bl|]) with (double_to_Z w_digits w_to_Z 1 (WW bh bl)). rewrite <- (@spec_double_modn1 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 bh bl) ml Hml). apply spec_gcd_gt. rewrite (@spec_double_modn1 w w_digits w_zdigits w_0 w_WW); trivial. apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. Spec_w_to_Z ml;exfalso;lia. assert ([[WW bh bl]] > [[WW mh ml]]). rewrite H;simpl; apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. assert (H1:= spec_ww_mod_gt_aux _ _ _ H0 Hmh). assert (H3 : 0 < [[WW mh ml]]). simpl;Spec_w_to_Z ml. apply Z.lt_le_trans with ([|mh|]*wB). 2: zarith. apply Z.mul_pos_pos;zarith. apply Zis_gcd_mod. zarith. simpl in *;rewrite <- H1. destruct (ww_mod_gt_aux bh bl mh ml) as [ |rh rl]. simpl; apply Zis_gcd_0. simpl;apply Hcont. simpl in H1;rewrite H1. apply Z.lt_gt;match goal with | |- ?x mod ?y < ?y => destruct (Z_mod_lt x y);zarith end. apply Z.le_trans with (2^n/2). apply Zdiv_le_lower_bound. zarith. apply Z.le_trans with ([|bh|] * wB + [|bl|]). 2: zarith. assert (H3' := Z_div_mod_eq_full [[WW bh bl]] [[WW mh ml]]). assert (H4 : 0 <= [[WW bh bl]]/[[WW mh ml]]). apply Z.ge_le;apply Z_div_ge0;zarith. simpl in *;rewrite H1. pattern ([|bh|] * wB + [|bl|]) at 2;rewrite H3'. Z.le_elim H4. assert (H6' : [[WW bh bl]] mod [[WW mh ml]] = [[WW bh bl]] - [[WW mh ml]] * ([[WW bh bl]]/[[WW mh ml]])). simpl;pattern ([|bh|] * wB + [|bl|]) at 2;rewrite H3';ring. simpl in H6'. assert ([[WW mh ml]] <= [[WW mh ml]] * ([[WW bh bl]]/[[WW mh ml]])). simpl;pattern ([|mh|]*wB+[|ml|]) at 1;rewrite <- Z.mul_1_r;zarith. simpl in *;assert (H8 := Z_mod_lt [[WW bh bl]] [[WW mh ml]]);simpl in H8; zarith. assert (H8 := Z_mod_lt [[WW bh bl]] [[WW mh ml]]);simpl in *. lia. pattern n at 1;replace n with (n-1+1) by ring. rewrite Zpower_exp. 3: zarith. change (2^1) with 2. rewrite Z_div_mult;zarith. assert (2^1 <= 2^n). change (2^1) with 2;zarith. assert (H7 := @Zpower_le_monotone_inv 2 1 n);zarith. Spec_w_to_Z mh;exfalso;zarith. Spec_w_to_Z bh;exfalso;zarith. Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase DoubleDivn1 DoubleAdd DoubleSub