diff options
Diffstat (limited to 'theories/NArith')
| -rw-r--r-- | theories/NArith/Ndec.v | 29 | ||||
| -rw-r--r-- | theories/NArith/Nnat.v | 30 | ||||
| -rw-r--r-- | theories/NArith/Pnat.v | 162 |
3 files changed, 108 insertions, 113 deletions
diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index bbab81f4e..e9bc4b266 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -354,6 +354,35 @@ Proof. trivial. Qed. +(* Nleb and Ncompare *) + +(* NB: No need to prove that Nleb a b = true <-> Ncompare a b <> Gt, + this statement is in fact Nleb_Nle! *) + +Lemma Nltb_Ncompare : forall a b, + Nleb a b = false <-> Ncompare a b = Gt. +Proof. + intros. + assert (IFF : forall x:bool, x = false <-> ~ x = true) + by (destruct x; intuition). + rewrite IFF, Nleb_Nle; unfold Nle. + destruct (Ncompare a b); split; intro H; auto; + elim H; discriminate. +Qed. + +Lemma Ncompare_Gt_Nltb : forall a b, + Ncompare a b = Gt -> Nleb a b = false. +Proof. + intros; apply <- Nltb_Ncompare; auto. +Qed. + +Lemma Ncompare_Lt_Nltb : forall a b, + Ncompare a b = Lt -> Nleb b a = false. +Proof. + intros a b H. + rewrite Nltb_Ncompare, <- Ncompare_antisym, H; auto. +Qed. + (* An alternate [min] function over [N] *) Definition Nmin' (a b:N) := if Nleb a b then a else b. diff --git a/theories/NArith/Nnat.v b/theories/NArith/Nnat.v index 98b482bc9..36a1f1d8f 100644 --- a/theories/NArith/Nnat.v +++ b/theories/NArith/Nnat.v @@ -179,22 +179,12 @@ Lemma nat_of_Ncompare : forall a a', Ncompare a a' = nat_compare (nat_of_N a) (nat_of_N a'). Proof. destruct a; destruct a'; simpl. - compute; auto. - generalize (lt_O_nat_of_P p). - unfold nat_compare. - destruct (lt_eq_lt_dec 0 (nat_of_P p)) as [[H|H]|H]; auto. - rewrite <- H; inversion 1. - intros; generalize (lt_trans _ _ _ H0 H); inversion 1. - generalize (lt_O_nat_of_P p). - unfold nat_compare. - destruct (lt_eq_lt_dec (nat_of_P p) 0) as [[H|H]|H]; auto. - intros; generalize (lt_trans _ _ _ H0 H); inversion 1. - rewrite H; inversion 1. - unfold nat_compare. - destruct (lt_eq_lt_dec (nat_of_P p) (nat_of_P p0)) as [[H|H]|H]; auto. - apply nat_of_P_lt_Lt_compare_complement_morphism; auto. - rewrite (nat_of_P_inj _ _ H); apply Pcompare_refl. - apply nat_of_P_gt_Gt_compare_complement_morphism; auto. + reflexivity. + assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. + destruct nat_of_P; [inversion NZ|auto]. + assert (NZ : 0 < nat_of_P p) by auto using lt_O_nat_of_P. + destruct nat_of_P; [inversion NZ|auto]. + apply nat_of_P_compare_morphism. Qed. Lemma N_of_nat_compare : @@ -210,8 +200,8 @@ Lemma nat_of_Nmin : forall a a', nat_of_N (Nmin a a') = min (nat_of_N a) (nat_of_N a'). Proof. intros; unfold Nmin; rewrite nat_of_Ncompare. - unfold nat_compare. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + rewrite nat_compare_equiv; unfold nat_compare_alt. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; simpl; intros; symmetry; auto with arith. apply min_l; rewrite e; auto with arith. Qed. @@ -230,8 +220,8 @@ Lemma nat_of_Nmax : forall a a', nat_of_N (Nmax a a') = max (nat_of_N a) (nat_of_N a'). Proof. intros; unfold Nmax; rewrite nat_of_Ncompare. - unfold nat_compare. - destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; + rewrite nat_compare_equiv; unfold nat_compare_alt. + destruct (lt_eq_lt_dec (nat_of_N a) (nat_of_N a')) as [[|]|]; simpl; intros; symmetry; auto with arith. apply max_r; rewrite e; auto with arith. Qed. diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index 9bec3e994..bf42c5e99 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -22,6 +22,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 *) @@ -161,7 +165,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; @@ -193,29 +197,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 +235,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 +248,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,21 +299,18 @@ 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. (**********************************************************************) @@ -327,9 +322,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 +332,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 +351,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,8 +362,7 @@ 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. (**********************************************************************) @@ -389,21 +373,13 @@ Qed. 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. @@ -423,9 +399,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; @@ -446,9 +422,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 +445,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; |