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.

Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleLift

Navigation