Library Coq.Numbers.Natural.BigN.Nbasic



Require Import ZArith.
Require Import BigNumPrelude.
Require Import Max.
Require Import DoubleType.
Require Import DoubleBase.
Require Import CyclicAxioms.
Require Import DoubleCyclic.


Fixpoint plength (p: positive) : positive :=
  match p with
    xH => xH
  | xO p1 => Psucc (plength p1)
  | xI p1 => Psucc (plength p1)
  end.

Theorem plength_correct: forall p, (Zpos p < 2 ^ Zpos (plength p))%Z.

Theorem plength_pred_correct: forall p, (Zpos p <= 2 ^ Zpos (plength (Ppred p)))%Z.

Definition Pdiv p q :=
  match Zdiv (Zpos p) (Zpos q) with
    Zpos q1 => match (Zpos p) - (Zpos q) * (Zpos q1) with
                 Z0 => q1
               | _ => (Psucc q1)
               end
  | _ => xH
  end.

Theorem Pdiv_le: forall p q,
  Zpos p <= Zpos q * Zpos (Pdiv p q).

Definition is_one p := match p with xH => true | _ => false end.

Theorem is_one_one: forall p, is_one p = true -> p = xH.

Definition get_height digits p :=
  let r := Pdiv p digits in
   if is_one r then xH else Psucc (plength (Ppred r)).

Theorem get_height_correct:
  forall digits N,
   Zpos N <= Zpos digits * (2 ^ (Zpos (get_height digits N) -1)).

Definition zn2z_word_comm : forall w n, zn2z (word w n) = word (zn2z w) n.
Defined.

Fixpoint extend (n:nat) {struct n} : forall w:Type, zn2z w -> word w (S n) :=
 match n return forall w:Type, zn2z w -> word w (S n) with
 | O => fun w x => x
 | S m =>
   let aux := extend m in
   fun w x => WW W0 (aux w x)
 end.

Section ExtendMax.

Open Scope nat_scope.

Fixpoint plusnS (n m: nat) {struct n} : (n + S m = S (n + m))%nat :=
  match n return (n + S m = S (n + m))%nat with
  | 0 => refl_equal (S m)
  | S n1 =>
      let v := S (S n1 + m) in
      eq_ind_r (fun n => S n = v) (refl_equal v) (plusnS n1 m)
  end.

Fixpoint plusn0 n : n + 0 = n :=
  match n return (n + 0 = n) with
  | 0 => refl_equal 0
  | S n1 =>
      let v := S n1 in
      eq_ind_r (fun n : nat => S n = v) (refl_equal v) (plusn0 n1)
  end.

 Fixpoint diff (m n: nat) {struct m}: nat * nat :=
   match m, n with
     O, n => (O, n)
   | m, O => (m, O)
   | S m1, S n1 => diff m1 n1
   end.

Fixpoint diff_l (m n : nat) {struct m} : fst (diff m n) + n = max m n :=
  match m return fst (diff m n) + n = max m n with
  | 0 =>
      match n return (n = max 0 n) with
      | 0 => refl_equal _
      | S n0 => refl_equal _
      end
  | S m1 =>
      match n return (fst (diff (S m1) n) + n = max (S m1) n)
      with
      | 0 => plusn0 _
      | S n1 =>
          let v := fst (diff m1 n1) + n1 in
          let v1 := fst (diff m1 n1) + S n1 in
          eq_ind v (fun n => v1 = S n)
            (eq_ind v1 (fun n => v1 = n) (refl_equal v1) (S v) (plusnS _ _))
            _ (diff_l _ _)
      end
  end.

Fixpoint diff_r (m n: nat) {struct m}: snd (diff m n) + m = max m n :=
  match m return (snd (diff m n) + m = max m n) with
  | 0 =>
      match n return (snd (diff 0 n) + 0 = max 0 n) with
      | 0 => refl_equal _
      | S _ => plusn0 _
      end
  | S m =>
      match n return (snd (diff (S m) n) + S m = max (S m) n) with
      | 0 => refl_equal (snd (diff (S m) 0) + S m)
      | S n1 =>
          let v := S (max m n1) in
          eq_ind_r (fun n => n = v)
            (eq_ind_r (fun n => S n = v)
               (refl_equal v) (diff_r _ _)) (plusnS _ _)
      end
  end.

 Variable w: Type.

 Definition castm (m n: nat) (H: m = n) (x: word w (S m)):
     (word w (S n)) :=
 match H in (_ = y) return (word w (S y)) with
 | refl_equal => x
 end.

Variable m: nat.
Variable v: (word w (S m)).

Fixpoint extend_tr (n : nat) {struct n}: (word w (S (n + m))) :=
  match n return (word w (S (n + m))) with
  | O => v
  | S n1 => WW W0 (extend_tr n1)
  end.

End ExtendMax.

Implicit Arguments extend_tr[w m].
Implicit Arguments castm[w m n].

Section Reduce.

 Variable w : Type.
 Variable nT : Type.
 Variable N0 : nT.
 Variable eq0 : w -> bool.
 Variable reduce_n : w -> nT.
 Variable zn2z_to_Nt : zn2z w -> nT.

 Definition reduce_n1 (x:zn2z w) :=
  match x with
  | W0 => N0
  | WW xh xl =>
    if eq0 xh then reduce_n xl
    else zn2z_to_Nt x
  end.

End Reduce.

Section ReduceRec.

 Variable w : Type.
 Variable nT : Type.
 Variable N0 : nT.
 Variable reduce_1n : zn2z w -> nT.
 Variable c : forall n, word w (S n) -> nT.

 Fixpoint reduce_n (n:nat) : word w (S n) -> nT :=
  match n return word w (S n) -> nT with
  | O => reduce_1n
  | S m => fun x =>
    match x with
    | W0 => N0
    | WW xh xl =>
      match xh with
      | W0 => @reduce_n m xl
      | _ => @c (S m) x
      end
    end
  end.

End ReduceRec.

Definition opp_compare cmp :=
  match cmp with
  | Lt => Gt
  | Eq => Eq
  | Gt => Lt
  end.

Section CompareRec.

 Variable wm w : Type.
 Variable w_0 : w.
 Variable compare : w -> w -> comparison.
 Variable compare0_m : wm -> comparison.
 Variable compare_m : wm -> w -> comparison.

 Fixpoint compare0_mn (n:nat) : word wm n -> comparison :=
  match n return word wm n -> comparison with
  | O => compare0_m
  | S m => fun x =>
    match x with
    | W0 => Eq
    | WW xh xl =>
      match compare0_mn m xh with
      | Eq => compare0_mn m xl
      | r => Lt
      end
    end
  end.

 Variable wm_base: positive.
 Variable wm_to_Z: wm -> Z.
 Variable w_to_Z: w -> Z.
 Variable w_to_Z_0: w_to_Z w_0 = 0.
 Variable spec_compare0_m: forall x,
    match compare0_m x with
      Eq => w_to_Z w_0 = wm_to_Z x
    | Lt => w_to_Z w_0 < wm_to_Z x
    | Gt => w_to_Z w_0 > wm_to_Z x
    end.
 Variable wm_to_Z_pos: forall x, 0 <= wm_to_Z x < base wm_base.

 Let double_to_Z := double_to_Z wm_base wm_to_Z.
 Let double_wB := double_wB wm_base.

 Lemma base_xO: forall n, base (xO n) = (base n)^2.

 Let double_to_Z_pos: forall n x, 0 <= double_to_Z n x < double_wB n :=
   (spec_double_to_Z wm_base wm_to_Z wm_to_Z_pos).

 Lemma spec_compare0_mn: forall n x,
    match compare0_mn n x with
      Eq => 0 = double_to_Z n x
    | Lt => 0 < double_to_Z n x
    | Gt => 0 > double_to_Z n x
    end.

 Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison :=
  match n return word wm n -> w -> comparison with
  | O => compare_m
  | S m => fun x y =>
    match x with
    | W0 => compare w_0 y
    | WW xh xl =>
      match compare0_mn m xh with
      | Eq => compare_mn_1 m xl y
      | r => Gt
      end
    end
  end.

 Variable spec_compare: forall x y,
   match compare x y with
     Eq => w_to_Z x = w_to_Z y
   | Lt => w_to_Z x < w_to_Z y
   | Gt => w_to_Z x > w_to_Z y
   end.
 Variable spec_compare_m: forall x y,
   match compare_m x y with
     Eq => wm_to_Z x = w_to_Z y
   | Lt => wm_to_Z x < w_to_Z y
   | Gt => wm_to_Z x > w_to_Z y
   end.
 Variable wm_base_lt: forall x,
   0 <= w_to_Z x < base (wm_base).

 Let double_wB_lt: forall n x,
   0 <= w_to_Z x < (double_wB n).


 Lemma spec_compare_mn_1: forall n x y,
   match compare_mn_1 n x y with
     Eq => double_to_Z n x = w_to_Z y
   | Lt => double_to_Z n x < w_to_Z y
   | Gt => double_to_Z n x > w_to_Z y
   end.

End CompareRec.

Section AddS.

 Variable w wm : Type.
 Variable incr : wm -> carry wm.
 Variable addr : w -> wm -> carry wm.
 Variable injr : w -> zn2z wm.

 Variable w_0 u: w.
 Fixpoint injs (n:nat): word w (S n) :=
  match n return (word w (S n)) with
    O => WW w_0 u
  | S n1 => (WW W0 (injs n1))
  end.

 Definition adds x y :=
   match y with
    W0 => C0 (injr x)
  | WW hy ly => match addr x ly with
                  C0 z => C0 (WW hy z)
                | C1 z => match incr hy with
                            C0 z1 => C0 (WW z1 z)
                          | C1 z1 => C1 (WW z1 z)
                          end
                 end
   end.

End AddS.

 Lemma spec_opp: forall u x y,
  match u with
  | Eq => y = x
  | Lt => y < x
  | Gt => y > x
  end ->
  match opp_compare u with
  | Eq => x = y
  | Lt => x < y
  | Gt => x > y
  end.

 Fixpoint length_pos x :=
  match x with xH => O | xO x1 => S (length_pos x1) | xI x1 => S (length_pos x1) end.

 Theorem length_pos_lt: forall x y,
   (length_pos x < length_pos y)%nat -> Zpos x < Zpos y.

 Theorem cancel_app: forall A B (f g: A -> B) x, f = g -> f x = g x.

 Section SimplOp.

 Variable w: Type.

 Theorem digits_zop: forall w (x: znz_op w),
  znz_digits (mk_zn2z_op x) = xO (znz_digits x).

 Theorem digits_kzop: forall w (x: znz_op w),
  znz_digits (mk_zn2z_op_karatsuba x) = xO (znz_digits x).

 Theorem make_zop: forall w (x: znz_op w),
  znz_to_Z (mk_zn2z_op x) =
    fun z => match z with
                W0 => 0
             | WW xh xl => znz_to_Z x xh * base (znz_digits x)
                                + znz_to_Z x xl
             end.

 Theorem make_kzop: forall w (x: znz_op w),
  znz_to_Z (mk_zn2z_op_karatsuba x) =
    fun z => match z with
                W0 => 0
             | WW xh xl => znz_to_Z x xh * base (znz_digits x)
                                + znz_to_Z x xl
             end.

 End SimplOp.