Library Coq.NArith.Nnat

Require Import Arith_base.
Require Import Compare_dec.
Require Import Sumbool.
Require Import Div2.
Require Import BinPos.
Require Import BinNat.
Require Import Pnat.
Translation from N to nat and back.

Definition nat_of_N (a:N) :=
  match a with
  | N0 => 0%nat
  | Npos p => nat_of_P p
  end.

Definition N_of_nat (n:nat) :=
  match n with
  | O => N0
  | S n' => Npos (P_of_succ_nat n')
  end.

Lemma N_of_nat_of_N : forall a:N, N_of_nat (nat_of_N a) = a.
Proof.
  destruct a as [| p]. reflexivity.
  simpl in |- *. elim (ZL4 p). intros n H. rewrite H. simpl in |- *.
  rewrite <- nat_of_P_o_P_of_succ_nat_eq_succ in H.
  rewrite nat_of_P_inj with (1 := H). reflexivity.
Qed.

Lemma nat_of_N_of_nat : forall n:nat, nat_of_N (N_of_nat n) = n.
Proof.
  induction n. trivial.
  intros. simpl in |- *. apply nat_of_P_o_P_of_succ_nat_eq_succ.
Qed.
Interaction of this translation and usual operations.

Lemma nat_of_Ndouble : forall a, nat_of_N (Ndouble a) = 2*(nat_of_N a).
Proof.
  destruct a; simpl nat_of_N; auto.
  apply nat_of_P_xO.
Qed.

Lemma N_of_double : forall n, N_of_nat (2*n) = Ndouble (N_of_nat n).
Proof.
  intros.
  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
  rewrite <- nat_of_Ndouble.
  apply N_of_nat_of_N.
Qed.

Lemma nat_of_Ndouble_plus_one :
  forall a, nat_of_N (Ndouble_plus_one a) = S (2*(nat_of_N a)).
Proof.
  destruct a; simpl nat_of_N; auto.
  apply nat_of_P_xI.
Qed.

Lemma N_of_double_plus_one :
  forall n, N_of_nat (S (2*n)) = Ndouble_plus_one (N_of_nat n).
Proof.
  intros.
  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
  rewrite <- nat_of_Ndouble_plus_one.
  apply N_of_nat_of_N.
Qed.

Lemma nat_of_Nsucc : forall a, nat_of_N (Nsucc a) = S (nat_of_N a).
Proof.
  destruct a; simpl.
  apply nat_of_P_xH.
  apply nat_of_P_succ_morphism.
Qed.

Lemma N_of_S : forall n, N_of_nat (S n) = Nsucc (N_of_nat n).
Proof.
  intros.
  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
  rewrite <- nat_of_Nsucc.
  apply N_of_nat_of_N.
Qed.

Lemma nat_of_Nplus :
  forall a a', nat_of_N (Nplus a a') = (nat_of_N a)+(nat_of_N a').
Proof.
  destruct a; destruct a'; simpl; auto.
  apply nat_of_P_plus_morphism.
Qed.

Lemma N_of_plus :
  forall n n', N_of_nat (n+n') = Nplus (N_of_nat n) (N_of_nat n').
Proof.
  intros.
  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
  rewrite <- nat_of_Nplus.
  apply N_of_nat_of_N.
Qed.

Lemma nat_of_Nmult :
  forall a a', nat_of_N (Nmult a a') = (nat_of_N a)*(nat_of_N a').
Proof.
  destruct a; destruct a'; simpl; auto.
  apply nat_of_P_mult_morphism.
Qed.

Lemma N_of_mult :
  forall n n', N_of_nat (n*n') = Nmult (N_of_nat n) (N_of_nat n').
Proof.
  intros.
  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
  rewrite <- nat_of_Nmult.
  apply N_of_nat_of_N.
Qed.

Lemma nat_of_Ndiv2 :
  forall a, nat_of_N (Ndiv2 a) = div2 (nat_of_N a).
Proof.
  destruct a; simpl in *; auto.
  destruct p; auto.
  rewrite nat_of_P_xI.
  rewrite div2_double_plus_one; auto.
  rewrite nat_of_P_xO.
  rewrite div2_double; auto.
Qed.

Lemma N_of_div2 :
  forall n, N_of_nat (div2 n) = Ndiv2 (N_of_nat n).
Proof.
  intros.
  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
  rewrite <- nat_of_Ndiv2.
  apply N_of_nat_of_N.
Qed.

Lemma nat_of_Ncompare :
 forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a').
Proof.
  destruct a; destruct a'; simpl.
  compute; auto.
  generalize (lt_O_nat_of_P p).
  unfold nat_compare.
  destruct (lt_eq_lt_dec 0 (nat_of_P p)) as [[H|H]|H]; auto.
  rewrite <- H; inversion 1.
  intros; generalize (lt_trans _ _ _ H0 H); inversion 1.
  generalize (lt_O_nat_of_P p).
  unfold nat_compare.
  destruct (lt_eq_lt_dec (nat_of_P p) 0) as [[H|H]|H]; auto.
  intros; generalize (lt_trans _ _ _ H0 H); inversion 1.
  rewrite H; inversion 1.
  unfold nat_compare.
  destruct (lt_eq_lt_dec (nat_of_P p) (nat_of_P p0)) as [[H|H]|H]; auto.
  apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
  rewrite (nat_of_P_inj _ _ H); apply Pcompare_refl.
  apply nat_of_P_gt_Gt_compare_complement_morphism; auto.
Qed.

Lemma N_of_nat_compare :
 forall n n', nat_compare n n' = Ncompare (N_of_nat n) (N_of_nat n').
Proof.
  intros.
  pattern n at 1; rewrite <- (nat_of_N_of_nat n).
  pattern n' at 1; rewrite <- (nat_of_N_of_nat n').
  symmetry; apply nat_of_Ncompare.
Qed.