Library Coq.Numbers.Cyclic.DoubleCyclic.DoubleDivn1


Set Implicit Arguments.

Require Import ZArith Ndigits.
Require Import BigNumPrelude.
Require Import DoubleType.
Require Import DoubleBase.

Local Open Scope Z_scope.


Section GENDIVN1.

 Variable w : Type.
 Variable w_digits : positive.
 Variable w_zdigits : w.
 Variable w_0 : w.
 Variable w_WW : w -> w -> zn2z w.
 Variable w_head0 : w -> w.
 Variable w_add_mul_div : w -> w -> w -> w.
 Variable w_div21 : w -> w -> w -> w * w.
 Variable w_compare : w -> w -> comparison.
 Variable w_sub : w -> w -> w.

 Variable w_to_Z : w -> Z.

 Notation wB := (base w_digits).

 Notation "[| x |]" := (w_to_Z x) (at level 0, x at level 99).
 Notation "[! n | x !]" := (double_to_Z w_digits w_to_Z n x)
                                      (at level 0, x at level 99).
 Notation "[[ x ]]" := (zn2z_to_Z wB w_to_Z x) (at level 0, x at level 99).

 Variable spec_to_Z : forall x, 0 <= [| x |] < wB.
 Variable spec_w_zdigits: [|w_zdigits|] = Zpos w_digits.
 Variable spec_0 : [|w_0|] = 0.
 Variable spec_WW : forall h l, [[w_WW h l]] = [|h|] * wB + [|l|].
 Variable spec_head0 : forall x, 0 < [|x|] ->
         wB/ 2 <= 2 ^ [|w_head0 x|] * [|x|] < wB.
 Variable spec_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_div21 : forall a1 a2 b,
     wB/2 <= [|b|] ->
     [|a1|] < [|b|] ->
     let (q,r) := w_div21 a1 a2 b in
     [|a1|] *wB+ [|a2|] = [|q|] * [|b|] + [|r|] /\
     0 <= [|r|] < [|b|].
 Variable spec_compare :
   forall x y, w_compare x y = Z.compare [|x|] [|y|].
 Variable spec_sub: forall x y,
   [|w_sub x y|] = ([|x|] - [|y|]) mod wB.

 Section DIVAUX.
  Variable b2p : w.
  Variable b2p_le : wB/2 <= [|b2p|].

  Definition double_divn1_0_aux n (divn1: w -> word w n -> word w n * w) r h :=
   let (hh,hl) := double_split w_0 n h in
   let (qh,rh) := divn1 r hh in
   let (ql,rl) := divn1 rh hl in
   (double_WW w_WW n qh ql, rl).

  Fixpoint double_divn1_0 (n:nat) : w -> word w n -> word w n * w :=
   match n return w -> word w n -> word w n * w with
   | O => fun r x => w_div21 r x b2p
   | S n => double_divn1_0_aux n (double_divn1_0 n)
   end.

  Lemma spec_split : forall (n : nat) (x : zn2z (word w n)),
       let (h, l) := double_split w_0 n x in
       [!S n | x!] = [!n | h!] * double_wB w_digits n + [!n | l!].

  Lemma spec_double_divn1_0 : forall n r a,
    [|r|] < [|b2p|] ->
    let (q,r') := double_divn1_0 n r a in
    [|r|] * double_wB w_digits n + [!n|a!] = [!n|q!] * [|b2p|] + [|r'|] /\
    0 <= [|r'|] < [|b2p|].

  Definition double_modn1_0_aux n (modn1:w -> word w n -> w) r h :=
   let (hh,hl) := double_split w_0 n h in modn1 (modn1 r hh) hl.

  Fixpoint double_modn1_0 (n:nat) : w -> word w n -> w :=
   match n return w -> word w n -> w with
   | O => fun r x => snd (w_div21 r x b2p)
   | S n => double_modn1_0_aux n (double_modn1_0 n)
   end.

  Lemma spec_double_modn1_0 : forall n r x,
     double_modn1_0 n r x = snd (double_divn1_0 n r x).

  Variable p : w.
  Variable p_bounded : [|p|] <= Zpos w_digits.

  Lemma spec_add_mul_divp : forall x y,
    [| w_add_mul_div p x y |] =
       ([|x|] * (2 ^ [|p|]) +
          [|y|] / (2 ^ ((Zpos w_digits) - [|p|]))) mod wB.

  Definition double_divn1_p_aux n
   (divn1 : w -> word w n -> word w n -> word w n * w) r h l :=
   let (hh,hl) := double_split w_0 n h in
   let (lh,ll) := double_split w_0 n l in
   let (qh,rh) := divn1 r hh hl in
   let (ql,rl) := divn1 rh hl lh in
   (double_WW w_WW n qh ql, rl).

  Fixpoint double_divn1_p (n:nat) : w -> word w n -> word w n -> word w n * w :=
   match n return w -> word w n -> word w n -> word w n * w with
   | O => fun r h l => w_div21 r (w_add_mul_div p h l) b2p
   | S n => double_divn1_p_aux n (double_divn1_p n)
   end.

  Lemma p_lt_double_digits : forall n, [|p|] <= Zpos (w_digits << n).

  Lemma spec_double_divn1_p : forall n r h l,
    [|r|] < [|b2p|] ->
    let (q,r') := double_divn1_p n r h l in
    [|r|] * double_wB w_digits n +
      ([!n|h!]*2^[|p|] +
        [!n|l!] / (2^(Zpos(w_digits << n) - [|p|])))
        mod double_wB w_digits n = [!n|q!] * [|b2p|] + [|r'|] /\
    0 <= [|r'|] < [|b2p|].

  Definition double_modn1_p_aux n (modn1 : w -> word w n -> word w n -> w) r h l:=
   let (hh,hl) := double_split w_0 n h in
   let (lh,ll) := double_split w_0 n l in
   modn1 (modn1 r hh hl) hl lh.

  Fixpoint double_modn1_p (n:nat) : w -> word w n -> word w n -> w :=
   match n return w -> word w n -> word w n -> w with
   | O => fun r h l => snd (w_div21 r (w_add_mul_div p h l) b2p)
   | S n => double_modn1_p_aux n (double_modn1_p n)
   end.

  Lemma spec_double_modn1_p : forall n r h l ,
    double_modn1_p n r h l = snd (double_divn1_p n r h l).

 End DIVAUX.

 Fixpoint high (n:nat) : word w n -> w :=
  match n return word w n -> w with
  | O => fun a => a
  | S n =>
    fun (a:zn2z (word w n)) =>
     match a with
     | W0 => w_0
     | WW h l => high n h
     end
  end.

 Lemma spec_double_digits:forall n, Zpos w_digits <= Zpos (w_digits << n).

 Lemma spec_high : forall n (x:word w n),
   [|high n x|] = [!n|x!] / 2^(Zpos (w_digits << n) - Zpos w_digits).

 Definition double_divn1 (n:nat) (a:word w n) (b:w) :=
  let p := w_head0 b in
  match w_compare p w_0 with
  | Gt =>
    let b2p := w_add_mul_div p b w_0 in
    let ha := high n a in
    let k := w_sub w_zdigits p in
    let lsr_n := w_add_mul_div k w_0 in
    let r0 := w_add_mul_div p w_0 ha in
    let (q,r) := double_divn1_p b2p p n r0 a (double_0 w_0 n) in
    (q, lsr_n r)
  | _ => double_divn1_0 b n w_0 a
  end.

 Lemma spec_double_divn1 : forall n a b,
    0 < [|b|] ->
    let (q,r) := double_divn1 n a b in
    [!n|a!] = [!n|q!] * [|b|] + [|r|] /\
    0 <= [|r|] < [|b|].

 Definition double_modn1 (n:nat) (a:word w n) (b:w) :=
  let p := w_head0 b in
  match w_compare p w_0 with
  | Gt =>
    let b2p := w_add_mul_div p b w_0 in
    let ha := high n a in
    let k := w_sub w_zdigits p in
    let lsr_n := w_add_mul_div k w_0 in
    let r0 := w_add_mul_div p w_0 ha in
    let r := double_modn1_p b2p p n r0 a (double_0 w_0 n) in
    lsr_n r
  | _ => double_modn1_0 b n w_0 a
  end.

 Lemma spec_double_modn1_aux : forall n a b,
    double_modn1 n a b = snd (double_divn1 n a b).

 Lemma spec_double_modn1 : forall n a b, 0 < [|b|] ->
  [|double_modn1 n a b|] = [!n|a!] mod [|b|].

End GENDIVN1.