# Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleDivn1

Set Implicit Arguments.
Require Import ZArith Ndigits.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Local Open Scope Z_scope.
Local Infix "<<" := Pos.shiftl_nat (at level 30).
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, w_compare x y = Z.compare [| x |] [| y |].
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 (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(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 (w_digits << n).
Lemma spec_high : forall n (x:word w n),
[| high n x |] = [! n | x !] / 2^( Zpos (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.