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.