Library Coq.ZArith.ZOdiv_def


Require Import BinPos BinNat Nnat ZArith_base.

Open Scope Z_scope.

Definition NPgeb (a:N)(b:positive) :=
  match a with
   | N0 => false
   | Npos na => match Pcompare na b Eq with Lt => false | _ => true end
  end.

Fixpoint Pdiv_eucl (a b:positive) {struct a} : N * N :=
  match a with
    | xH =>
       match b with xH => (1, 0)%N | _ => (0, 1)%N end
    | xO a' =>
       let (q, r) := Pdiv_eucl a' b in
       let r' := (2 * r)%N in
        if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N
        else (2 * q, r')%N
    | xI a' =>
       let (q, r) := Pdiv_eucl a' b in
       let r' := (2 * r + 1)%N in
        if (NPgeb r' b) then (2 * q + 1, (Nminus r' (Npos b)))%N
        else (2 * q, r')%N
  end.

Definition ZOdiv_eucl (a b:Z) : Z * Z :=
  match a, b with
   | Z0, _ => (Z0, Z0)
   | _, Z0 => (Z0, a)
   | Zpos na, Zpos nb =>
         let (nq, nr) := Pdiv_eucl na nb in
         (Z_of_N nq, Z_of_N nr)
   | Zneg na, Zpos nb =>
         let (nq, nr) := Pdiv_eucl na nb in
         (Zopp (Z_of_N nq), Zopp (Z_of_N nr))
   | Zpos na, Zneg nb =>
         let (nq, nr) := Pdiv_eucl na nb in
         (Zopp (Z_of_N nq), Z_of_N nr)
   | Zneg na, Zneg nb =>
         let (nq, nr) := Pdiv_eucl na nb in
         (Z_of_N nq, Zopp (Z_of_N nr))
  end.

Definition ZOdiv a b := fst (ZOdiv_eucl a b).
Definition ZOmod a b := snd (ZOdiv_eucl a b).

Definition Ndiv_eucl (a b:N) : N * N :=
  match a, b with
   | N0, _ => (N0, N0)
   | _, N0 => (N0, a)
   | Npos na, Npos nb => Pdiv_eucl na nb
  end.

Definition Ndiv a b := fst (Ndiv_eucl a b).
Definition Nmod a b := snd (Ndiv_eucl a b).


Theorem NPgeb_correct: forall (a:N)(b:positive),
  if NPgeb a b then a = (Nminus a (Npos b) + Npos b)%N else True.

Hint Rewrite Z_of_N_plus Z_of_N_mult Z_of_N_minus Zmult_1_l Zmult_assoc
 Zmult_plus_distr_l Zmult_plus_distr_r : zdiv.
Hint Rewrite <- Zplus_assoc : zdiv.

Theorem Pdiv_eucl_correct: forall a b,
  let (q,r) := Pdiv_eucl a b in
  Zpos a = Z_of_N q * Zpos b + Z_of_N r.

Theorem ZOdiv_eucl_correct: forall a b,
  let (q,r) := ZOdiv_eucl a b in a = q * b + r.

Theorem Ndiv_eucl_correct: forall a b,
  let (q,r) := Ndiv_eucl a b in a = (q * b + r)%N.