Library Coq.NArith.Nnat

Require Import Arith_base Compare_dec Sumbool Div2 Min Max.
Require Import BinPos BinNat Pnat.

Conversions from N to nat

Module N2Nat.

N.to_nat is a bijection between N and nat, with Pos.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

Lemma inj a a´ : N.to_nat a = N.to_nat a´ -> a = a´.

Lemma inj_iff a a´ : N.to_nat a = N.to_nat a´ <-> a = a´.

Interaction of this translation and usual operations.

Lemma inj_double a : N.to_nat (N.double a) = 2*(N.to_nat a ).

Lemma inj_succ_double a : N.to_nat (N.succ_double a) = S (2*(N.to_nat a )).

Lemma inj_succ a : N.to_nat (N.succ a) = S (N.to_nat a).

Lemma inj_add a a´ :
  N.to_nat (a + a´) = N.to_nat a + N.to_nat a´.

Lemma inj_mul a a´ :
  N.to_nat (a * a´) = N.to_nat a * N.to_nat a´.

Lemma inj_sub a a´ :
  N.to_nat (a - a´) = N.to_nat a - N.to_nat a´.

Lemma inj_pred a : N.to_nat (N.pred a) = pred (N.to_nat a).

Lemma inj_div2 a : N.to_nat (N.div2 a) = div2 (N.to_nat a).

Lemma inj_compare a a´ :
(a ?= a´)%N = nat_compare (N.to_nat a) (N.to_nat a´).

Lemma inj_max a a´ :
  N.to_nat (N.max a a´) = max (N.to_nat a) (N.to_nat a´).

Lemma inj_min a a´ :
  N.to_nat (N.min a a´) = min (N.to_nat a) (N.to_nat a´).

Lemma inj_iter a {A} (f:A->A) (x:A) :
  N.iter a f x = nat_iter (N.to_nat a) f x.

End N2Nat.

Hint Rewrite N2Nat.inj_double N2Nat.inj_succ_double
N2Nat.inj_succ N2Nat.inj_add N2Nat.inj_mul N2Nat.inj_sub
N2Nat.inj_pred N2Nat.inj_div2 N2Nat.inj_max N2Nat.inj_min
N2Nat.id
: Nnat.

Conversions from nat to N

Module Nat2N.

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

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

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

N.of_nat is hence injective

Lemma inj n n´ : N.of_nat n = N.of_nat n´ -> n = n´.

Lemma inj_iff n n´ : N.of_nat n = N.of_nat n´ <-> n = n´.

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 (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 (div2 n) = N.div2 (N.of_nat n).

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

Lemma inj_min n n´ :
  N.of_nat (min n n´) = N.min (N.of_nat n) (N.of_nat n´).

Lemma inj_max n n´ :
  N.of_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.

Hint Rewrite Nat2N.id : Nnat.

Compatibility notations

Notation nat_of_N_inj := N2Nat.inj (compat "8.3").
Notation N_of_nat_of_N := N2Nat.id (compat "8.3").
Notation nat_of_Ndouble := N2Nat.inj_double (compat "8.3").
Notation nat_of_Ndouble_plus_one := N2Nat.inj_succ_double (compat "8.3").
Notation nat_of_Nsucc := N2Nat.inj_succ (compat "8.3").
Notation nat_of_Nplus := N2Nat.inj_add (compat "8.3").
Notation nat_of_Nmult := N2Nat.inj_mul (compat "8.3").
Notation nat_of_Nminus := N2Nat.inj_sub (compat "8.3").
Notation nat_of_Npred := N2Nat.inj_pred (compat "8.3").
Notation nat_of_Ndiv2 := N2Nat.inj_div2 (compat "8.3").
Notation nat_of_Ncompare := N2Nat.inj_compare (compat "8.3").
Notation nat_of_Nmax := N2Nat.inj_max (compat "8.3").
Notation nat_of_Nmin := N2Nat.inj_min (compat "8.3").

Notation nat_of_N_of_nat := Nat2N.id (compat "8.3").
Notation N_of_nat_inj := Nat2N.inj (compat "8.3").
Notation N_of_double := Nat2N.inj_double (compat "8.3").
Notation N_of_double_plus_one := Nat2N.inj_succ_double (compat "8.3").
Notation N_of_S := Nat2N.inj_succ (compat "8.3").
Notation N_of_pred := Nat2N.inj_pred (compat "8.3").
Notation N_of_plus := Nat2N.inj_add (compat "8.3").
Notation N_of_minus := Nat2N.inj_sub (compat "8.3").
Notation N_of_mult := Nat2N.inj_mul (compat "8.3").
Notation N_of_div2 := Nat2N.inj_div2 (compat "8.3").
Notation N_of_nat_compare := Nat2N.inj_compare (compat "8.3").
Notation N_of_min := Nat2N.inj_min (compat "8.3").
Notation N_of_max := Nat2N.inj_max (compat "8.3").