diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-18 18:02:20 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-11-18 18:02:20 +0000 |
commit | 59726c5343613379d38a9409af044d85cca130ed (patch) | |
tree | 185cef19334e67de344b6417a07c11ad61ed0c46 /theories/PArith/Pnat.v | |
parent | 16cf970765096f55a03efad96100add581ce0edb (diff) |
Some more revision of {P,N,Z}Arith + bitwise ops in Ndigits
Initial plan was only to add shiftl/shiftr/land/... to N and
other number type, this is only partly done, but this work has
diverged into a big reorganisation and improvement session
of PArith,NArith,ZArith.
Bool/Bool: add lemmas orb_diag (a||a = a) and andb_diag (a&&a = a)
PArith/BinPos:
- added a power function Ppow
- iterator iter_pos moved from Zmisc to here + some lemmas
- added Psize_pos, which is 1+log2, used to define Nlog2/Zlog2
- more lemmas on Pcompare and succ/+/* and order, allow
to simplify a lot some old proofs elsewhere.
- new/revised results on Pminus (including some direct proof of
stuff from Pnat)
PArith/Pnat:
- more direct proofs (limit the need of stuff about Pmult_nat).
- provide nicer names for some lemmas (eg. Pplus_plus instead of
nat_of_P_plus_morphism), compatibility notations provided.
- kill some too-specific lemmas unused in stdlib + contribs
NArith/BinNat:
- N_of_nat, nat_of_N moved from Nnat to here.
- a lemma relating Npred and Nminus
- revised definitions and specification proofs of Npow and Nlog2
NArith/Nnat:
- shorter proofs.
- stuff about Z_of_N is moved to Znat. This way, NArith is
entirely independent from ZArith.
NArith/Ndigits:
- added bitwise operations Nand Nor Ndiff Nshiftl Nshiftr
- revised proofs about Nxor, still using functional bit stream
- use the same approach to prove properties of Nand Nor Ndiff
ZArith/BinInt: huge simplification of Zplus_assoc + cosmetic stuff
ZArith/Zcompare: nicer proofs of ugly things like Zcompare_Zplus_compat
ZArith/Znat: some nicer proofs and names, received stuff about Z_of_N
ZArith/Zmisc: almost empty new, only contain stuff about badly-named
iter. Should be reformed more someday.
ZArith/Zlog_def: Zlog2 is now based on Psize_pos, this factorizes
proofs and avoid slowdown due to adding 1 in Z instead of in positive
Zarith/Zpow_def: Zpower_opt is renamed more modestly Zpower_alt
as long as I dont't know why it's slower on powers of two.
Elsewhere: propagate new names + some nicer proofs
NB: Impact on compatibility is probably non-zero, but should be
really moderate. We'll see on contribs, but a few Require here
and there might be necessary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13651 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/PArith/Pnat.v')
-rw-r--r-- | theories/PArith/Pnat.v | 511 |
1 files changed, 149 insertions, 362 deletions
diff --git a/theories/PArith/Pnat.v b/theories/PArith/Pnat.v index b3f2493b2..590217d5d 100644 --- a/theories/PArith/Pnat.v +++ b/theories/PArith/Pnat.v @@ -7,332 +7,199 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -Require Import BinPos. +Require Import BinPos Le Lt Gt Plus Mult Minus Compare_dec Wf_nat. -(**********************************************************************) -(** Properties of the injection from binary positive numbers to Peano - natural numbers *) +(** 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. -Proof. -intro x; induction x as [p IHp| p IHp| ]; simpl in |- *; auto; intro m; - rewrite IHp; rewrite plus_assoc; trivial. -Qed. +(** [Pmult_nat] in term of [nat_of_P] *) -Lemma nat_of_P_succ_morphism : - forall p:positive, nat_of_P (Psucc p) = S (nat_of_P p). +Lemma Pmult_nat_mult : forall p n, + Pmult_nat p n = nat_of_P p * n. 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. + induction p; intros n. + unfold nat_of_P. simpl. f_equal. rewrite 2 IHp. + rewrite <- mult_assoc. f_equal. simpl. now rewrite <- plus_n_O. + unfold nat_of_P. simpl. rewrite 2 IHp. + rewrite <- mult_assoc. f_equal. simpl. now rewrite <- plus_n_O. + simpl. now rewrite <- plus_n_O. 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. +(** [nat_of_P] is a morphism for successor, addition, multiplication *) -Theorem nat_of_P_plus_carry_morphism : - forall p q:positive, nat_of_P (Pplus_carry p q) = S (nat_of_P (p + q)). +Lemma Psucc_S : forall p, nat_of_P (Psucc p) = S (nat_of_P p). Proof. -intros; unfold nat_of_P in |- *; rewrite Pmult_nat_plus_carry_morphism; - simpl in |- *; trivial with arith. + induction p; unfold nat_of_P; simpl; trivial. + now rewrite !Pmult_nat_mult, IHp. 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. +Theorem Pplus_plus : + forall p q, nat_of_P (p + q) = nat_of_P p + nat_of_P q. 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 ]. + induction p using Pind; intros q. + now rewrite <- Pplus_one_succ_l, Psucc_S. + now rewrite Pplus_succ_permute_l, !Psucc_S, IHp. Qed. -Theorem nat_of_P_plus_morphism : - forall p q:positive, nat_of_P (p + q) = nat_of_P p + nat_of_P q. +Theorem Pmult_mult : + forall p q, 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). + induction p using Pind; simpl; intros; trivial. + now rewrite Pmult_Sn_m, Pplus_plus, IHp, Psucc_S. Qed. -(** [Pmult_nat] is a morphism for addition *) +(** Mapping of xH, xO and xI through [nat_of_P] *) -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 nat_of_P_xH : nat_of_P 1 = 1. 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 ]. + reflexivity. Qed. -Lemma ZL6 : forall p:positive, Pmult_nat p 2 = nat_of_P p + nat_of_P p. +Lemma nat_of_P_xO : forall p, nat_of_P (xO p) = 2 * nat_of_P p. Proof. -intro p; change 2 with (1 + 1) in |- *; rewrite Pmult_nat_r_plus_morphism; - trivial. + intros. exact (Pmult_mult 2 p). 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. +Lemma nat_of_P_xI : forall p, nat_of_P (xI p) = S (2 * nat_of_P p). 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 ]. + intros. now rewrite xI_succ_xO, Psucc_S, nat_of_P_xO. 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. +Lemma nat_of_P_is_S : forall p, exists n, nat_of_P p = S n. 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 ]. +induction p as [p (h,IH)| p (h,IH)| ]; unfold nat_of_P; simpl. + exists (S h * 2). now rewrite Pmult_nat_mult, IH. + exists (S (h*2)). now rewrite Pmult_nat_mult,IH. + now exists 0. 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. +(** [nat_of_P] is strictly positive *) -Lemma ZL8 : forall n m:nat, n < m -> S (n + n) < m + m. +Lemma nat_of_P_pos : forall p, 0 < nat_of_P p. 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) ]. + intros p. destruct (nat_of_P_is_S p) as (n,->). auto with arith. Qed. -(** [nat_of_P] is a morphism from [positive] to [nat] for [lt] (expressed - from [compare] on [positive]) +(** [nat_of_P] is a morphism for comparison *) - 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. +Lemma Pcompare_nat_compare : forall p q, + (p ?= q) Eq = nat_compare (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 ]. + induction p as [ |p IH] using Pind; intros q. + destruct (Psucc_pred q) as [Hq|Hq]; [now subst|]. + rewrite <- Hq, Plt_1_succ, Psucc_S, nat_of_P_xH, nat_compare_S. + symmetry. apply nat_compare_lt, nat_of_P_pos. + destruct (Psucc_pred q) as [Hq|Hq]; [subst|]. + rewrite ZC4, Plt_1_succ, Psucc_S. simpl. + symmetry. apply nat_compare_gt, nat_of_P_pos. + now rewrite <- Hq, 2 Psucc_S, Pcompare_succ_succ, IH. Qed. -(** [nat_of_P] is a morphism from [positive] to [nat] for [gt] (expressed - from [compare] on [positive]) +(** [nat_of_P] is hence injective *) - 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. +Lemma nat_of_P_inj_iff : forall p q, nat_of_P p = nat_of_P q <-> p = q. Proof. -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. + intros. + eapply iff_trans; [eapply iff_sym|eapply Pcompare_eq_iff]. + rewrite Pcompare_nat_compare. + apply nat_compare_eq_iff. 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). +Lemma nat_of_P_inj : forall p q, nat_of_P p = nat_of_P q -> 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. + intros. now apply nat_of_P_inj_iff. Qed. -(** [nat_of_P] is hence injective. *) +(** [nat_of_P] is a morphism for [lt], [le], etc *) -Lemma nat_of_P_inj : forall p q:positive, nat_of_P p = nat_of_P q -> p = q. +Lemma Plt_lt : forall p q, Plt p q <-> nat_of_P p < nat_of_P q. Proof. -intros. -apply Pcompare_Eq_eq. -rewrite nat_of_P_compare_morphism. -apply <- nat_compare_eq_iff; auto. + intros. unfold Plt. rewrite Pcompare_nat_compare. + apply iff_sym, nat_compare_lt. Qed. -(** Stating this bidirectionally lets us reason equationally with it: *) - -Lemma nat_of_P_inj_iff : forall p q, nat_of_P p = nat_of_P q <-> p = q. +Lemma Ple_le : forall p q, Ple p q <-> nat_of_P p <= nat_of_P q. Proof. - split; intro. now apply nat_of_P_inj. now subst. + intros. unfold Ple. rewrite Pcompare_nat_compare. + apply iff_sym, nat_compare_le. 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) Eq = Lt. +Lemma Pgt_gt : forall p q, Pgt p q <-> nat_of_P p > nat_of_P q. Proof. - intros. rewrite nat_of_P_compare_morphism. - apply -> nat_compare_lt; auto. + intros. unfold Pgt. rewrite Pcompare_nat_compare. + apply iff_sym, nat_compare_gt. Qed. -(** Again, stating this bidirectionally lets us reason equationally with it: *) - -Lemma Plt_lt : forall p q, Plt p q <-> lt (nat_of_P p) (nat_of_P q). +Lemma Pge_ge : forall p q, Pge p q <-> nat_of_P p >= nat_of_P q. Proof. - intros. unfold Plt. rewrite nat_of_P_compare_morphism. - apply iff_sym, nat_compare_lt. + intros. unfold Pge. rewrite Pcompare_nat_compare. + apply iff_sym, nat_compare_ge. Qed. -(** And the same for Ple *) +(** [nat_of_P] is a morphism for subtraction *) -Lemma Ple_le : forall p q, Ple p q <-> le (nat_of_P p) (nat_of_P q). +Theorem Pminus_minus : + forall p q, Plt q p -> nat_of_P (p - q) = nat_of_P p - nat_of_P q. Proof. - intros. unfold Ple. rewrite nat_of_P_compare_morphism. - apply iff_sym, nat_compare_le. + intros x y H; apply plus_reg_l with (nat_of_P y); rewrite le_plus_minus_r. + rewrite <- Pplus_plus, Pplus_minus. trivial. now apply ZC2. + now apply lt_le_weak, Plt_lt. 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] -*) +(** Results about [Pmult_nat], many are old intermediate results *) -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. +Lemma Pmult_nat_succ_morphism : + forall p n, Pmult_nat (Psucc p) n = n + Pmult_nat p n. Proof. - 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. -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. + intros. now rewrite !Pmult_nat_mult, Psucc_S. 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. +Theorem Pmult_nat_l_plus_morphism : + forall p q n, Pmult_nat (p + q) n = Pmult_nat p n + Pmult_nat q 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. + intros. rewrite !Pmult_nat_mult, Pplus_plus. apply mult_plus_distr_r. Qed. -Lemma Pmult_nat_2_mult_2_permute : - forall p:positive, Pmult_nat p 2 = 2 * Pmult_nat p 1. +Theorem Pmult_nat_plus_carry_morphism : + forall p q n, Pmult_nat (Pplus_carry p q) n = n + Pmult_nat (p + q) n. Proof. - intros. rewrite <- Pmult_nat_mult_permute. reflexivity. + intros. now rewrite Pplus_carry_spec, Pmult_nat_succ_morphism. Qed. -Lemma Pmult_nat_4_mult_2_permute : - forall p:positive, Pmult_nat p 4 = 2 * Pmult_nat p 2. +Lemma Pmult_nat_r_plus_morphism : + forall p n, Pmult_nat p (n + n) = Pmult_nat p n + Pmult_nat p n. Proof. - intros. rewrite <- Pmult_nat_mult_permute. reflexivity. + intros. rewrite !Pmult_nat_mult. apply mult_plus_distr_l. Qed. -(** Mapping of xH, xO and xI through [nat_of_P] *) - -Lemma nat_of_P_xH : nat_of_P 1 = 1. +Lemma ZL6 : forall p, Pmult_nat p 2 = nat_of_P p + nat_of_P p. Proof. - reflexivity. + intros. rewrite Pmult_nat_mult, mult_comm. simpl. now rewrite <- plus_n_O. Qed. -Lemma nat_of_P_xO : forall p:positive, nat_of_P (xO p) = 2 * nat_of_P p. +Lemma le_Pmult_nat : forall p n, n <= Pmult_nat p n. Proof. - intros. - change 2 with (nat_of_P 2). - rewrite <- nat_of_P_mult_morphism. - f_equal. + intros. rewrite Pmult_nat_mult. + apply le_trans with (1*n). now rewrite mult_1_l. + apply mult_le_compat_r. apply nat_of_P_pos. Qed. -Lemma nat_of_P_xI : forall p:positive, nat_of_P (xI p) = S (2 * nat_of_P p). +(** [nat_of_P] is a morphism for [iter_pos] and [iter_nat] *) + +Theorem iter_nat_of_P : + forall p (A:Type) (f:A->A) (x:A), + iter_pos p A f x = iter_nat (nat_of_P p) A f x. Proof. - intros. - change 2 with (nat_of_P 2). - rewrite <- nat_of_P_mult_morphism, <- nat_of_P_succ_morphism. - f_equal. + induction p as [p IH|p IH| ]; intros A f x; simpl; trivial. + f_equal. now rewrite 2 IH, <- iter_nat_plus, <- ZL6. + now rewrite 2 IH, <- iter_nat_plus, <- ZL6. Qed. (**********************************************************************) @@ -341,143 +208,63 @@ Qed. (** 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. -induction n as [|n H]. -reflexivity. -simpl; rewrite nat_of_P_succ_morphism, 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). +Theorem nat_of_P_of_succ_nat : + forall n, nat_of_P (P_of_succ_nat n) = S n. Proof. -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. -induction n as [| n H]; simpl; - [ auto with arith - | rewrite <- plus_n_Sm; simpl; simpl in H; rewrite H; - auto with arith ]. +induction n as [|n H]; trivial; simpl; now rewrite Psucc_S, H. 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. +Theorem P_of_succ_nat_of_P : + forall p, P_of_succ_nat (nat_of_P p) = Psucc p. Proof. intros. -apply nat_of_P_inj. -rewrite nat_of_P_o_P_of_succ_nat_eq_succ, nat_of_P_succ_morphism; auto. +apply nat_of_P_inj. now rewrite nat_of_P_of_succ_nat, Psucc_S. 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. +Theorem Ppred_of_succ_nat_of_P : + forall p, Ppred (P_of_succ_nat (nat_of_P p)) = p. Proof. -intros; rewrite P_of_succ_nat_o_nat_of_P_eq_succ, Ppred_succ; auto. +intros; rewrite P_of_succ_nat_of_P, Ppred_succ; auto. 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) 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. - - -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) 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; - [ 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) 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; - [ 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) 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; - [ 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. +(** Extra properties of the injection from binary positive numbers + to Peano natural numbers *) + +(** Old names and old-style lemmas *) + +Notation nat_of_P_succ_morphism := Psucc_S (only parsing). +Notation nat_of_P_plus_morphism := Pplus_plus (only parsing). +Notation nat_of_P_mult_morphism := Pmult_mult (only parsing). +Notation nat_of_P_compare_morphism := Pcompare_nat_compare (only parsing). +Notation lt_O_nat_of_P := nat_of_P_pos (only parsing). +Notation ZL4 := nat_of_P_is_S (only parsing). +Notation nat_of_P_o_P_of_succ_nat_eq_succ := nat_of_P_of_succ_nat (only parsing). +Notation P_of_succ_nat_o_nat_of_P_eq_succ := P_of_succ_nat_of_P (only parsing). +Notation pred_o_P_of_succ_nat_o_nat_of_P_eq_id := Ppred_of_succ_nat_of_P + (only parsing). + +Definition nat_of_P_minus_morphism p q : + (p ?= q) Eq = Gt -> nat_of_P (p - q) = nat_of_P p - nat_of_P q + := fun H => Pminus_minus p q (ZC1 _ _ H). + +Definition nat_of_P_lt_Lt_compare_morphism p q : + (p ?= q) Eq = Lt -> nat_of_P p < nat_of_P q + := proj1 (Plt_lt p q). + +Definition nat_of_P_gt_Gt_compare_morphism p q : + (p ?= q) Eq = Gt -> nat_of_P p > nat_of_P q + := proj1 (Pgt_gt p q). + +Definition nat_of_P_lt_Lt_compare_complement_morphism p q : + nat_of_P p < nat_of_P q -> (p ?= q) Eq = Lt + := proj2 (Plt_lt p q). + +Definition nat_of_P_gt_Gt_compare_complement_morphism p q : + nat_of_P p > nat_of_P q -> (p ?= q) Eq = Gt + := proj2 (Pgt_gt p q). |