diff options
Diffstat (limited to 'theories/NArith/Pnat.v')
| -rw-r--r-- | theories/NArith/Pnat.v | 193 |
1 files changed, 85 insertions, 108 deletions
diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index 2c007398..0891dea2 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -1,3 +1,4 @@ +(* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) @@ -6,12 +7,12 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Pnat.v 9883 2007-06-07 18:44:59Z letouzey $ i*) +(*i $Id$ i*) Require Import BinPos. (**********************************************************************) -(** Properties of the injection from binary positive numbers to Peano +(** Properties of the injection from binary positive numbers to Peano natural numbers *) (** Original development by Pierre Crégut, CNET, Lannion, France *) @@ -22,6 +23,10 @@ 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 *) @@ -46,7 +51,7 @@ 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; + | 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 @@ -71,11 +76,11 @@ intro x; induction x as [p IHp| p IHp| ]; intro y; | 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))); + 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))); + 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 ]. @@ -106,7 +111,7 @@ 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 : @@ -129,11 +134,11 @@ 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 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 Pmult_nat_r_plus_morphism; unfold nat_of_P in H2; rewrite H2; auto with arith | exists 0; auto with arith ]. Qed. @@ -161,7 +166,7 @@ Qed. *) 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. + forall p q:positive, (p ?= q) 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; @@ -178,7 +183,7 @@ intro x; induction x as [p H| p H| ]; intro y; destruct y as [q| q| ]; 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 |- *; + 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; @@ -193,29 +198,35 @@ Qed. *) 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. + forall p q:positive, (p ?= q) 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 ]. +intros p q GT. unfold gt. +apply nat_of_P_lt_Lt_compare_morphism. +change ((q ?= p) (CompOpp Eq) = CompOpp Gt). +rewrite <- Pcompare_antisym, GT; auto. +Qed. + +(** [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). +Proof. + intros p q; symmetry. + destruct ((p ?= q) Eq) as [ | | ]_eqn. + rewrite (Pcompare_Eq_eq p q); auto. + apply <- nat_compare_eq_iff; auto. + apply -> nat_compare_lt. apply nat_of_P_lt_Lt_compare_morphism; auto. + apply -> nat_compare_gt. apply nat_of_P_gt_Gt_compare_morphism; auto. +Qed. + +(** [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. +Proof. +intros. +apply Pcompare_Eq_eq. +rewrite nat_of_P_compare_morphism. +apply <- nat_compare_eq_iff; auto. Qed. (** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed @@ -225,17 +236,10 @@ Qed. *) 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. + forall p q:positive, nat_of_P p < nat_of_P q -> (p ?= q) 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 ] ] ]. + intros. rewrite nat_of_P_compare_morphism. + apply -> nat_compare_lt; auto. Qed. (** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed @@ -245,18 +249,13 @@ Qed. *) 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. + forall p q:positive, nat_of_P p > nat_of_P q -> (p ?= q) 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 ] ]. + intros. rewrite nat_of_P_compare_morphism. + apply -> nat_compare_gt; auto. Qed. + (** [nat_of_P] is strictly positive *) Lemma le_Pmult_nat : forall (p:positive) (n:nat), n <= Pmult_nat p n. @@ -301,25 +300,22 @@ 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. + intros. + change 2 with (nat_of_P 2). + rewrite <- nat_of_P_mult_morphism. + f_equal. 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. + intros. + change 2 with (nat_of_P 2). + rewrite <- nat_of_P_mult_morphism, <- nat_of_P_succ_morphism. + f_equal. Qed. (**********************************************************************) -(** Properties of the shifted injection from Peano natural numbers to +(** 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] *) @@ -327,9 +323,9 @@ Qed. 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 ]. +induction n as [|n H]. +reflexivity. +simpl; rewrite nat_of_P_succ_morphism, H; auto. Qed. (** Miscellaneous lemmas on [P_of_succ_nat] *) @@ -337,17 +333,17 @@ Qed. 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; +induction n as [| n H]; simpl; + [ auto with arith + | rewrite plus_comm; simpl; 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 |- *; +induction n as [| n H]; simpl; [ auto with arith - | rewrite <- plus_n_Sm; simpl in |- *; simpl in H; rewrite H; + | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H; auto with arith ]. Qed. @@ -356,19 +352,9 @@ Qed. 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 ]. +intros. +apply nat_of_P_inj. +rewrite nat_of_P_o_P_of_succ_nat_eq_succ, nat_of_P_succ_morphism; auto. Qed. (** Composition of [nat_of_P], [P_of_succ_nat] and [Ppred] is identity @@ -377,45 +363,36 @@ Qed. 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. +intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ, Ppred_succ; auto. Qed. (**********************************************************************) -(** Extra properties of the injection from binary positive numbers to Peano +(** 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. + (p ?= q) 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; + 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 |- *; + intros k H; rewrite H; rewrite plus_comm; simpl in |- *; apply le_n_S; apply le_plus_r. Qed. @@ -423,9 +400,9 @@ Qed. 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. + (q ?= p) Eq = Lt -> + (r ?= p) Eq = Gt -> + (r ?= q) Eq = Gt -> (r - p ?= r - q) Eq = Lt. Proof. intros; apply nat_of_P_lt_Lt_compare_complement_morphism; rewrite nat_of_P_minus_morphism; @@ -434,7 +411,7 @@ intros; apply nat_of_P_lt_Lt_compare_complement_morphism; [ 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; + apply nat_of_P_lt_Lt_compare_morphism; assumption | apply lt_le_weak; apply nat_of_P_lt_Lt_compare_morphism; apply ZC1; assumption ] @@ -446,9 +423,9 @@ 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. + (q ?= p) Eq = Lt -> + (p ?= r) Eq = Gt -> + (q ?= r) Eq = Gt -> (q - r ?= p - r) Eq = Lt. Proof. intros p q z; intros; apply nat_of_P_lt_Lt_compare_complement_morphism; rewrite nat_of_P_minus_morphism; @@ -469,8 +446,8 @@ Qed. Theorem Pmult_minus_distr_l : forall p q r:positive, - (q ?= r)%positive Eq = Gt -> - (p * (q - r))%positive = (p * q - p * r)%positive. + (q ?= r) Eq = Gt -> + (p * (q - r) = 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; @@ -478,7 +455,7 @@ intros x y z H; apply nat_of_P_inj; rewrite nat_of_P_mult_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 |- *; + 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 ]. |