# Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleDivn1

Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Local Open Scope Z_scope.
Section GENDIVN1.
Variable w : Type.
Variable w_digits : positive.
Variable w_zdigits : w.
Variable w_0 : w.
Variable w_WW : w -> w -> zn2z w.
Variable w_head0 : w -> w.
Variable w_add_mul_div : w -> w -> w -> w.
Variable w_div21 : w -> w -> w -> w * w.
Variable w_compare : w -> w -> comparison.
Variable w_sub : w -> w -> w.
Variable w_to_Z : w -> Z.
Notation wB := (base w_digits).
Notation "[| x |]" := (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).
Notation "[[ x ]]" := (zn2z_to_Z wB w_to_Z x) (at level 0, x at level 99).
Variable spec_to_Z : forall x, 0 <= [| x |] < wB.
Variable spec_w_zdigits: [|w_zdigits|] = Zpos w_digits.
Variable spec_0 : [|w_0|] = 0.
Variable spec_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
Variable spec_head0 : forall x, 0 < [|x|] ->
wB/ 2 <= 2 ^ [|w_head0 x|] * [|x|] < wB.
Variable spec_add_mul_div : forall x y p,
[|p|] <= Zpos w_digits ->
[| w_add_mul_div p x y |] =
([|x|] * (2 ^ [|p|]) +
[|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB.
Variable spec_div21 : forall a1 a2 b,
wB/2 <= [|b|] ->
[|a1|] < [|b|] ->
let (q,r) := w_div21 a1 a2 b in
[|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|].
Variable spec_compare :
forall x y,
match w_compare x y with
| Eq => [|x|] = [|y|]
| Lt => [|x|] < [|y|]
| Gt => [|x|] > [|y|]
end.
Variable spec_sub: forall x y,
[|w_sub x y|] = ([|x|] - [|y|]) mod wB.
Section DIVAUX.
Variable b2p : w.
Variable b2p_le : wB/2 <= [|b2p|].
Definition double_divn1_0_aux n (divn1: w -> word w n -> word w n * w) r h :=
let (hh,hl) := double_split w_0 n h in
let (qh,rh) := divn1 r hh in
let (ql,rl) := divn1 rh hl in
(double_WW w_WW n qh ql, rl).
Fixpoint double_divn1_0 (n:nat) : w -> word w n -> word w n * w :=
match n return w -> word w n -> word w n * w with
| O => fun r x => w_div21 r x b2p
| S n => double_divn1_0_aux n (double_divn1_0 n)
end.
Lemma spec_split : forall (n : nat) (x : zn2z (word w n)),
let (h, l) := double_split w_0 n x in
[!S n | x!] = [!n | h!] * double_wB w_digits n + [!n | l!].
Lemma spec_double_divn1_0 : forall n r a,
[|r|] < [|b2p|] ->
let (q,r') := double_divn1_0 n r a in
[|r|] * double_wB w_digits n + [!n|a!] = [!n|q!] * [|b2p|] + [|r'|] /\
0 <= [|r'|] < [|b2p|].
Definition double_modn1_0_aux n (modn1:w -> word w n -> w) r h :=
let (hh,hl) := double_split w_0 n h in modn1 (modn1 r hh) hl.
Fixpoint double_modn1_0 (n:nat) : w -> word w n -> w :=
match n return w -> word w n -> w with
| O => fun r x => snd (w_div21 r x b2p)
| S n => double_modn1_0_aux n (double_modn1_0 n)
end.
Lemma spec_double_modn1_0 : forall n r x,
double_modn1_0 n r x = snd (double_divn1_0 n r x).
Variable p : w.
Variable p_bounded : [|p|] <= Zpos w_digits.
Lemma spec_add_mul_divp : forall x y,
[| w_add_mul_div p x y |] =
([|x|] * (2 ^ [|p|]) +
[|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB.
Definition double_divn1_p_aux n
(divn1 : w -> word w n -> word w n -> word w n * w) r h l :=
let (hh,hl) := double_split w_0 n h in
let (lh,ll) := double_split w_0 n l in
let (qh,rh) := divn1 r hh hl in
let (ql,rl) := divn1 rh hl lh in
(double_WW w_WW n qh ql, rl).
Fixpoint double_divn1_p (n:nat) : w -> word w n -> word w n -> word w n * w :=
match n return w -> word w n -> word w n -> word w n * w with
| O => fun r h l => w_div21 r (w_add_mul_div p h l) b2p
| S n => double_divn1_p_aux n (double_divn1_p n)
end.
Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (double_digits w_digits n).
Lemma spec_double_divn1_p : forall n r h l,
[|r|] < [|b2p|] ->
let (q,r') := double_divn1_p n r h l in
[|r|] * double_wB w_digits n +
([!n|h!]*2^[|p|] +
[!n|l!] / (2^(Zpos(double_digits w_digits n) - [|p|])))
mod double_wB w_digits n = [!n|q!] * [|b2p|] + [|r'|] /\
0 <= [|r'|] < [|b2p|].
Definition double_modn1_p_aux n (modn1 : w -> word w n -> word w n -> w) r h l:=
let (hh,hl) := double_split w_0 n h in
let (lh,ll) := double_split w_0 n l in
modn1 (modn1 r hh hl) hl lh.
Fixpoint double_modn1_p (n:nat) : w -> word w n -> word w n -> w :=
match n return w -> word w n -> word w n -> w with
| O => fun r h l => snd (w_div21 r (w_add_mul_div p h l) b2p)
| S n => double_modn1_p_aux n (double_modn1_p n)
end.
Lemma spec_double_modn1_p : forall n r h l ,
double_modn1_p n r h l = snd (double_divn1_p n r h l).
End DIVAUX.
Fixpoint high (n:nat) : word w n -> w :=
match n return word w n -> w with
| O => fun a => a
| S n =>
fun (a:zn2z (word w n)) =>
match a with
| W0 => w_0
| WW h l => high n h
end
end.
Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (double_digits w_digits n).
Lemma spec_high : forall n (x:word w n),
[|high n x|] = [!n|x!] / 2^(Zpos (double_digits w_digits n) - Zpos w_digits).
Definition double_divn1 (n:nat) (a:word w n) (b:w) :=
let p := w_head0 b in
match w_compare p w_0 with
| Gt =>
let b2p := w_add_mul_div p b w_0 in
let ha := high n a in
let k := w_sub w_zdigits p in
let lsr_n := w_add_mul_div k w_0 in
let r0 := w_add_mul_div p w_0 ha in
let (q,r) := double_divn1_p b2p p n r0 a (double_0 w_0 n) in
(q, lsr_n r)
| _ => double_divn1_0 b n w_0 a
end.
Lemma spec_double_divn1 : forall n a b,
0 < [|b|] ->
let (q,r) := double_divn1 n a b in
[!n|a!] = [!n|q!] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|].
Definition double_modn1 (n:nat) (a:word w n) (b:w) :=
let p := w_head0 b in
match w_compare p w_0 with
| Gt =>
let b2p := w_add_mul_div p b w_0 in
let ha := high n a in
let k := w_sub w_zdigits p in
let lsr_n := w_add_mul_div k w_0 in
let r0 := w_add_mul_div p w_0 ha in
let r := double_modn1_p b2p p n r0 a (double_0 w_0 n) in
lsr_n r
| _ => double_modn1_0 b n w_0 a
end.
Lemma spec_double_modn1_aux : forall n a b,
double_modn1 n a b = snd (double_divn1 n a b).
Lemma spec_double_modn1 : forall n a b, 0 < [|b|] ->
[|double_modn1 n a b|] = [!n|a!] mod [|b|].
End GENDIVN1.