proposition: Lemma spec_kara_prod : forall xh xl yh yl hh ll, [[hh]] = [|xh|]*[|yh|] -> [[ll]] = [|xl|]*[|yl|] -> let (wc,cc) := kara_prod xh xl yh yl hh ll in [|wc|]*wwB + [[cc]] = [|xh|]*[|yl|] + [|xl|]*[|yh|].
proof: Proof. intros xh xl yh yl hh ll H H0; rewrite <- kara_prod_aux; rewrite <- H; rewrite <- H0; unfold kara_prod. assert (Hxh := (spec_to_Z xh)); assert (Hxl := (spec_to_Z xl)); assert (Hyh := (spec_to_Z yh)); assert (Hyl := (spec_to_Z yl)). generalize (spec_ww_add_c hh ll); case (ww_add_c hh ll); intros z Hz; rewrite <- Hz; unfold interp_carry; assert (Hz1 := (spec_ww_to_Z z)). rewrite spec_w_compare; case Z.compare_spec; intros Hxlh; try rewrite Hxlh; try rewrite spec_w_0; try (ring; fail). rewrite spec_w_compare; case Z.compare_spec; intros Hylh. rewrite Hylh; rewrite spec_w_0; try (ring; fail). rewrite spec_w_0; try (ring; fail). repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). split; auto with zarith. simpl in Hz; rewrite Hz; rewrite H; rewrite H0. rewrite kara_prod_aux; apply Z.add_nonneg_nonneg; apply Z.mul_nonneg_nonneg; auto with zarith. apply Z.le_lt_trans with ([[z]]-0); auto with zarith. unfold Z.sub; apply Z.add_le_mono_l; apply Z.le_0_sub; simpl; rewrite Z.opp_involutive. apply Z.mul_nonneg_nonneg; auto with zarith. match goal with |- context[ww_add_c ?x ?y] => generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_0; intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_compare; case Z.compare_spec; intros Hylh. rewrite Hylh; rewrite spec_w_0; try (ring; fail). match goal with |- context[ww_add_c ?x ?y] => generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_0; intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_1; unfold interp_carry in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_0; try (ring; fail). repeat (rewrite spec_ww_sub || rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). split. match goal with |- context[(?x - ?y) * (?z - ?t)] => replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring] end. simpl in Hz; rewrite Hz; rewrite H; rewrite H0. rewrite kara_prod_aux; apply Z.add_nonneg_nonneg; apply Z.mul_nonneg_nonneg; auto with zarith. apply Z.le_lt_trans with ([[z]]-0); auto with zarith. unfold Z.sub; apply Z.add_le_mono_l; apply Z.le_0_sub; simpl; rewrite Z.opp_involutive. apply Z.mul_nonneg_nonneg; auto with zarith. rewrite Z.mul_1_l. rewrite spec_w_compare; case Z.compare_spec; intros Hxlh; try rewrite Hxlh; try rewrite spec_w_1; try (ring; fail). rewrite spec_w_compare; case Z.compare_spec; intros Hylh; try rewrite Hylh; try rewrite spec_w_1; try (ring; fail). match goal with |- context[ww_sub_c ?x ?y] => generalize (spec_ww_sub_c x y); case (ww_sub_c x y); try rewrite spec_w_1; intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_0; rewrite Z.mul_0_l; rewrite Z.add_0_l. generalize Hz2; clear Hz2; unfold interp_carry. repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). match goal with |- context[ww_add_c ?x ?y] => generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_1; intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_2; unfold interp_carry in Hz2. transitivity (wwB + (1 * wwB + [[z1]])). ring. rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_compare; case Z.compare_spec; intros Hylh; try rewrite Hylh; try rewrite spec_w_1; try (ring; fail). match goal with |- context[ww_add_c ?x ?y] => generalize (spec_ww_add_c x y); case (ww_add_c x y); try rewrite spec_w_1; intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_2; unfold interp_carry in Hz2. transitivity (wwB + (1 * wwB + [[z1]])). ring. rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). match goal with |- context[ww_sub_c ?x ?y] => generalize (spec_ww_sub_c x y); case (ww_sub_c x y); try rewrite spec_w_1; intros z1 Hz2 end. simpl in Hz2; rewrite Hz2; repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). rewrite spec_w_0; rewrite Z.mul_0_l; rewrite Z.add_0_l. match goal with |- context[(?x - ?y) * (?z - ?t)] => replace ((x - y) * (z - t)) with ((y - x) * (t - z)); [idtac | ring] end. generalize Hz2; clear Hz2; unfold interp_carry. repeat (rewrite spec_w_sub || rewrite spec_w_mul_c). repeat rewrite Zmod_small; auto with zarith; try (ring; fail). Qed.
imports: ZArith Lia BigNumPrelude DoubleType DoubleBase