Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleLift
Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Open Local Scope Z_scope.
Section DoubleLift.
Variable w :
Type.
Variable w_0 :
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 ww_compare :
zn2z w ->
zn2z w ->
comparison.
Variable w_head0 :
w ->
w.
Variable w_tail0 :
w ->
w.
Variable w_add:
w ->
w ->
zn2z w.
Variable w_add_mul_div :
w ->
w ->
w ->
w.
Variable ww_sub:
zn2z w ->
zn2z w ->
zn2z w.
Variable w_digits :
positive.
Variable ww_Digits :
positive.
Variable w_zdigits :
w.
Variable ww_zdigits :
zn2z w.
Variable low:
zn2z w ->
w.
Definition ww_head0 x :=
match x with
|
W0 =>
ww_zdigits
|
WW xh xl =>
match w_compare w_0 xh with
|
Eq =>
w_add w_zdigits (
w_head0 xl)
|
_ =>
w_0W (
w_head0 xh)
end
end.
Definition ww_tail0 x :=
match x with
|
W0 =>
ww_zdigits
|
WW xh xl =>
match w_compare w_0 xl with
|
Eq =>
w_add w_zdigits (
w_tail0 xh)
|
_ =>
w_0W (
w_tail0 xl)
end
end.
Definition ww_add_mul_div p x y :=
let zdigits :=
w_0W w_zdigits in
match x,
y with
|
W0,
W0 =>
W0
|
W0,
WW yh yl =>
match ww_compare p zdigits with
|
Eq =>
w_0W yh
|
Lt =>
w_0W (
w_add_mul_div (
low p)
w_0 yh)
|
Gt =>
let n :=
low (
ww_sub p zdigits)
in
w_WW (
w_add_mul_div n w_0 yh) (
w_add_mul_div n yh yl)
end
|
WW xh xl,
W0 =>
match ww_compare p zdigits with
|
Eq =>
w_W0 xl
|
Lt =>
w_WW (
w_add_mul_div (
low p)
xh xl) (
w_add_mul_div (
low p)
xl w_0)
|
Gt =>
let n :=
low (
ww_sub p zdigits)
in
w_W0 (
w_add_mul_div n xl w_0)
end
|
WW xh xl,
WW yh yl =>
match ww_compare p zdigits with
|
Eq =>
w_WW xl yh
|
Lt =>
w_WW (
w_add_mul_div (
low p)
xh xl) (
w_add_mul_div (
low p)
xl yh)
|
Gt =>
let n :=
low (
ww_sub p zdigits)
in
w_WW (
w_add_mul_div n xl yh) (
w_add_mul_div n yh yl)
end
end.
Section DoubleProof.
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_w_W0 :
forall h, [[
w_W0 h]] = [|h|] *
wB.
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_ww_compare :
forall x y,
match ww_compare x y with
|
Eq => [[
x]] = [[
y]]
|
Lt => [[
x]] < [[
y]]
|
Gt => [[
x]] > [[
y]]
end.
Variable spec_ww_digits :
ww_Digits =
xO w_digits.
Variable spec_w_head00 :
forall x, [|x|] = 0 -> [|w_head0
x|] =
Zpos w_digits.
Variable spec_w_head0 :
forall x, 0 < [|x|] ->
wB/ 2 <= 2 ^ ([|w_head0
x|]) * [|x|] <
wB.
Variable spec_w_tail00 :
forall x, [|x|] = 0 -> [|w_tail0
x|] =
Zpos w_digits.
Variable spec_w_tail0 :
forall x, 0 < [|x|] ->
exists y, 0 <=
y /\ [|x|] = (2*
y + 1) * (2 ^ [|w_tail0
x|]).
Variable spec_w_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_w_add:
forall x y,
[[
w_add x y]] = [|x|] + [|y|].
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]] =
Zpos ww_Digits.
Hint Resolve div_le_0 div_lt w_to_Z_wwB:
lift.
Ltac zarith :=
auto with zarith lift.
Lemma spec_ww_head00 :
forall x, [[
x]] = 0 -> [[
ww_head0 x]] =
Zpos ww_Digits.
Lemma spec_ww_head0 :
forall x, 0 < [[
x]] ->
wwB/ 2 <= 2 ^ [[
ww_head0 x]] * [[
x]] <
wwB.
Lemma spec_ww_tail00 :
forall x, [[
x]] = 0 -> [[
ww_tail0 x]] =
Zpos ww_Digits.
Lemma spec_ww_tail0 :
forall x, 0 < [[
x]] ->
exists y, 0 <=
y /\ [[
x]] = (2 *
y + 1) * 2 ^ [[
ww_tail0 x]].
Hint Rewrite Zdiv_0_l Zmult_0_l Zplus_0_l Zmult_0_r Zplus_0_r
spec_w_W0 spec_w_0W spec_w_WW spec_w_0
(
wB_div w_digits w_to_Z spec_to_Z)
(
wB_div_plus w_digits w_to_Z spec_to_Z) :
w_rewrite.
Ltac w_rewrite :=
autorewrite with w_rewrite;
trivial.
Lemma spec_ww_add_mul_div_aux :
forall xh xl yh yl p,
let zdigits :=
w_0W w_zdigits in
[[
p]] <=
Zpos (
xO w_digits) ->
[[
match ww_compare p zdigits with
|
Eq =>
w_WW xl yh
|
Lt =>
w_WW (
w_add_mul_div (
low p)
xh xl)
(
w_add_mul_div (
low p)
xl yh)
|
Gt =>
let n :=
low (
ww_sub p zdigits)
in
w_WW (
w_add_mul_div n xl yh) (
w_add_mul_div n yh yl)
end]] =
([[
WW xh xl]] * (2^[[
p]]) +
[[
WW yh yl]] / (2^(Zpos (
xO w_digits) - [[
p]])))
mod wwB.
Lemma 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.
End DoubleProof.
End DoubleLift.