# 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.