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.

Proof.

intro x; induction x as [p IHp| p IHp| ]; simpl in |- *; auto; intro m;

 rewrite IHp; rewrite plus_assoc; trivial.

Qed.




Lemma nat_of_P_succ_morphism :

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

Proof.

  intro; change (S (nat_of_P p)) with (1 + nat_of_P p) in |- *;

   unfold nat_of_P in |- *; apply Pmult_nat_succ_morphism.

Qed.




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.

Proof.

intro x; induction x as [p IHp| p IHp| ]; intro y;

 [ destruct y as [p0| p0| ]

 | destruct y as [p0| p0| ]

 | destruct y as [p| p| ] ]; simpl in |- *; auto with arith; 

 intro m;

 [ rewrite IHp; rewrite plus_assoc; trivial with arith
 | rewrite IHp; rewrite plus_assoc; trivial with arith
 | rewrite Pmult_nat_succ_morphism; rewrite plus_assoc; trivial with arith
 | rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ].

Qed.




Theorem nat_of_P_plus_carry_morphism :

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

Proof.

intros; unfold nat_of_P in |- *; rewrite Pmult_nat_plus_carry_morphism;

 simpl in |- *; trivial with arith.

Qed.




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.

Proof.

intro x; induction x as [p IHp| p IHp| ]; intro y;

 [ destruct y as [p0| p0| ]

 | destruct y as [p0| p0| ]

 | destruct y as [p| p| ] ]; simpl in |- *; auto with arith;

 [ intros m; rewrite Pmult_nat_plus_carry_morphism; rewrite IHp;
    rewrite plus_assoc_reverse; rewrite plus_assoc_reverse;
    rewrite (plus_permute m (Pmult_nat p (m + m))); 
    trivial with arith
 | intros m; rewrite IHp; apply plus_assoc
 | intros m; rewrite Pmult_nat_succ_morphism;
    rewrite (plus_comm (m + Pmult_nat p (m + m))); 
    apply plus_assoc_reverse
 | intros m; rewrite IHp; apply plus_permute
 | intros m; rewrite Pmult_nat_succ_morphism; apply plus_assoc_reverse ].

Qed.




Theorem nat_of_P_plus_morphism :

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

Proof.

intros x y; exact (Pmult_nat_l_plus_morphism x y 1).

Qed.

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.

Proof.

intro y; induction y as [p H| p H| ]; intro m;

 [ simpl in |- *; rewrite H; rewrite plus_assoc_reverse;
    rewrite (plus_permute m (Pmult_nat p (m + m)));
    rewrite plus_assoc_reverse; auto with arith
 | simpl in |- *; rewrite H; auto with arith
 | simpl in |- *; trivial with arith ].

Qed.




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

Proof.

intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism;

 trivial.

Qed.

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.

Proof.

intros x y; induction x as [x' H| x' H| ];

 [ change (xI x' * y)%positive with (y + xO (x' * y))%positive in |- *;
    rewrite nat_of_P_plus_morphism; unfold nat_of_P at 2 3 in |- *;
    simpl in |- *; do 2 rewrite ZL6; rewrite H; rewrite mult_plus_distr_r;
    reflexivity
 | unfold nat_of_P at 1 2 in |- *; simpl in |- *; do 2 rewrite ZL6; rewrite H;
    rewrite mult_plus_distr_r; reflexivity
 | simpl in |- *; rewrite <- plus_n_O; reflexivity ].

Qed.

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.

Proof.

intro y; induction y as [p H| p H| ];

 [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *;

    simpl in |- *; change 2 with (1 + 1) in |- *;

    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H1; 

    rewrite H1; auto with arith

 | destruct H as [x H2]; exists (x + S x); unfold nat_of_P in |- *;

    simpl in |- *; change 2 with (1 + 1) in |- *;

    rewrite Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; 

    rewrite H2; auto with arith

 | exists 0; auto with arith ].

Qed.

Extra lemmas on lt on Peano natural numbers





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

Proof.

intros m n H; apply lt_trans with (m := m + n);

 [ apply plus_lt_compat_l with (1 := H)

 | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ].

Qed.




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

Proof.

intros m n H; apply le_lt_trans with (m := m + n);

 [ change (m + m < m + n) in |- *; apply plus_lt_compat_l with (1 := H)

 | rewrite (plus_comm m n); apply plus_lt_compat_l with (1 := H) ].

Qed.

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.

Proof.

intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ];

 intro H2;

 [ unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; do 2 rewrite ZL6;

    apply ZL7; apply H; simpl in H2; assumption

 | unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6; apply ZL8;

    apply H; simpl in H2; apply Pcompare_Gt_Lt; assumption

 | simpl in |- *; discriminate H2

 | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;

    elim (Pcompare_Lt_Lt p q H2);

    [ intros H3; apply lt_S; apply ZL7; apply H; apply H3
    | intros E; rewrite E; apply lt_n_Sn ]

 | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;

    apply ZL7; apply H; assumption

 | simpl in |- *; discriminate H2

 | unfold nat_of_P in |- *; simpl in |- *; apply lt_n_S; rewrite ZL6;

    elim (ZL4 q); intros h H3; rewrite H3; simpl in |- *; 

    apply lt_O_Sn

 | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 q);

    intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm;

    apply lt_n_S; apply lt_O_Sn

 | simpl in |- *; discriminate H2 ].

Qed.

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.

Proof.

unfold gt in |- *; intro x; induction x as [p H| p H| ]; intro y;

 destruct y as [q| q| ]; intro H2;

 [ simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;

    apply lt_n_S; apply ZL7; apply H; assumption

 | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;

    elim (Pcompare_Gt_Gt p q H2);

    [ intros H3; apply lt_S; apply ZL7; apply H; assumption
    | intros E; rewrite E; apply lt_n_Sn ]

 | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p);

    intros h H3; rewrite H3; simpl in |- *; apply lt_n_S; 

    apply lt_O_Sn

 | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;

    apply ZL8; apply H; apply Pcompare_Lt_Gt; assumption

 | simpl in |- *; unfold nat_of_P in |- *; simpl in |- *; do 2 rewrite ZL6;

    apply ZL7; apply H; assumption

 | unfold nat_of_P in |- *; simpl in |- *; rewrite ZL6; elim (ZL4 p);

    intros h H3; rewrite H3; simpl in |- *; rewrite <- plus_n_Sm;

    apply lt_n_S; apply lt_O_Sn

 | simpl in |- *; discriminate H2

 | simpl in |- *; discriminate H2

 | simpl in |- *; discriminate H2 ].

Qed.

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.

Proof.

intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq));

 [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H;

    absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ]

 | intros H; elim H;

    [ auto

    | intros H1 H2; absurd (nat_of_P x < nat_of_P y);

       [ apply lt_asym; change (nat_of_P x > nat_of_P y) in |- *;
          apply nat_of_P_gt_Gt_compare_morphism; assumption
       | assumption ] ] ].

Qed.

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.

Proof.

intros x y; unfold gt in |- *; elim (Dcompare ((x ?= y)%positive Eq));

 [ intros E; rewrite (Pcompare_Eq_eq x y E); intros H;

    absurd (nat_of_P y < nat_of_P y); [ apply lt_irrefl | assumption ]

 | intros H; elim H;

    [ intros H1 H2; absurd (nat_of_P y < nat_of_P x);

       [ apply lt_asym; apply nat_of_P_lt_Lt_compare_morphism; assumption
       | assumption ]

    | auto ] ].

Qed.

nat_of_P is strictly positive





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

induction p; simpl in |- *; auto with arith.

intro m; apply le_trans with (m + m); auto with arith.

Qed.




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

intro; unfold nat_of_P in |- *; apply lt_le_trans with 1; auto with arith.

apply le_Pmult_nat.

Qed.

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.

Proof.

  simple induction p. intros. simpl in |- *. rewrite mult_plus_distr_l. rewrite <- (mult_plus_distr_l m n n).

  rewrite (H (n + n) m). reflexivity.

  intros. simpl in |- *. rewrite <- (mult_plus_distr_l m n n). apply H.

  trivial.

Qed.




Lemma Pmult_nat_2_mult_2_permute :

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

Proof.

  intros. rewrite <- Pmult_nat_mult_permute. reflexivity.

Qed.




Lemma Pmult_nat_4_mult_2_permute :

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

Proof.

  intros. rewrite <- Pmult_nat_mult_permute. reflexivity.

Qed.

Mapping of xH, xO and xI through nat_of_P





Lemma nat_of_P_xH : nat_of_P 1 = 1.

Proof.

  reflexivity.

Qed.




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

Proof.

  simple induction p. unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute.

  rewrite Pmult_nat_4_mult_2_permute. rewrite H. simpl in |- *. rewrite <- plus_Snm_nSm. reflexivity.

  unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute.

  rewrite H. reflexivity.

  reflexivity.

Qed.




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

Proof.

  simple induction p. unfold nat_of_P in |- *. simpl in |- *. intro p0. intro. rewrite Pmult_nat_2_mult_2_permute.

  rewrite Pmult_nat_4_mult_2_permute; injection H; intro H1; rewrite H1;

   rewrite <- plus_Snm_nSm; reflexivity.

  unfold nat_of_P in |- *. simpl in |- *. intros. rewrite Pmult_nat_2_mult_2_permute. rewrite Pmult_nat_4_mult_2_permute.

  injection H; intro H1; rewrite H1; reflexivity.

  reflexivity.

Qed.

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.

Proof.

intro m; induction m as [| n H];

 [ reflexivity
 | simpl in |- *; rewrite nat_of_P_succ_morphism; rewrite H; auto ].

Qed.

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

Proof.

intro x; induction x as [| n H];

 [ simpl in |- *; auto with arith
 | simpl in |- *; rewrite plus_comm; simpl in |- *; rewrite H;
    rewrite xO_succ_permute; auto with arith ].

Qed.




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

Proof.

intro x; induction x as [| n H]; simpl in |- *;

 [ auto with arith
 | rewrite <- plus_n_Sm; simpl in |- *; simpl in H; rewrite H;
    auto with arith ].

Qed.

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.

Proof.

intro x; induction x as [p H| p H| ];

 [ simpl in |- *; rewrite <- H; change 2 with (1 + 1) in |- *;
    rewrite Pmult_nat_r_plus_morphism; elim (ZL4 p); 
    unfold nat_of_P in |- *; intros n H1; rewrite H1; 
    rewrite ZL3; auto with arith
 | unfold nat_of_P in |- *; simpl in |- *; change 2 with (1 + 1) in |- *;
    rewrite Pmult_nat_r_plus_morphism;
    rewrite <- (Ppred_succ (P_of_succ_nat (Pmult_nat p 1 + Pmult_nat p 1)));
    rewrite <- (Ppred_succ (xI p)); simpl in |- *; 
    rewrite <- H; elim (ZL4 p); unfold nat_of_P in |- *; 
    intros n H1; rewrite H1; rewrite ZL5; simpl in |- *; 
    trivial with arith
 | unfold nat_of_P in |- *; simpl in |- *; auto with arith ].

Qed.

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.

Proof.

intros x; rewrite P_of_succ_nat_o_nat_of_P_eq_succ; rewrite Ppred_succ;

 trivial with arith.

Qed.

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.

Proof.

intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r;

 [ rewrite <- nat_of_P_plus_morphism; rewrite Pplus_minus; auto with arith
 | apply lt_le_weak; exact (nat_of_P_gt_Gt_compare_morphism x y H) ].

Qed.

nat_of_P is injective





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

Proof.

intros x y H; rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id x);

 rewrite <- (pred_o_P_of_succ_nat_o_nat_of_P_eq_id y); 

 rewrite H; trivial with arith.

Qed.




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

Proof.

intros p q; elim (ZL4 p); elim (ZL4 q); intros h H1 i H2; rewrite H1;

 rewrite H2; simpl in |- *; unfold lt in |- *; apply le_n_S; 

 apply le_minus.

Qed.




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

Proof.

intros p q; rewrite nat_of_P_plus_morphism; unfold lt in |- *; elim (ZL4 q);

 intros k H; rewrite H; rewrite plus_comm; simpl in |- *; 

 apply le_n_S; apply le_plus_r.

Qed.

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.

Proof.

intros; apply nat_of_P_lt_Lt_compare_complement_morphism;

 rewrite nat_of_P_minus_morphism;

 [ rewrite nat_of_P_minus_morphism;

    [ apply plus_lt_reg_l with (p := nat_of_P q); rewrite le_plus_minus_r;

       [ rewrite plus_comm; apply plus_lt_reg_l with (p := nat_of_P p);

          rewrite plus_assoc; rewrite le_plus_minus_r;

          [ rewrite (plus_comm (nat_of_P p)); apply plus_lt_compat_l;
             apply nat_of_P_lt_Lt_compare_morphism; 
             assumption
          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
             apply ZC1; assumption ]

       | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;

          assumption ]

    | assumption ]

 | assumption ].

Qed.




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.

Proof.

intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism;

 rewrite nat_of_P_minus_morphism;

 [ rewrite nat_of_P_minus_morphism;

    [ unfold gt in |- *; apply plus_lt_reg_l with (p := nat_of_P z);

       rewrite le_plus_minus_r;

       [ rewrite le_plus_minus_r;

          [ apply nat_of_P_lt_Lt_compare_morphism; assumption
          | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism;
             apply ZC1; assumption ]

       | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1;

          assumption ]

    | assumption ]

 | assumption ].

Qed.

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.

Proof.

intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_morphism;

 rewrite nat_of_P_minus_morphism;

 [ rewrite nat_of_P_minus_morphism;

    [ do 2 rewrite nat_of_P_mult_morphism;
       do 3 rewrite (mult_comm (nat_of_P x)); apply mult_minus_distr_r
    | apply nat_of_P_gt_Gt_compare_complement_morphism;
       do 2 rewrite nat_of_P_mult_morphism; unfold gt in |- *; 
       elim (ZL4 x); intros h H1; rewrite H1; apply mult_S_lt_compat_l;
       exact (nat_of_P_gt_Gt_compare_morphism y z H) ]

 | assumption ].

Qed.