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