# Library Coq.ZArith.Znat

Binary Integers (Pierre Crégut, CNET, Lannion, France)
Require Export Arith_base.
Require Import BinPos BinInt BinNat Pnat Nnat.
Local Open Scope Z_scope.
Conversions between integers and natural numbers
Seven sections:

- chains of conversions (combining two conversions)
- module N2Z : from N to Z
- module Z2N : from Z to N (negative numbers rounded to 0)
- module Zabs2N : from Z to N (via the absolute value)
- module Nat2Z : from nat to Z
- module Z2Nat : from Z to nat (negative numbers rounded to 0)
- module Zabs2Nat : from Z to nat (via the absolute value)

# Chains of conversions

When combining successive conversions, we have the following commutative diagram:

          ---> Nat ----
         |      ^      |
         |      |      v
        Pos ---------> Z
         |      |      ^
         |      v      |
          ----> N -----

Lemma nat_N_Z n : Z.of_N (N.of_nat n) = Z.of_nat n.
Lemma N_nat_Z n : Z.of_nat (N.to_nat n) = Z.of_N n.
Lemma positive_nat_Z p : Z.of_nat (Pos.to_nat p) = Zpos p.
Lemma positive_N_Z p : Z.of_N (Npos p) = Zpos p.
Lemma positive_N_nat p : N.to_nat (Npos p) = Pos.to_nat p.
Lemma positive_nat_N p : N.of_nat (Pos.to_nat p) = Npos p.
Lemma Z_N_nat n : N.to_nat (Z.to_N n) = Z.to_nat n.
Lemma Z_nat_N n : N.of_nat (Z.to_nat n) = Z.to_N n.
Lemma Zabs_N_nat n : N.to_nat (Z.abs_N n) = Z.abs_nat n.
Lemma Zabs_nat_N n : N.of_nat (Z.abs_nat n) = Z.abs_N n.

# Conversions between Z and N

Module N2Z.
Z.of_N is a bijection between N and non-negative Z, with Z.to_N (or Z.abs_N) as reciprocal. See Z2N.id below for the dual equation.
Lemma id n : Z.to_N (Z.of_N n) = n.
Z.of_N is hence injective
Lemma inj n m : Z.of_N n = Z.of_N m -> n = m.
Lemma inj_iff n m : Z.of_N n = Z.of_N m <-> n = m.
Z.of_N produce non-negative integers
Lemma is_nonneg n : 0 <= Z.of_N n.
Z.of_N, basic equations
Lemma inj_0 : Z.of_N 0 = 0.
Lemma inj_pos p : Z.of_N (Npos p) = Zpos p.
Z.of_N and usual operations.
Lemma inj_compare n m : (Z.of_N n ?= Z.of_N m) = (n ?= m)%N.
Lemma inj_le n m : (n<=m)%N <-> Z.of_N n <= Z.of_N m.
Lemma inj_lt n m : (n<m)%N <-> Z.of_N n < Z.of_N m.
Lemma inj_ge n m : (n>=m)%N <-> Z.of_N n >= Z.of_N m.
Lemma inj_gt n m : (n>m)%N <-> Z.of_N n > Z.of_N m.
Lemma inj_abs_N z : Z.of_N (Z.abs_N z) = Z.abs z.
Lemma inj_add n m : Z.of_N (n+m) = Z.of_N n + Z.of_N m.
Lemma inj_mul n m : Z.of_N (n*m) = Z.of_N n * Z.of_N m.
Lemma inj_sub_max n m : Z.of_N (n-m) = Z.max 0 (Z.of_N n - Z.of_N m).
Lemma inj_sub n m : (m<=n)%N -> Z.of_N (n-m) = Z.of_N n - Z.of_N m.
Lemma inj_succ n : Z.of_N (N.succ n) = Z.succ (Z.of_N n).
Lemma inj_pred_max n : Z.of_N (N.pred n) = Z.max 0 (Z.pred (Z.of_N n)).
Lemma inj_pred n : (0<n)%N -> Z.of_N (N.pred n) = Z.pred (Z.of_N n).
Lemma inj_min n m : Z.of_N (N.min n m) = Z.min (Z.of_N n) (Z.of_N m).
Lemma inj_max n m : Z.of_N (N.max n m) = Z.max (Z.of_N n) (Z.of_N m).
Lemma inj_div n m : Z.of_N (n/m) = Z.of_N n / Z.of_N m.
Lemma inj_mod n m : (m<>0)%N -> Z.of_N (n mod m) = (Z.of_N n) mod (Z.of_N m).
Lemma inj_quot n m : Z.of_N (n/m) = Z.of_N n ÷ Z.of_N m.
Lemma inj_rem n m : Z.of_N (n mod m) = Z.rem (Z.of_N n) (Z.of_N m).
Lemma inj_div2 n : Z.of_N (N.div2 n) = Z.div2 (Z.of_N n).
Lemma inj_quot2 n : Z.of_N (N.div2 n) = Z.quot2 (Z.of_N n).
Lemma inj_pow n m : Z.of_N (n^m) = (Z.of_N n)^(Z.of_N m).
Lemma inj_testbit a n :
Z.testbit (Z.of_N a) (Z.of_N n) = N.testbit a n.
End N2Z.
Module Z2N.
Z.to_N is a bijection between non-negative Z and N, with Pos.of_N as reciprocal. See N2Z.id above for the dual equation.
Lemma id n : 0<=n -> Z.of_N (Z.to_N n) = n.
Z.to_N is hence injective for non-negative integers.
Lemma inj n m : 0<=n -> 0<=m -> Z.to_N n = Z.to_N m -> n = m.
Lemma inj_iff n m : 0<=n -> 0<=m -> (Z.to_N n = Z.to_N m <-> n = m).
Z.to_N, basic equations
Lemma inj_0 : Z.to_N 0 = 0%N.
Lemma inj_pos n : Z.to_N (Zpos n) = Npos n.
Lemma inj_neg n : Z.to_N (Zneg n) = 0%N.
Z.to_N and operations
Lemma inj_add n m : 0<=n -> 0<=m -> Z.to_N (n+m) = (Z.to_N n + Z.to_N m)%N.
Lemma inj_mul n m : 0<=n -> 0<=m -> Z.to_N (n*m) = (Z.to_N n * Z.to_N m)%N.
Lemma inj_succ n : 0<=n -> Z.to_N (Z.succ n) = N.succ (Z.to_N n).
Lemma inj_sub n m : 0<=m -> Z.to_N (n - m) = (Z.to_N n - Z.to_N m)%N.
Lemma inj_pred n : Z.to_N (Z.pred n) = N.pred (Z.to_N n).
Lemma inj_compare n m : 0<=n -> 0<=m ->
(Z.to_N n ?= Z.to_N m)%N = (n ?= m).
Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.to_N n <= Z.to_N m)%N).
Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.to_N n < Z.to_N m)%N).
Lemma inj_min n m : Z.to_N (Z.min n m) = N.min (Z.to_N n) (Z.to_N m).
Lemma inj_max n m : Z.to_N (Z.max n m) = N.max (Z.to_N n) (Z.to_N m).
Lemma inj_div n m : 0<=n -> 0<=m -> Z.to_N (n/m) = (Z.to_N n / Z.to_N m)%N.
Lemma inj_mod n m : 0<=n -> 0<m ->
Z.to_N (n mod m) = ((Z.to_N n) mod (Z.to_N m))%N.
Lemma inj_quot n m : 0<=n -> 0<=m -> Z.to_N (n÷m) = (Z.to_N n / Z.to_N m)%N.
Lemma inj_rem n m :0<=n -> 0<=m ->
Z.to_N (Z.rem n m) = ((Z.to_N n) mod (Z.to_N m))%N.
Lemma inj_div2 n : Z.to_N (Z.div2 n) = N.div2 (Z.to_N n).
Lemma inj_quot2 n : Z.to_N (Z.quot2 n) = N.div2 (Z.to_N n).
Lemma inj_pow n m : 0<=n -> 0<=m -> Z.to_N (n^m) = ((Z.to_N n)^(Z.to_N m))%N.
Lemma inj_testbit a n : 0<=n ->
Z.testbit (Z.of_N a) n = N.testbit a (Z.to_N n).
End Z2N.
Module Zabs2N.
Results about Z.abs_N, converting absolute values of Z integers to N.
Lemma abs_N_spec n : Z.abs_N n = Z.to_N (Z.abs n).
Lemma abs_N_nonneg n : 0<=n -> Z.abs_N n = Z.to_N n.
Lemma id_abs n : Z.of_N (Z.abs_N n) = Z.abs n.
Lemma id n : Z.abs_N (Z.of_N n) = n.
Z.abs_N, basic equations
Lemma inj_0 : Z.abs_N 0 = 0%N.
Lemma inj_pos p : Z.abs_N (Zpos p) = Npos p.
Lemma inj_neg p : Z.abs_N (Zneg p) = Npos p.
Z.abs_N and usual operations, with non-negative integers
Lemma inj_opp n : Z.abs_N (-n) = Z.abs_N n.
Lemma inj_succ n : 0<=n -> Z.abs_N (Z.succ n) = N.succ (Z.abs_N n).
Lemma inj_add n m : 0<=n -> 0<=m -> Z.abs_N (n+m) = (Z.abs_N n + Z.abs_N m)%N.
Lemma inj_mul n m : Z.abs_N (n*m) = (Z.abs_N n * Z.abs_N m)%N.
Lemma inj_sub n m : 0<=m<=n -> Z.abs_N (n-m) = (Z.abs_N n - Z.abs_N m)%N.
Lemma inj_pred n : 0<n -> Z.abs_N (Z.pred n) = N.pred (Z.abs_N n).
Lemma inj_compare n m : 0<=n -> 0<=m ->
(Z.abs_N n ?= Z.abs_N m)%N = (n ?= m).
Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.abs_N n <= Z.abs_N m)%N).
Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.abs_N n < Z.abs_N m)%N).
Lemma inj_min n m : 0<=n -> 0<=m ->
Z.abs_N (Z.min n m) = N.min (Z.abs_N n) (Z.abs_N m).
Lemma inj_max n m : 0<=n -> 0<=m ->
Z.abs_N (Z.max n m) = N.max (Z.abs_N n) (Z.abs_N m).
Lemma inj_quot n m : Z.abs_N (n÷m) = ((Z.abs_N n) / (Z.abs_N m))%N.
Lemma inj_rem n m : Z.abs_N (Z.rem n m) = ((Z.abs_N n) mod (Z.abs_N m))%N.
Lemma inj_pow n m : 0<=m -> Z.abs_N (n^m) = ((Z.abs_N n)^(Z.abs_N m))%N.
Z.abs_N and usual operations, statements with Z.abs
Lemma inj_succ_abs n : Z.abs_N (Z.succ (Z.abs n)) = N.succ (Z.abs_N n).
Lemma inj_add_abs n m :
Z.abs_N (Z.abs n + Z.abs m) = (Z.abs_N n + Z.abs_N m)%N.
Lemma inj_mul_abs n m :
Z.abs_N (Z.abs n * Z.abs m) = (Z.abs_N n * Z.abs_N m)%N.
End Zabs2N.

# Conversions between Z and nat

Module Nat2Z.
Z.of_nat, basic equations
Lemma inj_0 : Z.of_nat 0 = 0.
Lemma inj_succ n : Z.of_nat (S n) = Z.succ (Z.of_nat n).
Z.of_N produce non-negative integers
Lemma is_nonneg n : 0 <= Z.of_nat n.
Z.of_nat is a bijection between nat and non-negative Z, with Z.to_nat (or Z.abs_nat) as reciprocal. See Z2Nat.id below for the dual equation.
Lemma id n : Z.to_nat (Z.of_nat n) = n.
Z.of_nat is hence injective
Lemma inj n m : Z.of_nat n = Z.of_nat m -> n = m.
Lemma inj_iff n m : Z.of_nat n = Z.of_nat m <-> n = m.
Z.of_nat and usual operations
Lemma inj_compare n m : (Z.of_nat n ?= Z.of_nat m) = nat_compare n m.
Lemma inj_le n m : (n<=m)%nat <-> Z.of_nat n <= Z.of_nat m.
Lemma inj_lt n m : (n<m)%nat <-> Z.of_nat n < Z.of_nat m.
Lemma inj_ge n m : (n>=m)%nat <-> Z.of_nat n >= Z.of_nat m.
Lemma inj_gt n m : (n>m)%nat <-> Z.of_nat n > Z.of_nat m.
Lemma inj_abs_nat z : Z.of_nat (Z.abs_nat z) = Z.abs z.
Lemma inj_add n m : Z.of_nat (n+m) = Z.of_nat n + Z.of_nat m.
Lemma inj_mul n m : Z.of_nat (n*m) = Z.of_nat n * Z.of_nat m.
Lemma inj_sub_max n m : Z.of_nat (n-m) = Z.max 0 (Z.of_nat n - Z.of_nat m).
Lemma inj_sub n m : (m<=n)%nat -> Z.of_nat (n-m) = Z.of_nat n - Z.of_nat m.
Lemma inj_pred_max n : Z.of_nat (pred n) = Z.max 0 (Z.pred (Z.of_nat n)).
Lemma inj_pred n : (0<n)%nat -> Z.of_nat (pred n) = Z.pred (Z.of_nat n).
Lemma inj_min n m : Z.of_nat (min n m) = Z.min (Z.of_nat n) (Z.of_nat m).
Lemma inj_max n m : Z.of_nat (max n m) = Z.max (Z.of_nat n) (Z.of_nat m).
End Nat2Z.
Module Z2Nat.
Z.to_nat is a bijection between non-negative Z and nat, with Pos.of_nat as reciprocal. See nat2Z.id above for the dual equation.
Lemma id n : 0<=n -> Z.of_nat (Z.to_nat n) = n.
Z.to_nat is hence injective for non-negative integers.
Lemma inj n m : 0<=n -> 0<=m -> Z.to_nat n = Z.to_nat m -> n = m.
Lemma inj_iff n m : 0<=n -> 0<=m -> (Z.to_nat n = Z.to_nat m <-> n = m).
Z.to_nat, basic equations
Lemma inj_0 : Z.to_nat 0 = O.
Lemma inj_pos n : Z.to_nat (Zpos n) = Pos.to_nat n.
Lemma inj_neg n : Z.to_nat (Zneg n) = O.
Z.to_nat and operations
Lemma inj_add n m : 0<=n -> 0<=m ->
Z.to_nat (n+m) = (Z.to_nat n + Z.to_nat m)%nat.
Lemma inj_mul n m : 0<=n -> 0<=m ->
Z.to_nat (n*m) = (Z.to_nat n * Z.to_nat m)%nat.
Lemma inj_succ n : 0<=n -> Z.to_nat (Z.succ n) = S (Z.to_nat n).
Lemma inj_sub n m : 0<=m -> Z.to_nat (n - m) = (Z.to_nat n - Z.to_nat m)%nat.
Lemma inj_pred n : Z.to_nat (Z.pred n) = pred (Z.to_nat n).
Lemma inj_compare n m : 0<=n -> 0<=m ->
nat_compare (Z.to_nat n) (Z.to_nat m) = (n ?= m).
Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.to_nat n <= Z.to_nat m)%nat).
Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.to_nat n < Z.to_nat m)%nat).
Lemma inj_min n m : Z.to_nat (Z.min n m) = min (Z.to_nat n) (Z.to_nat m).
Lemma inj_max n m : Z.to_nat (Z.max n m) = max (Z.to_nat n) (Z.to_nat m).
End Z2Nat.
Module Zabs2Nat.
Results about Z.abs_nat, converting absolute values of Z integers to nat.
Lemma abs_nat_spec n : Z.abs_nat n = Z.to_nat (Z.abs n).
Lemma abs_nat_nonneg n : 0<=n -> Z.abs_nat n = Z.to_nat n.
Lemma id_abs n : Z.of_nat (Z.abs_nat n) = Z.abs n.
Lemma id n : Z.abs_nat (Z.of_nat n) = n.
Z.abs_nat, basic equations
Lemma inj_0 : Z.abs_nat 0 = 0%nat.
Lemma inj_pos p : Z.abs_nat (Zpos p) = Pos.to_nat p.
Lemma inj_neg p : Z.abs_nat (Zneg p) = Pos.to_nat p.
Z.abs_nat and usual operations, with non-negative integers
Lemma inj_succ n : 0<=n -> Z.abs_nat (Z.succ n) = S (Z.abs_nat n).
Lemma inj_add n m : 0<=n -> 0<=m ->
Z.abs_nat (n+m) = (Z.abs_nat n + Z.abs_nat m)%nat.
Lemma inj_mul n m : Z.abs_nat (n*m) = (Z.abs_nat n * Z.abs_nat m)%nat.
Lemma inj_sub n m : 0<=m<=n ->
Z.abs_nat (n-m) = (Z.abs_nat n - Z.abs_nat m)%nat.
Lemma inj_pred n : 0<n -> Z.abs_nat (Z.pred n) = pred (Z.abs_nat n).
Lemma inj_compare n m : 0<=n -> 0<=m ->
nat_compare (Z.abs_nat n) (Z.abs_nat m) = (n ?= m).
Lemma inj_le n m : 0<=n -> 0<=m -> (n<=m <-> (Z.abs_nat n <= Z.abs_nat m)%nat).
Lemma inj_lt n m : 0<=n -> 0<=m -> (n<m <-> (Z.abs_nat n < Z.abs_nat m)%nat).
Lemma inj_min n m : 0<=n -> 0<=m ->
Z.abs_nat (Z.min n m) = min (Z.abs_nat n) (Z.abs_nat m).
Lemma inj_max n m : 0<=n -> 0<=m ->
Z.abs_nat (Z.max n m) = max (Z.abs_nat n) (Z.abs_nat m).
Z.abs_nat and usual operations, statements with Z.abs
Lemma inj_succ_abs n : Z.abs_nat (Z.succ (Z.abs n)) = S (Z.abs_nat n).
Lemma inj_add_abs n m :
Z.abs_nat (Z.abs n + Z.abs m) = (Z.abs_nat n + Z.abs_nat m)%nat.
Lemma inj_mul_abs n m :
Z.abs_nat (Z.abs n * Z.abs m) = (Z.abs_nat n * Z.abs_nat m)%nat.
End Zabs2Nat.
Compatibility
Definition neq (x y:nat) := x <> y.
Lemma inj_neq n m : neq n m -> Zne (Z.of_nat n) (Z.of_nat m).
Lemma Zpos_P_of_succ_nat n : Zpos (Pos.of_succ_nat n) = Z.succ (Z.of_nat n).
For these one, used in omega, a Definition is necessary
Definition inj_eq := (f_equal Z.of_nat).
Definition inj_le n m := proj1 (Nat2Z.inj_le n m).
Definition inj_lt n m := proj1 (Nat2Z.inj_lt n m).
Definition inj_ge n m := proj1 (Nat2Z.inj_ge n m).
Definition inj_gt n m := proj1 (Nat2Z.inj_gt n m).
For the others, a Notation is fine
Notation inj_0 := Nat2Z.inj_0 (compat "8.3").
Notation inj_S := Nat2Z.inj_succ (compat "8.3").
Notation inj_compare := Nat2Z.inj_compare (compat "8.3").
Notation inj_eq_rev := Nat2Z.inj (compat "8.3").
Notation inj_eq_iff := (fun n m => iff_sym (Nat2Z.inj_iff n m)) (compat "8.3").
Notation inj_le_iff := Nat2Z.inj_le (compat "8.3").
Notation inj_lt_iff := Nat2Z.inj_lt (compat "8.3").
Notation inj_ge_iff := Nat2Z.inj_ge (compat "8.3").
Notation inj_gt_iff := Nat2Z.inj_gt (compat "8.3").
Notation inj_le_rev := (fun n m => proj2 (Nat2Z.inj_le n m)) (compat "8.3").
Notation inj_lt_rev := (fun n m => proj2 (Nat2Z.inj_lt n m)) (compat "8.3").
Notation inj_ge_rev := (fun n m => proj2 (Nat2Z.inj_ge n m)) (compat "8.3").
Notation inj_gt_rev := (fun n m => proj2 (Nat2Z.inj_gt n m)) (compat "8.3").
Notation inj_plus := Nat2Z.inj_add (compat "8.3").
Notation inj_mult := Nat2Z.inj_mul (compat "8.3").
Notation inj_minus1 := Nat2Z.inj_sub (compat "8.3").
Notation inj_minus := Nat2Z.inj_sub_max (compat "8.3").
Notation inj_min := Nat2Z.inj_min (compat "8.3").
Notation inj_max := Nat2Z.inj_max (compat "8.3").
Notation Z_of_nat_of_P := positive_nat_Z (compat "8.3").
Notation Zpos_eq_Z_of_nat_o_nat_of_P :=
(fun p => eq_sym (positive_nat_Z p)) (compat "8.3").
Notation Z_of_nat_of_N := N_nat_Z (compat "8.3").
Notation Z_of_N_of_nat := nat_N_Z (compat "8.3").
Notation Z_of_N_eq := (f_equal Z.of_N) (compat "8.3").
Notation Z_of_N_eq_rev := N2Z.inj (compat "8.3").
Notation Z_of_N_eq_iff := (fun n m => iff_sym (N2Z.inj_iff n m)) (compat "8.3").
Notation Z_of_N_compare := N2Z.inj_compare (compat "8.3").
Notation Z_of_N_le_iff := N2Z.inj_le (compat "8.3").
Notation Z_of_N_lt_iff := N2Z.inj_lt (compat "8.3").
Notation Z_of_N_ge_iff := N2Z.inj_ge (compat "8.3").
Notation Z_of_N_gt_iff := N2Z.inj_gt (compat "8.3").
Notation Z_of_N_le := (fun n m => proj1 (N2Z.inj_le n m)) (compat "8.3").
Notation Z_of_N_lt := (fun n m => proj1 (N2Z.inj_lt n m)) (compat "8.3").
Notation Z_of_N_ge := (fun n m => proj1 (N2Z.inj_ge n m)) (compat "8.3").
Notation Z_of_N_gt := (fun n m => proj1 (N2Z.inj_gt n m)) (compat "8.3").
Notation Z_of_N_le_rev := (fun n m => proj2 (N2Z.inj_le n m)) (compat "8.3").
Notation Z_of_N_lt_rev := (fun n m => proj2 (N2Z.inj_lt n m)) (compat "8.3").
Notation Z_of_N_ge_rev := (fun n m => proj2 (N2Z.inj_ge n m)) (compat "8.3").
Notation Z_of_N_gt_rev := (fun n m => proj2 (N2Z.inj_gt n m)) (compat "8.3").
Notation Z_of_N_pos := N2Z.inj_pos (compat "8.3").
Notation Z_of_N_abs := N2Z.inj_abs_N (compat "8.3").
Notation Z_of_N_le_0 := N2Z.is_nonneg (compat "8.3").
Notation Z_of_N_plus := N2Z.inj_add (compat "8.3").
Notation Z_of_N_mult := N2Z.inj_mul (compat "8.3").
Notation Z_of_N_minus := N2Z.inj_sub_max (compat "8.3").
Notation Z_of_N_succ := N2Z.inj_succ (compat "8.3").
Notation Z_of_N_min := N2Z.inj_min (compat "8.3").
Notation Z_of_N_max := N2Z.inj_max (compat "8.3").
Notation Zabs_of_N := Zabs2N.id (compat "8.3").
Notation Zabs_N_succ_abs := Zabs2N.inj_succ_abs (compat "8.3").
Notation Zabs_N_succ := Zabs2N.inj_succ (compat "8.3").
Notation Zabs_N_plus_abs := Zabs2N.inj_add_abs (compat "8.3").
Notation Zabs_N_plus := Zabs2N.inj_add (compat "8.3").
Notation Zabs_N_mult_abs := Zabs2N.inj_mul_abs (compat "8.3").
Notation Zabs_N_mult := Zabs2N.inj_mul (compat "8.3").
Theorem inj_minus2 : forall n m:nat, (m > n)%nat -> Z.of_nat (n - m) = 0.