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.

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)%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

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

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

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

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)%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.