# 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
Lemma nat_of_P_lt_Lt_compare_complement_morphism :
forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt.
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
Lemma nat_of_P_gt_Gt_compare_complement_morphism :
forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt.
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
Theorem nat_of_P_o_P_of_succ_nat_eq_succ :
forall n:nat, nat_of_P (P_of_succ_nat n) = S n.
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
Theorem P_of_succ_nat_o_nat_of_P_eq_succ :
forall p:positive, P_of_succ_nat (nat_of_P p) = Psucc p.
Composition of nat_of_P, P_of_succ_nat and Ppred is identity on positive
Theorem pred_o_P_of_succ_nat_o_nat_of_P_eq_id :
forall p:positive, Ppred (P_of_succ_nat (nat_of_P p)) = p.
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.