Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleLift
Set Implicit Arguments.
Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.
Local Open 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,
w_compare x y = Z.compare [|x|] [|y|].
Variable spec_ww_compare :
forall x y,
ww_compare x y = Z.compare [[x]] [[y]].
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 Z.mul_0_l Z.add_0_l Z.mul_0_r Z.add_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.