# Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleMul

Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Local Open Scope Z_scope.
Section DoubleMul.
Variable w : Type.
Variable w_0 : w.
Variable w_1 : w.
Variable w_WW : w -> w -> zn2z w.
Variable w_W0 : w -> zn2z w.
Variable w_0W : w -> zn2z w.
Variable w_compare : w -> w -> comparison.
Variable w_succ : w -> w.
Variable w_add_c : w -> w -> carry w.
Variable w_add : w -> w -> w.
Variable w_sub: w -> w -> w.
Variable w_mul_c : w -> w -> zn2z w.
Variable w_mul : w -> w -> w.
Variable w_square_c : w -> zn2z w.
Variable ww_add_c : zn2z w -> zn2z w -> carry (zn2z w).
Variable ww_add : zn2z w -> zn2z w -> zn2z w.
Variable ww_add_carry : zn2z w -> zn2z w -> zn2z w.
Variable ww_sub_c : zn2z w -> zn2z w -> carry (zn2z w).
Variable ww_sub : zn2z w -> zn2z w -> zn2z w.
Definition double_mul_c (cross:w->w->w->w->zn2z w -> zn2z w -> w * zn2z w) x y :=
match x, y with
| W0, _ => W0
| _, W0 => W0
| WW xh xl, WW yh yl =>
let hh := w_mul_c xh yh in
let ll := w_mul_c xl yl in
let (wc,cc) := cross xh xl yh yl hh ll in
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
end.
Definition ww_mul_c :=
double_mul_c
(fun xh xl yh yl hh ll=>
match ww_add_c (w_mul_c xh yl) (w_mul_c xl yh) with
| C0 cc => ( w_0 , cc )
| C1 cc => ( w_1 , cc )
end).
Definition w_2 := w_add w_1 w_1.
Definition kara_prod xh xl yh yl hh ll :=
match ww_add_c hh ll with
C0 m =>
match w_compare xl xh with
Eq => ( w_0 , m )
| Lt =>
match w_compare yl yh with
Eq => ( w_0 , m )
| Lt => ( w_0 , ww_sub m (w_mul_c (w_sub xh xl) (w_sub yh yl)))
| Gt => match ww_add_c m (w_mul_c (w_sub xh xl) (w_sub yl yh)) with
C1 m1 => ( w_1 , m1 ) | C0 m1 => ( w_0 , m1 )
end
end
| Gt =>
match w_compare yl yh with
Eq => ( w_0 , m )
| Lt => match ww_add_c m (w_mul_c (w_sub xl xh) (w_sub yh yl)) with
C1 m1 => ( w_1 , m1 ) | C0 m1 => ( w_0 , m1 )
end
| Gt => ( w_0 , ww_sub m (w_mul_c (w_sub xl xh) (w_sub yl yh)))
end
end
| C1 m =>
match w_compare xl xh with
Eq => ( w_1 , m )
| Lt =>
match w_compare yl yh with
Eq => ( w_1 , m )
| Lt => match ww_sub_c m (w_mul_c (w_sub xh xl) (w_sub yh yl)) with
C0 m1 => ( w_1 , m1 ) | C1 m1 => ( w_0 , m1 )
end
| Gt => match ww_add_c m (w_mul_c (w_sub xh xl) (w_sub yl yh)) with
C1 m1 => ( w_2 , m1 ) | C0 m1 => ( w_1 , m1 )
end
end
| Gt =>
match w_compare yl yh with
Eq => ( w_1 , m )
| Lt => match ww_add_c m (w_mul_c (w_sub xl xh) (w_sub yh yl)) with
C1 m1 => ( w_2 , m1 ) | C0 m1 => ( w_1 , m1 )
end
| Gt => match ww_sub_c m (w_mul_c (w_sub xl xh) (w_sub yl yh)) with
C1 m1 => ( w_0 , m1 ) | C0 m1 => ( w_1 , m1 )
end
end
end
end.
Definition ww_karatsuba_c := double_mul_c kara_prod.
Definition ww_mul x y :=
match x, y with
| W0, _ => W0
| _, W0 => W0
| WW xh xl, WW yh yl =>
let ccl := w_add (w_mul xh yl) (w_mul xl yh) in
ww_add (w_W0 ccl) (w_mul_c xl yl)
end.
Definition ww_square_c x :=
match x with
| W0 => W0
| WW xh xl =>
let hh := w_square_c xh in
let ll := w_square_c xl in
let xhxl := w_mul_c xh xl in
let (wc,cc) :=
match ww_add_c xhxl xhxl with
| C0 cc => ( w_0 , cc )
| C1 cc => ( w_1 , cc )
end in
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
end.
Section DoubleMulAddn1.
Variable w_mul_add : w -> w -> w -> w * w.
Fixpoint double_mul_add_n1 (n:nat) : word w n -> w -> w -> w * word w n :=
match n return word w n -> w -> w -> w * word w n with
| O => w_mul_add
| S n1 =>
let mul_add := double_mul_add_n1 n1 in
fun x y r =>
match x with
| W0 => ( w_0 , extend w_0W n1 r )
| WW xh xl =>
let (rl,l) := mul_add xl y r in
let (rh,h) := mul_add xh y rl in
( rh , double_WW w_WW n1 h l )
end
end.
End DoubleMulAddn1.
Section DoubleMulAddmn1.
Variable wn: Type.
Variable extend_n : w -> wn.
Variable wn_0W : wn -> zn2z wn.
Variable wn_WW : wn -> wn -> zn2z wn.
Variable w_mul_add_n1 : wn -> w -> w -> w * wn.
Fixpoint double_mul_add_mn1 (m:nat) :
word wn m -> w -> w -> w * word wn m :=
match m return word wn m -> w -> w -> w * word wn m with
| O => w_mul_add_n1
| S m1 =>
let mul_add := double_mul_add_mn1 m1 in
fun x y r =>
match x with
| W0 => ( w_0 , extend wn_0W m1 (extend_n r))
| WW xh xl =>
let (rl,l) := mul_add xl y r in
let (rh,h) := mul_add xh y rl in
( rh , double_WW wn_WW m1 h l )
end
end.
End DoubleMulAddmn1.
Definition w_mul_add x y r :=
match w_mul_c x y with
| W0 => ( w_0 , r )
| WW h l =>
match w_add_c l r with
| C0 lr => ( h , lr )
| C1 lr => ( w_succ h , lr )
end
end.
Variable w_digits : positive.
Variable w_to_Z : w -> Z.
Notation wB := (base w_digits).
Notation wwB := (base (ww_digits w_digits)).
Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99).
Notation "[+| c |]" :=
(interp_carry 1 wB w_to_Z c) (at level 0, x at level 99).
Notation "[-| c |]" :=
(interp_carry (-1) wB w_to_Z c) (at level 0, x at level 99).
Notation "[[ x ]]" := (ww_to_Z w_digits w_to_Z x)(at level 0, x at level 99).
Notation "[+[ c ]]" :=
(interp_carry 1 wwB (ww_to_Z w_digits w_to_Z) c)
(at level 0, x at level 99).
Notation "[-[ c ]]" :=
(interp_carry (-1) wwB (ww_to_Z w_digits w_to_Z) c)
(at level 0, x at level 99).
Notation "[|| x ||]" :=
(zn2z_to_Z wwB (ww_to_Z w_digits w_to_Z) x) (at level 0, x at level 99).
Notation "[! n | x !]" := (double_to_Z w_digits w_to_Z n x)
(at level 0, x at level 99).
Variable spec_more_than_1_digit: 1 < Zpos w_digits.
Variable spec_w_0 : [| w_0 |] = 0.
Variable spec_w_1 : [| w_1 |] = 1.
Variable spec_to_Z : forall x, 0 <= [| x |] < wB.
Variable spec_w_WW : forall h l, [[ w_WW h l ]] = [| h |] * wB + [| l |].
Variable spec_w_W0 : forall h, [[ w_W0 h ]] = [| h |] * wB.
Variable spec_w_0W : forall l, [[ w_0W l ]] = [| l |].
Variable spec_w_compare :
forall x y,
match w_compare x y with
| Eq => [| x |] = [| y |]
| Lt => [| x |] < [| y |]
| Gt => [| x |] > [| y |]
end.
Variable spec_w_succ : forall x, [| w_succ x |] = ( [| x |] + 1) mod wB.
Variable spec_w_add_c : forall x y, [+| w_add_c x y |] = [| x |] + [| y |].
Variable spec_w_add : forall x y, [| w_add x y |] = ( [| x |] + [| y |] ) mod wB.
Variable spec_w_sub : forall x y, [| w_sub x y |] = ( [| x |] - [| y |] ) mod wB.
Variable spec_w_mul_c : forall x y, [[ w_mul_c x y ]] = [| x |] * [| y |].
Variable spec_w_mul : forall x y, [| w_mul x y |] = ( [| x |] * [| y |] ) mod wB.
Variable spec_w_square_c : forall x, [[ w_square_c x ]] = [| x |] * [| x |].
Variable spec_ww_add_c : forall x y, [+[ ww_add_c x y ]] = [[ x ]] + [[ y ]].
Variable spec_ww_add : forall x y, [[ ww_add x y ]] = ( [[ x ]] + [[ y ]] ) mod wwB.
Variable spec_ww_add_carry :
forall x y, [[ ww_add_carry x y ]] = ( [[ x ]] + [[ y ]] + 1) mod wwB.
Variable spec_ww_sub : forall x y, [[ ww_sub x y ]] = ( [[ x ]] - [[ y ]] ) mod wwB.
Variable spec_ww_sub_c : forall x y, [-[ ww_sub_c x y ]] = [[ x ]] - [[ y ]].
Lemma spec_ww_to_Z : forall x, 0 <= [[ x ]] < wwB.
Lemma spec_ww_to_Z_wBwB : forall x, 0 <= [[ x ]] < wB ^2.
Hint Resolve spec_ww_to_Z spec_ww_to_Z_wBwB : mult.
Ltac zarith := auto with zarith mult.
Lemma wBwB_lex: forall a b c d,
a * wB ^2 + [[ b ]] <= c * wB ^2 + [[ d ]] ->
a <= c.
Lemma wBwB_lex_inv: forall a b c d,
a < c ->
a * wB ^2 + [[ b ]] < c * wB ^2 + [[ d ]].
Lemma sum_mul_carry : forall xh xl yh yl wc cc,
[| wc |] * wB ^2 + [[ cc ]] = [| xh |] * [| yl |] + [| xl |] * [| yh |] ->
0 <= [| wc |] <= 1.
Theorem mult_add_ineq: forall xH yH crossH,
0 <= [| xH |] * [| yH |] + [| crossH |] < wwB.
Hint Resolve mult_add_ineq : mult.
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 |] ).
Lemma spec_double_mul_c : forall cross:w->w->w->w->zn2z w -> zn2z w -> w * zn2z w,
(forall xh xl yh yl hh ll,
[[ hh ]] = [| xh |] * [| yh |] ->
[[ ll ]] = [| xl |] * [| yl |] ->
let (wc,cc) := cross xh xl yh yl hh ll in
[| wc |] * wwB + [[ cc ]] = [| xh |] * [| yl |] + [| xl |] * [| yh |]) ->
forall x y, [|| double_mul_c cross x y ||] = [[ x ]] * [[ y ]].
Lemma spec_ww_mul_c : forall x y, [|| ww_mul_c x y ||] = [[ x ]] * [[ y ]].
Lemma spec_w_2: [| w_2 |] = 2.
Lemma kara_prod_aux : forall xh xl yh yl,
xh * yh + xl * yl - ( xh - xl )*( yh - yl ) = xh * yl + xl * yh.
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 |].
there is a carry in hh + ll
Lemma sub_carry : forall xh xl yh yl z,
0 <= z ->
[| xh |] * [| yl |] + [| xl |] * [| yh |] = wwB + z ->
z < wwB.
Ltac Spec_ww_to_Z x :=
let H:= fresh "H" in
assert (H:= spec_ww_to_Z x).
Ltac Zmult_lt_b x y :=
let H := fresh "H" in
assert (H := Zmult_lt_b _ _ _ (spec_to_Z x) (spec_to_Z y)).
Lemma spec_ww_karatsuba_c : forall x y, [|| ww_karatsuba_c x y ||] = [[ x ]] * [[ y ]].
Lemma spec_ww_mul : forall x y, [[ ww_mul x y ]] = [[ x ]] * [[ y ]] mod wwB.
Lemma spec_ww_square_c : forall x, [|| ww_square_c x ||] = [[ x ]] * [[ x ]].
Section DoubleMulAddn1Proof.
Variable w_mul_add : w -> w -> w -> w * w.
Variable spec_w_mul_add : forall x y r,
let (h,l):= w_mul_add x y r in
[| h |] * wB + [| l |] = [| x |] * [| y |] + [| r |].
Lemma spec_double_mul_add_n1 : forall n x y r,
let (h,l) := double_mul_add_n1 w_mul_add n x y r in
[| h |] * double_wB w_digits n + [! n | l !] = [! n | x !] * [| y |] + [| r |].
End DoubleMulAddn1Proof.
Lemma spec_w_mul_add : forall x y r,
let (h,l):= w_mul_add x y r in
[| h |] * wB + [| l |] = [| x |] * [| y |] + [| r |].
End DoubleMul.