Library Coq.NArith.Nnat


Require Import BinPos BinNat PeanoNat Pnat.

Conversions from N to nat


Module N2Nat.

N.to_nat is a bijection between N and nat, with N.of_nat as reciprocal. See Nat2N.id below for the dual equation.

Lemma id a : N.of_nat (N.to_nat a) = a.

N.to_nat is hence injective
Interaction of this translation and usual operations.

Conversions from nat to N


Module Nat2N.

N.of_nat is an bijection between nat and N, with N.to_nat as reciprocal. See N2Nat.id above for the dual equation.

Lemma id n : N.to_nat (N.of_nat n) = n.

Global Hint Rewrite id : Nnat.
Ltac nat2N := apply N2Nat.inj; now autorewrite with Nnat.

N.of_nat is hence injective
Interaction of this translation and usual operations.

Lemma inj_double n : N.of_nat (2*n) = N.double (N.of_nat n).

Lemma inj_succ_double n : N.of_nat (S (2*n)) = N.succ_double (N.of_nat n).

Lemma inj_succ n : N.of_nat (S n) = N.succ (N.of_nat n).

Lemma inj_pred n : N.of_nat (Nat.pred n) = N.pred (N.of_nat n).

Lemma inj_add n n' : N.of_nat (n+n') = (N.of_nat n + N.of_nat n')%N.

Lemma inj_sub n n' : N.of_nat (n-n') = (N.of_nat n - N.of_nat n')%N.

Lemma inj_mul n n' : N.of_nat (n*n') = (N.of_nat n * N.of_nat n')%N.

Lemma inj_div2 n : N.of_nat (Nat.div2 n) = N.div2 (N.of_nat n).

Lemma inj_compare n n' :
  (n ?= n') = (N.of_nat n ?= N.of_nat n')%N.

Lemma inj_div n n' :
  N.of_nat (n / n') = (N.of_nat n / N.of_nat n')%N.

Lemma inj_mod n n' :
  N.of_nat (n mod n') = (N.of_nat n mod N.of_nat n')%N.

Lemma inj_pow n n' :
  N.of_nat (n ^ n') = (N.of_nat n ^ N.of_nat n')%N.

Lemma inj_min n n' :
  N.of_nat (Nat.min n n') = N.min (N.of_nat n) (N.of_nat n').

Lemma inj_max n n' :
  N.of_nat (Nat.max n n') = N.max (N.of_nat n) (N.of_nat n').

Lemma inj_iter n {A} (f:A->A) (x:A) :
  Nat.iter n f x = N.iter (N.of_nat n) f x.

End Nat2N.

Global Hint Rewrite Nat2N.id : Nnat.

Compatibility notations

Notation nat_of_N_inj := N2Nat.inj (only parsing).
Notation N_of_nat_of_N := N2Nat.id (only parsing).
Notation nat_of_Ndouble := N2Nat.inj_double (only parsing).
Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (only parsing).
Notation nat_of_Nsucc := N2Nat.inj_succ (only parsing).
Notation nat_of_Nplus := N2Nat.inj_add (only parsing).
Notation nat_of_Nmult := N2Nat.inj_mul (only parsing).
Notation nat_of_Nminus := N2Nat.inj_sub (only parsing).
Notation nat_of_Npred := N2Nat.inj_pred (only parsing).
Notation nat_of_Ndiv2 := N2Nat.inj_div2 (only parsing).
Notation nat_of_Ncompare := N2Nat.inj_compare (only parsing).
Notation nat_of_Ndiv := N2Nat.inj_div (only parsing).
Notation nat_of_Nmod := N2Nat.inj_mod (only parsing).
Notation nat_of_Npow := N2Nat.inj_pow (only parsing).
Notation nat_of_Nmax := N2Nat.inj_max (only parsing).
Notation nat_of_Nmin := N2Nat.inj_min (only parsing).

Notation nat_of_N_of_nat := Nat2N.id (only parsing).
Notation N_of_nat_inj := Nat2N.inj (only parsing).
Notation N_of_double := Nat2N.inj_double (only parsing).
Notation N_of_double_plus_one := Nat2N.inj_succ_double (only parsing).
Notation N_of_S := Nat2N.inj_succ (only parsing).
Notation N_of_pred := Nat2N.inj_pred (only parsing).
Notation N_of_plus := Nat2N.inj_add (only parsing).
Notation N_of_minus := Nat2N.inj_sub (only parsing).
Notation N_of_mult := Nat2N.inj_mul (only parsing).
Notation N_of_div2 := Nat2N.inj_div2 (only parsing).
Notation N_of_nat_compare := Nat2N.inj_compare (only parsing).
Notation N_of_nat_div := Nat2N.inj_div (only parsing).
Notation N_of_nat_mod := Nat2N.inj_mod (only parsing).
Notation N_of_nat_pow := Nat2N.inj_pow (only parsing).
Notation N_of_min := Nat2N.inj_min (only parsing).
Notation N_of_max := Nat2N.inj_max (only parsing).