# Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleBase

Require Import ZArith.
Require Import BigNumPrelude.
Require Import DoubleType.
Local Open Scope Z_scope.
Section DoubleBase.
Variable w : Type.
Variable w_0 : w.
Variable w_1 : w.
Variable w_Bm1 : w.
Variable w_WW : w -> w -> zn2z w.
Variable w_0W : w -> zn2z w.
Variable w_digits : positive.
Variable w_zdigits: w.
Variable w_add: w -> w -> zn2z w.
Variable w_to_Z : w -> Z.
Variable w_compare : w -> w -> comparison.
Definition ww_digits := xO w_digits.
Definition ww_zdigits := w_add w_zdigits w_zdigits.
Definition ww_to_Z := zn2z_to_Z (base w_digits) w_to_Z.
Definition ww_1 := WW w_0 w_1.
Definition ww_Bm1 := WW w_Bm1 w_Bm1.
Definition ww_WW xh xl : zn2z (zn2z w) :=
match xh, xl with
| W0, W0 => W0
| _, _ => WW xh xl
end.
Definition ww_W0 h : zn2z (zn2z w) :=
match h with
| W0 => W0
| _ => WW h W0
end.
Definition ww_0W l : zn2z (zn2z w) :=
match l with
| W0 => W0
| _ => WW W0 l
end.
Definition double_WW (n:nat) :=
match n return word w n -> word w n -> word w (S n) with
| O => w_WW
| S n =>
fun (h l : zn2z (word w n)) =>
match h, l with
| W0, W0 => W0
| _, _ => WW h l
end
end.
Fixpoint double_digits (n:nat) : positive :=
match n with
| O => w_digits
| S n => xO (double_digits n)
end.
Definition double_wB n := base (double_digits n).
Fixpoint double_to_Z (n:nat) : word w n -> Z :=
match n return word w n -> Z with
| O => w_to_Z
| S n => zn2z_to_Z (double_wB n) (double_to_Z n)
end.
Fixpoint extend_aux (n:nat) (x:zn2z w) {struct n}: word w (S n) :=
match n return word w (S n) with
| O => x
| S n1 => WW W0 (extend_aux n1 x)
end.
Definition extend (n:nat) (x:w) : word w (S n) :=
let r := w_0W x in
match r with
| W0 => W0
| _ => extend_aux n r
end.
Definition double_0 n : word w n :=
match n return word w n with
| O => w_0
| S _ => W0
end.
Definition double_split (n:nat) (x:zn2z (word w n)) :=
match x with
| W0 =>
match n return word w n * word w n with
| O => ( w_0 , w_0 )
| S _ => ( W0 , W0 )
end
| WW h l => ( h , l )
end.
Definition ww_compare x y :=
match x, y with
| W0, W0 => Eq
| W0, WW yh yl =>
match w_compare w_0 yh with
| Eq => w_compare w_0 yl
| _ => Lt
end
| WW xh xl, W0 =>
match w_compare xh w_0 with
| Eq => w_compare xl w_0
| _ => Gt
end
| WW xh xl, WW yh yl =>
match w_compare xh yh with
| Eq => w_compare xl yl
| Lt => Lt
| Gt => Gt
end
end.
Fixpoint get_low (n : nat) {struct n}:
word w n -> w :=
match n return (word w n -> w) with
| 0%nat => fun x => x
| S n1 =>
fun x =>
match x with
| W0 => w_0
| WW _ x1 => get_low n1 x1
end
end.
Section DoubleProof.
Notation wB := (base w_digits).
Notation wwB := (base ww_digits).
Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99).
Notation "[[ x ]]" := (ww_to_Z x) (at level 0, x at level 99).
Notation "[+[ c ]]" :=
(interp_carry 1 wwB ww_to_Z c) (at level 0, x at level 99).
Notation "[-[ c ]]" :=
(interp_carry (-1) wwB ww_to_Z c) (at level 0, x at level 99).
Notation "[! n | x !]" := (double_to_Z n x) (at level 0, x at level 99).
Variable spec_w_0 : [| w_0 |] = 0.
Variable spec_w_1 : [| w_1 |] = 1.
Variable spec_w_Bm1 : [| w_Bm1 |] = wB - 1.
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_to_Z : forall x, 0 <= [| x |] < wB.
Variable spec_w_compare : forall x y,
match w_compare x y with
| Eq => [| x |] = [| y |]
| Lt => [| x |] < [| y |]
| Gt => [| x |] > [| y |]
end.
Lemma wwB_wBwB : wwB = wB ^2.
Lemma spec_ww_1 : [[ ww_1 ]] = 1.
Lemma spec_ww_Bm1 : [[ ww_Bm1 ]] = wwB - 1.
Lemma lt_0_wB : 0 < wB.
Lemma lt_0_wwB : 0 < wwB.
Lemma wB_pos: 1 < wB.
Lemma wwB_pos: 1 < wwB.
Theorem wB_div_2: 2 * ( wB / 2) = wB.
Theorem wwB_div_2 : wwB / 2 = wB / 2 * wB.
Lemma mod_wwB : forall z x,
( z * wB + [| x |] ) mod wwB = ( z mod wB )* wB + [| x |].
Lemma wB_div : forall x y, ( [| x |] * wB + [| y |] ) / wB = [| x |].
Lemma wB_div_plus : forall x y p,
0 <= p ->
( [| x |] * wB + [| y |] ) / 2^( Zpos w_digits + p ) = [| x |] / 2^ p.
Lemma lt_wB_wwB : wB < wwB.
Lemma w_to_Z_wwB : forall x, x < wB -> x < wwB.
Lemma spec_ww_to_Z : forall x, 0 <= [[ x ]] < wwB.
Lemma double_wB_wwB : forall n, double_wB n * double_wB n = double_wB (S n).
Lemma double_wB_pos:
forall n, 0 <= double_wB n.
Lemma double_wB_more_digits:
forall n, wB <= double_wB n.
Lemma spec_double_to_Z :
forall n (x:word w n), 0 <= [! n | x !] < double_wB n.
Lemma spec_get_low:
forall n x,
[! n | x !] < wB -> [| get_low n x |] = [! n | x !].
Lemma spec_double_WW : forall n (h l : word w n),
[! S n | double_WW n h l !] = [! n | h !] * double_wB n + [! n | l !].
Lemma spec_extend_aux : forall n x, [! S n | extend_aux n x !] = [[ x ]].
Lemma spec_extend : forall n x, [! S n | extend n x !] = [| x |].
Lemma spec_double_0 : forall n, [! n | double_0 n !] = 0.
Lemma spec_double_split : forall n x,
let (h,l) := double_split n x in
[! S n | x !] = [! n | h !] * double_wB n + [! n | l !].
Lemma wB_lex_inv: forall a b c d,
a < c ->
a * wB + [| b |] < c * wB + [| d |].
Lemma spec_ww_compare : forall x y,
match ww_compare x y with
| Eq => [[ x ]] = [[ y ]]
| Lt => [[ x ]] < [[ y ]]
| Gt => [[ x ]] > [[ y ]]
end.
End DoubleProof.
End DoubleBase.