# Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleBase

Set Implicit Arguments.
Require Import ZArith Ndigits.
Require Import BigNumPrelude.
Require Import DoubleType.
Local Open Scope Z_scope.
Local Infix "<<" := Pos.shiftl_nat (at level 30).
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.
Definition double_wB n := base (w_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,
w_compare x y = Z.compare [|x|] [|y|].
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|].
Ltac comp2ord := match goal with
| |- Lt = (?x ?= ?y) => symmetry; change (x < y)
| |- Gt = (?x ?= ?y) => symmetry; change (x > y); apply Z.lt_gt
end.
Lemma spec_ww_compare : forall x y,
ww_compare x y = Z.compare [[x]] [[y]].
End DoubleProof.
End DoubleBase.