Require Import BigNumPrelude ZArith CyclicAxioms.
Require Import Nbasic Wf_nat StreamMemo NSig NMake_gen.

Module Make (Import W0:CyclicType) <: NType.

 Include NMake_gen.Make W0.

 Lemma spec_pred : forall x, [pred x] = Zmax 0 ([x]-1).

 Lemma spec_sub : forall x y, [sub x y] = Zmax 0 ([x]-[y]).

 Theorem spec_compare : forall x y, compare x y = Zcompare [x] [y].

 Definition eq_bool x y :=
  match compare x y with
  | Eq => true
  | _ => false
  end.

 Theorem spec_eq_bool : forall x y, eq_bool x y = Zeq_bool [x] [y].

 Theorem spec_eq_bool_aux: forall x y,
    if eq_bool x y then [x] = [y] else [x] <> [y].

 Definition lt n m := [n] < [m].
 Definition le n m := [n] <= [m].

 Definition min n m := match compare n m with Gt => m | _ => n end.
 Definition max n m := match compare n m with Lt => m | _ => n end.

 Theorem spec_max : forall n m, [max n m] = Zmax [n] [m].

 Theorem spec_min : forall n m, [min n m] = Zmin [n] [m].

 Fixpoint power_pos (x:t) (p:positive) {struct p} : t :=
  match p with
  | xH => x
  | xO p => square (power_pos x p)
  | xI p => mul (square (power_pos x p)) x
  end.

 Theorem spec_power_pos: forall x n, [power_pos x n] = [x] ^ Zpos n.

 Definition power x (n:N) := match n with
  | BinNat.N0 => one
  | BinNat.Npos p => power_pos x p
 end.

 Theorem spec_power: forall x n, [power x n] = [x] ^ Z_of_N n.

 Definition div_eucl x y :=
  if eq_bool y zero then (zero,zero) else
  match compare x y with
  | Eq => (one, zero)
  | Lt => (zero, x)
  | Gt => div_gt x y
  end.

 Theorem spec_div_eucl: forall x y,
      let (q,r) := div_eucl x y in
      ([q], [r]) = Zdiv_eucl [x] [y].

 Definition div x y := fst (div_eucl x y).

 Theorem spec_div:
   forall x y, [div x y] = [x] / [y].

 Definition modulo x y :=
  if eq_bool y zero then zero else
  match compare x y with
  | Eq => zero
  | Lt => x
  | Gt => mod_gt x y
  end.

 Theorem spec_modulo:
   forall x y, [modulo x y] = [x] mod [y].

 Definition gcd_gt_body a b cont :=
  match compare b zero with
  | Gt =>
    let r := mod_gt a b in
    match compare r zero with
    | Gt => cont r (mod_gt b r)
    | _ => b
    end
  | _ => a
  end.

 Theorem Zspec_gcd_gt_body: forall a b cont p,
    [a] > [b] -> [a] < 2 ^ p ->
      (forall a1 b1, [a1] < 2 ^ (p - 1) -> [a1] > [b1] ->
         Zis_gcd [a1] [b1] [cont a1 b1]) ->
      Zis_gcd [a] [b] [gcd_gt_body a b cont].

 Fixpoint gcd_gt_aux (p:positive) (cont:t->t->t) (a b:t) {struct p} : t :=
  gcd_gt_body a b
    (fun a b =>
       match p with
       | xH => cont a b
       | xO p => gcd_gt_aux p (gcd_gt_aux p cont) a b
       | xI p => gcd_gt_aux p (gcd_gt_aux p cont) a b
       end).

 Theorem Zspec_gcd_gt_aux: forall p n a b cont,
    [a] > [b] -> [a] < 2 ^ (Zpos p + n) ->
      (forall a1 b1, [a1] < 2 ^ n -> [a1] > [b1] ->
            Zis_gcd [a1] [b1] [cont a1 b1]) ->
          Zis_gcd [a] [b] [gcd_gt_aux p cont a b].

 Definition gcd_cont a b :=
  match compare one b with
  | Eq => one
  | _ => a
  end.

 Definition gcd_gt a b := gcd_gt_aux (digits a) gcd_cont a b.

 Theorem spec_gcd_gt: forall a b,
   [a] > [b] -> [gcd_gt a b] = Zgcd [a] [b].

 Definition gcd a b :=
  match compare a b with
  | Eq => a
  | Lt => gcd_gt b a
  | Gt => gcd_gt a b
  end.

 Theorem spec_gcd: forall a b, [gcd a b] = Zgcd [a] [b].

 Definition of_N x :=
  match x with
  | BinNat.N0 => zero
  | Npos p => of_pos p
  end.

 Theorem spec_of_N: forall x,
   [of_N x] = Z_of_N x.

 Definition shiftr n x :=
   match compare n (Ndigits x) with
   | Lt => unsafe_shiftr n x
   | _ => N0 w_0
   end.

 Theorem spec_shiftr: forall n x,
   [shiftr n x] = [x] / 2 ^ [n].

 Definition shiftl_aux_body cont n x :=
   match compare n (head0 x) with
      Gt => cont n (double_size x)
   | _ => unsafe_shiftl n x
   end.

 Theorem spec_shiftl_aux_body: forall n p x cont,
       2^ Zpos p <= [head0 x] ->
      (forall x, 2 ^ (Zpos p + 1) <= [head0 x]->
         [cont n x] = [x] * 2 ^ [n]) ->
      [shiftl_aux_body cont n x] = [x] * 2 ^ [n].

 Fixpoint shiftl_aux p cont n x {struct p} :=
   shiftl_aux_body
       (fun n x => match p with
        | xH => cont n x
        | xO p => shiftl_aux p (shiftl_aux p cont) n x
        | xI p => shiftl_aux p (shiftl_aux p cont) n x
        end) n x.

 Theorem spec_shiftl_aux: forall p q n x cont,
    2 ^ (Zpos q) <= [head0 x] ->
      (forall x, 2 ^ (Zpos p + Zpos q) <= [head0 x] ->
         [cont n x] = [x] * 2 ^ [n]) ->
      [shiftl_aux p cont n x] = [x] * 2 ^ [n].

 Definition shiftl n x :=
  shiftl_aux_body
   (shiftl_aux_body
    (shiftl_aux (digits n) unsafe_shiftl)) n x.

 Theorem spec_shiftl: forall n x,
   [shiftl n x] = [x] * 2 ^ [n].

 Theorem spec_0: [zero] = 0.

 Theorem spec_1: [one] = 1.

End Make.