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

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.