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.

Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleBase

Navigation