Library Coq.NArith.Pnat
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.
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
nat_of_P maps to the strictly positive subset of nat
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
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)%positive 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
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)%positive Eq = Gt -> nat_of_P p > nat_of_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
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)%positive 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
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)%positive 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
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
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)%positive Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q.
nat_of_P is injective
Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> 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)%positive Eq = Lt ->
(r ?= p)%positive Eq = Gt ->
(r ?= q)%positive Eq = Gt -> (r - p ?= r - q)%positive Eq = Lt.
Lemma Pcompare_minus_l :
forall p q r:positive,
(q ?= p)%positive Eq = Lt ->
(p ?= r)%positive Eq = Gt ->
(q ?= r)%positive Eq = Gt -> (q - r ?= p - r)%positive Eq = Lt.
Distributivity of multiplication over subtraction
Theorem Pmult_minus_distr_l :
forall p q r:positive,
(q ?= r)%positive Eq = Gt ->
(p * (q - r))%positive = (p * q - p * r)%positive.