# Library Coq.NArith.Pnat

Require Import BinPos.

Properties of the injection from binary positive numbers to Peano natural numbers

Original development by Pierre CrÃ©gut, CNET, Lannion, France

Require Import Le.
Require Import Lt.
Require Import Gt.
Require Import Plus.
Require Import Mult.
Require Import Minus.
Require Import Compare_dec.

Local Open Scope positive_scope.
Local Open Scope nat_scope.

nat_of_P is a morphism for addition

Lemma Pmult_nat_succ_morphism :
forall (p:positive) (n:nat), Pmult_nat (Psucc p) n = n + Pmult_nat p n.

Lemma nat_of_P_succ_morphism :
forall p:positive, nat_of_P (Psucc p) = S (nat_of_P p).

Theorem Pmult_nat_plus_carry_morphism :
forall (p q:positive) (n:nat),
Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n.

Theorem nat_of_P_plus_carry_morphism :
forall p q:positive, nat_of_P (Pplus_carry p q) = S (nat_of_P (p + q)).

Theorem Pmult_nat_l_plus_morphism :
forall (p q:positive) (n:nat),
Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q n.

Theorem nat_of_P_plus_morphism :
forall p q:positive, nat_of_P (p + q) = nat_of_P p + nat_of_P q.

Pmult_nat is a morphism for addition

Lemma Pmult_nat_r_plus_morphism :
forall (p:positive) (n:nat),
Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n.

Lemma ZL6 : forall p:positive, Pmult_nat p 2 = nat_of_P p + nat_of_P p.

nat_of_P is a morphism for multiplication

Theorem nat_of_P_mult_morphism :
forall p q:positive, nat_of_P (p * q) = nat_of_P p * nat_of_P q.

nat_of_P maps to the strictly positive subset of nat

Lemma ZL4 : forall p:positive, exists h : nat, nat_of_P p = S h.

Extra lemmas on lt on Peano natural numbers

Lemma ZL7 : forall n m:nat, n < m -> n + n < m + m.

Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m.

nat_of_P is a morphism from positive to nat for lt (expressed from compare on positive)

Part 1: lt on positive is finer than lt on nat

Lemma nat_of_P_lt_Lt_compare_morphism :
forall p q:positive, (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q.

nat_of_P is a morphism from positive to nat for gt (expressed from compare on positive)

Part 1: gt on positive is finer than gt on nat

Lemma nat_of_P_gt_Gt_compare_morphism :
forall p q:positive, (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q.

nat_of_P is a morphism for Pcompare and nat_compare

Lemma nat_of_P_compare_morphism : forall p q,
(p ?= q) Eq = nat_compare (nat_of_P p) (nat_of_P q).

nat_of_P is hence injective.

Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q.

nat_of_P is a morphism from positive to nat for lt (expressed from compare on positive)

Part 2: lt on nat is finer than lt on positive
nat_of_P is a morphism from positive to nat for gt (expressed from compare on positive)

Part 2: gt on nat is finer than gt on positive
nat_of_P is strictly positive

Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n.

Lemma lt_O_nat_of_P : forall p:positive, 0 < nat_of_P p.

Pmult_nat permutes with multiplication

Lemma Pmult_nat_mult_permute :
forall (p:positive) (n m:nat), Pmult_nat p (m * n) = m * Pmult_nat p n.

Lemma Pmult_nat_2_mult_2_permute :
forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1.

Lemma Pmult_nat_4_mult_2_permute :
forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2.

Mapping of xH, xO and xI through nat_of_P

Lemma nat_of_P_xH : nat_of_P 1 = 1.

Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p.

Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p).

Properties of the shifted injection from Peano natural numbers to binary positive numbers

Composition of P_of_succ_nat and nat_of_P is successor on nat
Miscellaneous lemmas on P_of_succ_nat

Lemma ZL3 :
forall n:nat, Psucc (P_of_succ_nat (n + n)) = xO (P_of_succ_nat n).

Lemma ZL5 : forall n:nat, P_of_succ_nat (S n + S n) = xI (P_of_succ_nat n).

Composition of nat_of_P and P_of_succ_nat is successor on positive
Composition of nat_of_P, P_of_succ_nat and Ppred is identity on positive
Extra properties of the injection from binary positive numbers to Peano natural numbers

nat_of_P is a morphism for subtraction on positive numbers

Theorem nat_of_P_minus_morphism :
forall p q:positive,
(p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q.

Lemma ZL16 : forall p q:positive, nat_of_P p - nat_of_P q < nat_of_P p.

Lemma ZL17 : forall p q:positive, nat_of_P p < nat_of_P (p + q).

Comparison and subtraction

Lemma Pcompare_minus_r :
forall p q r:positive,
(q ?= p) Eq = Lt ->
(r ?= p) Eq = Gt ->
(r ?= q) Eq = Gt -> (r - p ?= r - q) Eq = Lt.

Lemma Pcompare_minus_l :
forall p q r:positive,
(q ?= p) Eq = Lt ->
(p ?= r) Eq = Gt ->
(q ?= r) Eq = Gt -> (q - r ?= p - r) Eq = Lt.

Distributivity of multiplication over subtraction

Theorem Pmult_minus_distr_l :
forall p q r:positive,
(q ?= r) Eq = Gt ->
(p * (q - r) = p * q - p * r)%positive.