Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Require Import DoubleDivn1.
Require Import DoubleAdd.
Require Import DoubleSub.
Open Local Scope Z_scope.
Ltac zarith :=
auto with zarith.
Section POS_MOD.
Variable w:Type.
Variable w_0 :
w.
Variable w_digits :
positive.
Variable w_zdigits :
w.
Variable w_WW :
w ->
w ->
zn2z w.
Variable w_pos_mod :
w ->
w ->
w.
Variable w_compare :
w ->
w ->
comparison.
Variable ww_compare :
zn2z w ->
zn2z w ->
comparison.
Variable w_0W :
w ->
zn2z w.
Variable low:
zn2z w ->
w.
Variable ww_sub:
zn2z w ->
zn2z w ->
zn2z w.
Variable ww_zdigits :
zn2z w.
Definition ww_pos_mod p x :=
let zdigits :=
w_0W w_zdigits in
match x with
|
W0 =>
W0
|
WW xh xl =>
match ww_compare p zdigits with
|
Eq =>
w_WW w_0 xl
|
Lt =>
w_WW w_0 (
w_pos_mod (
low p)
xl)
|
Gt =>
match ww_compare p ww_zdigits with
|
Lt =>
let n :=
low (
ww_sub p zdigits)
in
w_WW (
w_pos_mod n xh)
xl
|
_ =>
x
end
end
end.
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 "[[ x ]]" := (
ww_to_Z w_digits w_to_Z x)(
at level 0,
x at level 99).
Variable spec_w_0 : [|w_0|] = 0.
Variable spec_to_Z :
forall x, 0 <= [|x|] <
wB.
Variable spec_to_w_Z :
forall x, 0 <= [[
x]] <
wwB.
Variable spec_w_WW :
forall h l, [[
w_WW h l]] = [|h|] *
wB + [|l|].
Variable spec_pos_mod :
forall w p,
[|w_pos_mod
p w|] = [|w|]
mod (2 ^ [|p|]).
Variable spec_w_0W :
forall l, [[
w_0W l]] = [|l|].
Variable spec_ww_compare :
forall x y,
match ww_compare x y with
|
Eq => [[
x]] = [[
y]]
|
Lt => [[
x]] < [[
y]]
|
Gt => [[
x]] > [[
y]]
end.
Variable spec_ww_sub:
forall x y,
[[
ww_sub x y]] = ([[
x]] - [[
y]])
mod wwB.
Variable spec_zdigits : [|
w_zdigits |] =
Zpos w_digits.
Variable spec_low:
forall x, [|
low x|] = [[
x]]
mod wB.
Variable spec_ww_zdigits : [[
ww_zdigits]] = 2 * [|w_zdigits|].
Variable spec_ww_digits :
ww_digits w_digits =
xO w_digits.
Hint Rewrite spec_w_0 spec_w_WW :
w_rewrite.
Lemma spec_ww_pos_mod :
forall w p,
[[
ww_pos_mod p w]] = [[
w]]
mod (2 ^ [[
p]]).
End POS_MOD.
Section DoubleDiv32.
Variable w :
Type.
Variable w_0 :
w.
Variable w_Bm1 :
w.
Variable w_Bm2 :
w.
Variable w_WW :
w ->
w ->
zn2z w.
Variable w_compare :
w ->
w ->
comparison.
Variable w_add_c :
w ->
w ->
carry w.
Variable w_add_carry_c :
w ->
w ->
carry w.
Variable w_add :
w ->
w ->
w.
Variable w_add_carry :
w ->
w ->
w.
Variable w_pred :
w ->
w.
Variable w_sub :
w ->
w ->
w.
Variable w_mul_c :
w ->
w ->
zn2z w.
Variable w_div21 :
w ->
w ->
w ->
w*w.
Variable ww_sub_c :
zn2z w ->
zn2z w ->
carry (
zn2z w).
Definition w_div32 a1 a2 a3 b1 b2 :=
Eval lazy beta iota delta [
ww_add_c_cont ww_add]
in
match w_compare a1 b1 with
|
Lt =>
let (
q,r) :=
w_div21 a1 a2 b1 in
match ww_sub_c (
w_WW r a3) (
w_mul_c q b2)
with
|
C0 r1 => (
q,r1)
|
C1 r1 =>
let q :=
w_pred q in
ww_add_c_cont w_WW w_add_c w_add_carry_c
(
fun r2=>(w_pred
q,
ww_add w_add_c w_add w_add_carry r2 (
WW b1 b2)))
(
fun r2 => (
q,r2))
r1 (
WW b1 b2)
end
|
Eq =>
ww_add_c_cont w_WW w_add_c w_add_carry_c
(
fun r => (
w_Bm2,
ww_add w_add_c w_add w_add_carry r (
WW b1 b2)))
(
fun r => (
w_Bm1,r))
(
WW (
w_sub a2 b2)
a3) (
WW b1 b2)
|
Gt => (
w_0,
W0)
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).
Variable spec_w_0 : [|w_0|] = 0.
Variable spec_w_Bm1 : [|w_Bm1|] =
wB - 1.
Variable spec_w_Bm2 : [|w_Bm2|] =
wB - 2.
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_compare :
forall x y,
match w_compare x y with
|
Eq => [|x|] = [|y|]
|
Lt => [|x|] < [|y|]
|
Gt => [|x|] > [|y|]
end.
Variable spec_w_add_c :
forall x y, [+|w_add_c
x y|] = [|x|] + [|y|].
Variable spec_w_add_carry_c :
forall x y, [+|w_add_carry_c
x y|] = [|x|] + [|y|] + 1.
Variable spec_w_add :
forall x y, [|w_add
x y|] = ([|x|] + [|y|])
mod wB.
Variable spec_w_add_carry :
forall x y, [|w_add_carry
x y|] = ([|x|] + [|y|] + 1)
mod wB.
Variable spec_pred :
forall x, [|w_pred
x|] = ([|x|] - 1)
mod wB.
Variable spec_sub :
forall x y, [|w_sub
x y|] = ([|x|] - [|y|])
mod wB.
Variable spec_mul_c :
forall x y, [[
w_mul_c x y ]] = [|x|] * [|y|].
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_ww_sub_c :
forall x y, [-[
ww_sub_c x y]] = [[
x]] - [[
y]].
Ltac Spec_w_to_Z x :=
let H:=
fresh "HH"
in
assert (
H:=
spec_to_Z x).
Ltac Spec_ww_to_Z x :=
let H:=
fresh "HH"
in
assert (
H:=
spec_ww_to_Z w_digits w_to_Z spec_to_Z x).
Theorem wB_div2:
forall x,
wB/2 <=
x ->
wB <= 2 *
x.
Lemma Zmult_lt_0_reg_r_2 :
forall n m :
Z, 0 <=
n -> 0 <
m *
n -> 0 <
m.
Theorem spec_w_div32 :
forall a1 a2 a3 b1 b2,
wB/2 <= [|b1|] ->
[[
WW a1 a2]] < [[
WW b1 b2]] ->
let (
q,r) :=
w_div32 a1 a2 a3 b1 b2 in
[|a1|] *
wwB + [|a2|] *
wB + [|a3|] =
[|q|] * ([|b1|] *
wB + [|b2|]) + [[
r]] /\
0 <= [[
r]] < [|b1|] *
wB + [|b2|].
End DoubleDiv32.
Section DoubleDiv21.
Variable w :
Type.
Variable w_0 :
w.
Variable w_0W :
w ->
zn2z w.
Variable w_div32 :
w ->
w ->
w ->
w ->
w ->
w *
zn2z w.
Variable ww_1 :
zn2z w.
Variable ww_compare :
zn2z w ->
zn2z w ->
comparison.
Variable ww_sub :
zn2z w ->
zn2z w ->
zn2z w.
Definition ww_div21 a1 a2 b :=
match a1 with
|
W0 =>
match ww_compare a2 b with
|
Gt => (
ww_1,
ww_sub a2 b)
|
Eq => (
ww_1,
W0)
|
Lt => (
W0,
a2)
end
|
WW a1h a1l =>
match a2 with
|
W0 =>
match b with
|
W0 => (
W0,W0)
|
WW b1 b2 =>
let (
q1,
r) :=
w_div32 a1h a1l w_0 b1 b2 in
match r with
|
W0 => (
WW q1 w_0,
W0)
|
WW r1 r2 =>
let (
q2,
s) :=
w_div32 r1 r2 w_0 b1 b2 in
(
WW q1 q2,
s)
end
end
|
WW a2h a2l =>
match b with
|
W0 => (
W0,W0)
|
WW b1 b2 =>
let (
q1,
r) :=
w_div32 a1h a1l a2h b1 b2 in
match r with
|
W0 => (
WW q1 w_0,
w_0W a2l)
|
WW r1 r2 =>
let (
q2,
s) :=
w_div32 r1 r2 a2l b1 b2 in
(
WW q1 q2,
s)
end
end
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 "[[ 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).
Variable spec_w_0 : [|w_0|] = 0.
Variable spec_to_Z :
forall x, 0 <= [|x|] <
wB.
Variable spec_w_0W :
forall l, [[
w_0W l]] = [|l|].
Variable spec_w_div32 :
forall a1 a2 a3 b1 b2,
wB/2 <= [|b1|] ->
[[
WW a1 a2]] < [[
WW b1 b2]] ->
let (
q,r) :=
w_div32 a1 a2 a3 b1 b2 in
[|a1|] *
wwB + [|a2|] *
wB + [|a3|] =
[|q|] * ([|b1|] *
wB + [|b2|]) + [[
r]] /\
0 <= [[
r]] < [|b1|] *
wB + [|b2|].
Variable spec_ww_1 : [[
ww_1]] = 1.
Variable spec_ww_compare :
forall x y,
match ww_compare x y with
|
Eq => [[
x]] = [[
y]]
|
Lt => [[
x]] < [[
y]]
|
Gt => [[
x]] > [[
y]]
end.
Variable spec_ww_sub :
forall x y, [[
ww_sub x y]] = ([[
x]] - [[
y]])
mod wwB.
Theorem wwB_div:
wwB = 2 * (
wwB / 2).
Ltac Spec_w_to_Z x :=
let H:=
fresh "HH"
in
assert (
H:=
spec_to_Z x).
Ltac Spec_ww_to_Z x :=
let H:=
fresh "HH"
in
assert (
H:=
spec_ww_to_Z w_digits w_to_Z spec_to_Z x).
Theorem spec_ww_div21 :
forall a1 a2 b,
wwB/2 <= [[
b]] ->
[[
a1]] < [[
b]] ->
let (
q,r) :=
ww_div21 a1 a2 b in
[[
a1]] *wwB+[[
a2]] = [[
q]] * [[
b]] + [[
r]] /\ 0 <= [[
r]] < [[
b]].
End DoubleDiv21.
Section DoubleDivGt.
Variable w :
Type.
Variable w_digits :
positive.
Variable w_0 :
w.
Variable w_WW :
w ->
w ->
zn2z w.
Variable w_0W :
w ->
zn2z w.
Variable w_compare :
w ->
w ->
comparison.
Variable w_eq0 :
w ->
bool.
Variable w_opp_c :
w ->
carry w.
Variable w_opp w_opp_carry :
w ->
w.
Variable w_sub_c :
w ->
w ->
carry w.
Variable w_sub w_sub_carry :
w ->
w ->
w.
Variable w_div_gt :
w ->
w ->
w*w.
Variable w_mod_gt :
w ->
w ->
w.
Variable w_gcd_gt :
w ->
w ->
w.
Variable w_add_mul_div :
w ->
w ->
w ->
w.
Variable w_head0 :
w ->
w.
Variable w_div21 :
w ->
w ->
w ->
w *
w.
Variable w_div32 :
w ->
w ->
w ->
w ->
w ->
w *
zn2z w.
Variable _ww_zdigits :
zn2z w.
Variable ww_1 :
zn2z w.
Variable ww_add_mul_div :
zn2z w ->
zn2z w ->
zn2z w ->
zn2z w.
Variable w_zdigits :
w.
Definition ww_div_gt_aux ah al bh bl :=
Eval lazy beta iota delta [
ww_sub ww_opp]
in
let p :=
w_head0 bh in
match w_compare p w_0 with
|
Gt =>
let b1 :=
w_add_mul_div p bh bl in
let b2 :=
w_add_mul_div p bl w_0 in
let a1 :=
w_add_mul_div p w_0 ah in
let a2 :=
w_add_mul_div p ah al in
let a3 :=
w_add_mul_div p al w_0 in
let (
q,r) :=
w_div32 a1 a2 a3 b1 b2 in
(
WW w_0 q,
ww_add_mul_div
(
ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
w_opp w_sub w_sub_carry _ww_zdigits (
w_0W p))
W0 r)
|
_ => (
ww_1,
ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
w_opp w_sub w_sub_carry (
WW ah al) (
WW bh bl))
end.
Definition ww_div_gt a b :=
Eval lazy beta iota delta [
ww_div_gt_aux double_divn1
double_divn1_p double_divn1_p_aux double_divn1_0 double_divn1_0_aux
double_split double_0 double_WW]
in
match a,
b with
|
W0,
_ => (
W0,W0)
|
_,
W0 => (
W0,W0)
|
WW ah al,
WW bh bl =>
if w_eq0 ah then
let (
q,r) :=
w_div_gt al bl in
(
WW w_0 q,
w_0W r)
else
match w_compare w_0 bh with
|
Eq =>
let(
q,r):=
double_divn1 w_zdigits w_0 w_WW w_head0 w_add_mul_div w_div21
w_compare w_sub 1
a bl in
(
q,
w_0W r)
|
Lt =>
ww_div_gt_aux ah al bh bl
|
Gt => (
W0,W0)
end
end.
Definition ww_mod_gt_aux ah al bh bl :=
Eval lazy beta iota delta [
ww_sub ww_opp]
in
let p :=
w_head0 bh in
match w_compare p w_0 with
|
Gt =>
let b1 :=
w_add_mul_div p bh bl in
let b2 :=
w_add_mul_div p bl w_0 in
let a1 :=
w_add_mul_div p w_0 ah in
let a2 :=
w_add_mul_div p ah al in
let a3 :=
w_add_mul_div p al w_0 in
let (
q,r) :=
w_div32 a1 a2 a3 b1 b2 in
ww_add_mul_div (
ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
w_opp w_sub w_sub_carry _ww_zdigits (
w_0W p))
W0 r
|
_ =>
ww_sub w_0 w_WW w_opp_c w_opp_carry w_sub_c
w_opp w_sub w_sub_carry (
WW ah al) (
WW bh bl)
end.
Definition ww_mod_gt a b :=
Eval lazy beta iota delta [
ww_mod_gt_aux double_modn1
double_modn1_p double_modn1_p_aux double_modn1_0 double_modn1_0_aux
double_split double_0 double_WW snd]
in
match a,
b with
|
W0,
_ =>
W0
|
_,
W0 =>
W0
|
WW ah al,
WW bh bl =>
if w_eq0 ah then w_0W (
w_mod_gt al bl)
else
match w_compare w_0 bh with
|
Eq =>
w_0W (
double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
w_compare w_sub 1
a bl)
|
Lt =>
ww_mod_gt_aux ah al bh bl
|
Gt =>
W0
end
end.
Definition ww_gcd_gt_body (
cont:
w->w->w->w->zn2
z w) (
ah al bh bl:
w) :=
Eval lazy beta iota delta [
ww_mod_gt_aux double_modn1
double_modn1_p double_modn1_p_aux double_modn1_0 double_modn1_0_aux
double_split double_0 double_WW snd]
in
match w_compare w_0 bh with
|
Eq =>
match w_compare w_0 bl with
|
Eq =>
WW ah al
|
Lt =>
let m :=
double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
w_compare w_sub 1 (
WW ah al)
bl in
WW w_0 (
w_gcd_gt bl m)
|
Gt =>
W0
end
|
Lt =>
let m :=
ww_mod_gt_aux ah al bh bl in
match m with
|
W0 =>
WW bh bl
|
WW mh ml =>
match w_compare w_0 mh with
|
Eq =>
match w_compare w_0 ml with
|
Eq =>
WW bh bl
|
_ =>
let r :=
double_modn1 w_zdigits w_0 w_head0 w_add_mul_div w_div21
w_compare w_sub 1 (
WW bh bl)
ml in
WW w_0 (
w_gcd_gt ml r)
end
|
Lt =>
let r :=
ww_mod_gt_aux bh bl mh ml in
match r with
|
W0 =>
m
|
WW rh rl =>
cont mh ml rh rl
end
|
Gt =>
W0
end
end
|
Gt =>
W0
end.
Fixpoint ww_gcd_gt_aux
(
p:positive) (
cont:
w ->
w ->
w ->
w ->
zn2z w) (
ah al bh bl :
w)
{
struct p} :
zn2z w :=
ww_gcd_gt_body
(
fun mh ml rh rl =>
match p with
|
xH =>
cont mh ml rh rl
|
xO p =>
ww_gcd_gt_aux p (
ww_gcd_gt_aux p cont)
mh ml rh rl
|
xI p =>
ww_gcd_gt_aux p (
ww_gcd_gt_aux p cont)
mh ml rh rl
end)
ah al bh bl.
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 "[[ x ]]" := (
ww_to_Z w_digits w_to_Z x)(
at level 0,
x at level 99).
Variable spec_w_0 : [|w_0|] = 0.
Variable spec_to_Z :
forall x, 0 <= [|x|] <
wB.
Variable spec_to_w_Z :
forall x, 0 <= [[
x]] <
wwB.
Variable spec_w_WW :
forall h l, [[
w_WW h l]] = [|h|] *
wB + [|l|].
Variable spec_w_0W :
forall l, [[
w_0W l]] = [|l|].
Variable spec_compare :
forall x y,
match w_compare x y with
|
Eq => [|x|] = [|y|]
|
Lt => [|x|] < [|y|]
|
Gt => [|x|] > [|y|]
end.
Variable spec_eq0 :
forall x,
w_eq0 x =
true -> [|x|] = 0.
Variable spec_opp_c :
forall x, [-|w_opp_c
x|] = -[|x|].
Variable spec_opp :
forall x, [|w_opp
x|] = (-[|x|])
mod wB.
Variable spec_opp_carry :
forall x, [|w_opp_carry
x|] =
wB - [|x|] - 1.
Variable spec_sub_c :
forall x y, [-|w_sub_c
x y|] = [|x|] - [|y|].
Variable spec_sub :
forall x y, [|w_sub
x y|] = ([|x|] - [|y|])
mod wB.
Variable spec_sub_carry :
forall x y, [|w_sub_carry
x y|] = ([|x|] - [|y|] - 1)
mod wB.
Variable spec_div_gt :
forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
let (
q,r) :=
w_div_gt a b in
[|a|] = [|q|] * [|b|] + [|r|] /\
0 <= [|r|] < [|b|].
Variable spec_mod_gt :
forall a b, [|a|] > [|b|] -> 0 < [|b|] ->
[|w_mod_gt
a b|] = [|a|]
mod [|b|].
Variable spec_gcd_gt :
forall a b, [|a|] > [|b|] ->
Zis_gcd [|a|] [|b|] [|w_gcd_gt
a b|].
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_head0 :
forall x, 0 < [|x|] ->
wB/ 2 <= 2 ^ [|w_head0
x|] * [|x|] <
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_w_div32 :
forall a1 a2 a3 b1 b2,
wB/2 <= [|b1|] ->
[[
WW a1 a2]] < [[
WW b1 b2]] ->
let (
q,r) :=
w_div32 a1 a2 a3 b1 b2 in
[|a1|] *
wwB + [|a2|] *
wB + [|a3|] =
[|q|] * ([|b1|] *
wB + [|b2|]) + [[
r]] /\
0 <= [[
r]] < [|b1|] *
wB + [|b2|].
Variable spec_w_zdigits: [|w_zdigits|] =
Zpos w_digits.
Variable spec_ww_digits_ : [[
_ww_zdigits]] =
Zpos (
xO w_digits).
Variable spec_ww_1 : [[
ww_1]] = 1.
Variable spec_ww_add_mul_div :
forall x y p,
[[
p]] <=
Zpos (
xO w_digits) ->
[[
ww_add_mul_div p x y ]] =
([[
x]] * (2^[[
p]]) +
[[
y]] / (2^(Zpos (
xO w_digits) - [[
p]])))
mod wwB.
Ltac Spec_w_to_Z x :=
let H:=
fresh "HH"
in
assert (
H:=
spec_to_Z x).
Ltac Spec_ww_to_Z x :=
let H:=
fresh "HH"
in
assert (
H:=
spec_ww_to_Z w_digits w_to_Z spec_to_Z x).
Lemma to_Z_div_minus_p :
forall x p,
0 < [|p|] <
Zpos w_digits ->
0 <= [|x|] / 2 ^ (
Zpos w_digits - [|p|]) < 2 ^ [|p|].
Hint Resolve to_Z_div_minus_p :
zarith.
Lemma spec_ww_div_gt_aux :
forall ah al bh bl,
[[
WW ah al]] > [[
WW bh bl]] ->
0 < [|bh|] ->
let (
q,r) :=
ww_div_gt_aux ah al bh bl in
[[
WW ah al]] = [[
q]] * [[
WW bh bl]] + [[
r]] /\
0 <= [[
r]] < [[
WW bh bl]].
Lemma spec_ww_div_gt :
forall a b, [[
a]] > [[
b]] -> 0 < [[
b]] ->
let (
q,r) :=
ww_div_gt a b in
[[
a]] = [[
q]] * [[
b]] + [[
r]] /\
0 <= [[
r]] < [[
b]].
Lemma spec_ww_mod_gt_aux_eq :
forall ah al bh bl,
ww_mod_gt_aux ah al bh bl =
snd (
ww_div_gt_aux ah al bh bl).
Lemma spec_ww_mod_gt_aux :
forall ah al bh bl,
[[
WW ah al]] > [[
WW bh bl]] ->
0 < [|bh|] ->
[[
ww_mod_gt_aux ah al bh bl]] = [[
WW ah al]]
mod [[
WW bh bl]].
Lemma spec_w_mod_gt_eq :
forall a b, [|a|] > [|b|] -> 0 <[|b|] ->
[|w_mod_gt
a b|] = [|snd (
w_div_gt a b)|].
Lemma spec_ww_mod_gt_eq :
forall a b, [[
a]] > [[
b]] -> 0 < [[
b]] ->
[[
ww_mod_gt a b]] = [[
snd (
ww_div_gt a b)]].
Lemma spec_ww_mod_gt :
forall a b, [[
a]] > [[
b]] -> 0 < [[
b]] ->
[[
ww_mod_gt a b]] = [[
a]]
mod [[
b]].
Lemma Zis_gcd_mod :
forall a b d,
0 <
b ->
Zis_gcd b (
a mod b)
d ->
Zis_gcd a b d.
Lemma spec_ww_gcd_gt_aux_body :
forall ah al bh bl n cont,
[[
WW bh bl]] <= 2^n ->
[[
WW ah al]] > [[
WW bh bl]] ->
(
forall xh xl yh yl,
[[
WW xh xl]] > [[
WW yh yl]] -> [[
WW yh yl]] <= 2^(n-1) ->
Zis_gcd [[
WW xh xl]] [[
WW yh yl]] [[
cont xh xl yh yl]]) ->
Zis_gcd [[
WW ah al]] [[
WW bh bl]] [[
ww_gcd_gt_body cont ah al bh bl]].
Lemma spec_ww_gcd_gt_aux :
forall p cont n,
(
forall xh xl yh yl,
[[
WW xh xl]] > [[
WW yh yl]] ->
[[
WW yh yl]] <= 2^n ->
Zis_gcd [[
WW xh xl]] [[
WW yh yl]] [[
cont xh xl yh yl]]) ->
forall ah al bh bl , [[
WW ah al]] > [[
WW bh bl]] ->
[[
WW bh bl]] <= 2^(Zpos
p +
n) ->
Zis_gcd [[
WW ah al]] [[
WW bh bl]]
[[
ww_gcd_gt_aux p cont ah al bh bl]].
End DoubleDivGt.
Section DoubleDiv.
Variable w :
Type.
Variable w_digits :
positive.
Variable ww_1 :
zn2z w.
Variable ww_compare :
zn2z w ->
zn2z w ->
comparison.
Variable ww_div_gt :
zn2z w ->
zn2z w ->
zn2z w *
zn2z w.
Variable ww_mod_gt :
zn2z w ->
zn2z w ->
zn2z w.
Definition ww_div a b :=
match ww_compare a b with
|
Gt =>
ww_div_gt a b
|
Eq => (
ww_1,
W0)
|
Lt => (
W0,
a)
end.
Definition ww_mod a b :=
match ww_compare a b with
|
Gt =>
ww_mod_gt a b
|
Eq =>
W0
|
Lt =>
a
end.
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 "[[ x ]]" := (
ww_to_Z w_digits w_to_Z x)(
at level 0,
x at level 99).
Variable spec_to_Z :
forall x, 0 <= [|x|] <
wB.
Variable spec_ww_1 : [[
ww_1]] = 1.
Variable spec_ww_compare :
forall x y,
match ww_compare x y with
|
Eq => [[
x]] = [[
y]]
|
Lt => [[
x]] < [[
y]]
|
Gt => [[
x]] > [[
y]]
end.
Variable spec_ww_div_gt :
forall a b, [[
a]] > [[
b]] -> 0 < [[
b]] ->
let (
q,r) :=
ww_div_gt a b in
[[
a]] = [[
q]] * [[
b]] + [[
r]] /\
0 <= [[
r]] < [[
b]].
Variable spec_ww_mod_gt :
forall a b, [[
a]] > [[
b]] -> 0 < [[
b]] ->
[[
ww_mod_gt a b]] = [[
a]]
mod [[
b]].
Ltac Spec_w_to_Z x :=
let H:=
fresh "HH"
in
assert (
H:=
spec_to_Z x).
Ltac Spec_ww_to_Z x :=
let H:=
fresh "HH"
in
assert (
H:=
spec_ww_to_Z w_digits w_to_Z spec_to_Z x).
Lemma spec_ww_div :
forall a b, 0 < [[
b]] ->
let (
q,r) :=
ww_div a b in
[[
a]] = [[
q]] * [[
b]] + [[
r]] /\
0 <= [[
r]] < [[
b]].
Lemma spec_ww_mod :
forall a b, 0 < [[
b]] ->
[[
ww_mod a b]] = [[
a]]
mod [[
b]].
Variable w_0 :
w.
Variable w_1 :
w.
Variable w_compare :
w ->
w ->
comparison.
Variable w_eq0 :
w ->
bool.
Variable w_gcd_gt :
w ->
w ->
w.
Variable _ww_digits :
positive.
Variable spec_ww_digits_ :
_ww_digits =
xO w_digits.
Variable ww_gcd_gt_fix :
positive -> (
w ->
w ->
w ->
w ->
zn2z w) ->
w ->
w ->
w ->
w ->
zn2z w.
Variable spec_w_0 : [|w_0|] = 0.
Variable spec_w_1 : [|w_1|] = 1.
Variable spec_compare :
forall x y,
match w_compare x y with
|
Eq => [|x|] = [|y|]
|
Lt => [|x|] < [|y|]
|
Gt => [|x|] > [|y|]
end.
Variable spec_eq0 :
forall x,
w_eq0 x =
true -> [|x|] = 0.
Variable spec_gcd_gt :
forall a b, [|a|] > [|b|] ->
Zis_gcd [|a|] [|b|] [|w_gcd_gt
a b|].
Variable spec_gcd_gt_fix :
forall p cont n,
(
forall xh xl yh yl,
[[
WW xh xl]] > [[
WW yh yl]] ->
[[
WW yh yl]] <= 2^n ->
Zis_gcd [[
WW xh xl]] [[
WW yh yl]] [[
cont xh xl yh yl]]) ->
forall ah al bh bl , [[
WW ah al]] > [[
WW bh bl]] ->
[[
WW bh bl]] <= 2^(Zpos
p +
n) ->
Zis_gcd [[
WW ah al]] [[
WW bh bl]]
[[
ww_gcd_gt_fix p cont ah al bh bl]].
Definition gcd_cont (
xh xl yh yl:w) :=
match w_compare w_1 yl with
|
Eq =>
ww_1
|
_ =>
WW xh xl
end.
Lemma spec_gcd_cont :
forall xh xl yh yl,
[[
WW xh xl]] > [[
WW yh yl]] ->
[[
WW yh yl]] <= 1 ->
Zis_gcd [[
WW xh xl]] [[
WW yh yl]] [[
gcd_cont xh xl yh yl]].
Variable cont :
w ->
w ->
w ->
w ->
zn2z w.
Variable spec_cont :
forall xh xl yh yl,
[[
WW xh xl]] > [[
WW yh yl]] ->
[[
WW yh yl]] <= 1 ->
Zis_gcd [[
WW xh xl]] [[
WW yh yl]] [[
cont xh xl yh yl]].
Definition ww_gcd_gt a b :=
match a,
b with
|
W0,
_ =>
b
|
_,
W0 =>
a
|
WW ah al,
WW bh bl =>
if w_eq0 ah then (
WW w_0 (
w_gcd_gt al bl))
else ww_gcd_gt_fix _ww_digits cont ah al bh bl
end.
Definition ww_gcd a b :=
Eval lazy beta delta [
ww_gcd_gt]
in
match ww_compare a b with
|
Gt =>
ww_gcd_gt a b
|
Eq =>
a
|
Lt =>
ww_gcd_gt b a
end.
Lemma spec_ww_gcd_gt :
forall a b, [[
a]] > [[
b]] ->
Zis_gcd [[
a]] [[
b]] [[
ww_gcd_gt a b]].
Lemma spec_ww_gcd :
forall a b,
Zis_gcd [[
a]] [[
b]] [[
ww_gcd a b]].
End DoubleDiv.