diff options
Diffstat (limited to 'theories/Numbers/Integer/Abstract')
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZAddOrder.v | 5 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZLt.v | 2 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZMulOrder.v | 24 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZParity.v | 12 | ||||
| -rw-r--r-- | theories/Numbers/Integer/Abstract/ZPow.v | 12 |
5 files changed, 25 insertions, 30 deletions
diff --git a/theories/Numbers/Integer/Abstract/ZAddOrder.v b/theories/Numbers/Integer/Abstract/ZAddOrder.v index eb27e6378..b5ca908b4 100644 --- a/theories/Numbers/Integer/Abstract/ZAddOrder.v +++ b/theories/Numbers/Integer/Abstract/ZAddOrder.v @@ -102,6 +102,11 @@ Proof. intro n. rewrite (opp_le_mono 0 n). now rewrite opp_0. Qed. +Theorem lt_m1_0 : -(1) < 0. +Proof. +apply opp_neg_pos, lt_0_1. +Qed. + Theorem sub_lt_mono_l : forall n m p, n < m <-> p - m < p - n. Proof. intros n m p. do 2 rewrite <- add_opp_r. rewrite <- add_lt_mono_l. diff --git a/theories/Numbers/Integer/Abstract/ZLt.v b/theories/Numbers/Integer/Abstract/ZLt.v index 540e17cb4..23eac0e69 100644 --- a/theories/Numbers/Integer/Abstract/ZLt.v +++ b/theories/Numbers/Integer/Abstract/ZLt.v @@ -125,7 +125,7 @@ Theorem lt_n1_r : forall n m, n < m -> m < 0 -> n < -(1). Proof. intros n m H1 H2. apply -> lt_le_pred in H2. setoid_replace (P 0) with (-(1)) in H2. now apply lt_le_trans with m. -apply <- eq_opp_r. now rewrite opp_pred, opp_0. +apply <- eq_opp_r. now rewrite one_succ, opp_pred, opp_0. Qed. End ZOrderProp. diff --git a/theories/Numbers/Integer/Abstract/ZMulOrder.v b/theories/Numbers/Integer/Abstract/ZMulOrder.v index 76428584d..25989b2d4 100644 --- a/theories/Numbers/Integer/Abstract/ZMulOrder.v +++ b/theories/Numbers/Integer/Abstract/ZMulOrder.v @@ -177,22 +177,16 @@ Qed. Theorem eq_mul_1 : forall n m, n * m == 1 -> n == 1 \/ n == -1. Proof. -assert (F : ~ 1 < -1). -intro H. -assert (H1 : -1 < 0). apply <- opp_neg_pos. apply lt_succ_diag_r. -assert (H2 : 1 < 0) by now apply lt_trans with (-1). -false_hyp H2 nlt_succ_diag_l. +assert (F := lt_m1_0). zero_pos_neg n. -intros m H; rewrite mul_0_l in H; false_hyp H neq_succ_diag_r. -intros n H; split; apply <- le_succ_l in H; le_elim H. -intros m H1; apply (lt_1_mul_l n m) in H. -rewrite H1 in H; destruct H as [H | [H | H]]. -false_hyp H F. false_hyp H neq_succ_diag_l. false_hyp H lt_irrefl. -intros; now left. -intros m H1; apply (lt_1_mul_l n m) in H. rewrite mul_opp_l in H1; -apply -> eq_opp_l in H1. rewrite H1 in H; destruct H as [H | [H | H]]. -false_hyp H lt_irrefl. apply -> eq_opp_l in H. rewrite opp_0 in H. -false_hyp H neq_succ_diag_l. false_hyp H F. +(* n = 0 *) +intros m. nzsimpl. now left. +(* 0 < n, proving P n /\ P (-n) *) +intros n Hn. rewrite <- le_succ_l, <- one_succ in Hn. +le_elim Hn; split; intros m H. +destruct (lt_1_mul_l n m) as [|[|]]; order'. +rewrite mul_opp_l, eq_opp_l in H. destruct (lt_1_mul_l n m) as [|[|]]; order'. +now left. intros; right; symmetry; now apply opp_wd. Qed. diff --git a/theories/Numbers/Integer/Abstract/ZParity.v b/theories/Numbers/Integer/Abstract/ZParity.v index 1ababfe5c..4c752043c 100644 --- a/theories/Numbers/Integer/Abstract/ZParity.v +++ b/theories/Numbers/Integer/Abstract/ZParity.v @@ -41,20 +41,20 @@ Proof. intros x. split; intros [(y,H)|(y,H)]. right. exists y. rewrite H. now nzsimpl. - left. exists (S y). rewrite H. now nzsimpl. + left. exists (S y). rewrite H. now nzsimpl'. right. exists (P y). rewrite <- succ_inj_wd. rewrite H. - nzsimpl. now rewrite <- add_succ_l, <- add_succ_r, succ_pred. + nzsimpl'. now rewrite <- add_succ_l, <- add_succ_r, succ_pred. left. exists y. rewrite <- succ_inj_wd. rewrite H. now nzsimpl. Qed. Lemma double_below : forall n m, n<=m -> 2*n < 2*m+1. Proof. - intros. nzsimpl. apply lt_succ_r. now apply add_le_mono. + intros. nzsimpl'. apply lt_succ_r. now apply add_le_mono. Qed. Lemma double_above : forall n m, n<m -> 2*n+1 < 2*m. Proof. - intros. nzsimpl. + intros. nzsimpl'. rewrite <- le_succ_l, <- add_succ_l, <- add_succ_r. apply add_le_mono; now apply le_succ_l. Qed. @@ -95,7 +95,7 @@ Qed. Lemma odd_1 : odd 1 = true. Proof. - rewrite odd_spec. exists 0. now nzsimpl. + rewrite odd_spec. exists 0. now nzsimpl'. Qed. Lemma Odd_succ_Even : forall n, Odd (S n) <-> Even n. @@ -140,7 +140,7 @@ Proof. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_assoc. exists (n'+m'). now rewrite mul_add_distr_l, Hn, Hm, add_shuffle0. - exists (n'+m'+1). rewrite Hm,Hn. nzsimpl. now rewrite add_shuffle1. + exists (n'+m'+1). rewrite Hm,Hn. nzsimpl'. now rewrite add_shuffle1. Qed. Lemma odd_add : forall n m, odd (n+m) = xorb (odd n) (odd m). diff --git a/theories/Numbers/Integer/Abstract/ZPow.v b/theories/Numbers/Integer/Abstract/ZPow.v index 9de681375..782a11024 100644 --- a/theories/Numbers/Integer/Abstract/ZPow.v +++ b/theories/Numbers/Integer/Abstract/ZPow.v @@ -78,12 +78,10 @@ Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b. Proof. intros a b (c,H). rewrite H. destruct (le_gt_cases 0 c). - assert (0 <= 2) by (apply le_le_succ_r, le_0_1). - rewrite 2 pow_mul_r; trivial. + rewrite 2 pow_mul_r by order'. rewrite 2 pow_2_r. now rewrite mul_opp_opp. - assert (2*c < 0). - apply mul_pos_neg; trivial. rewrite lt_succ_r. apply le_0_1. + assert (2*c < 0) by (apply mul_pos_neg; order'). now rewrite !pow_neg. Qed. @@ -91,10 +89,8 @@ Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b). Proof. intros a b (c,H). rewrite H. destruct (le_gt_cases 0 c) as [LE|GT]. - assert (0 <= 2*c). - apply mul_nonneg_nonneg; trivial. - apply le_le_succ_r, le_0_1. - rewrite add_succ_r, add_0_r, !pow_succ_r; trivial. + assert (0 <= 2*c) by (apply mul_nonneg_nonneg; order'). + rewrite add_1_r, !pow_succ_r; trivial. rewrite pow_opp_even by (now exists c). apply mul_opp_l. apply double_above in GT. rewrite mul_0_r in GT. |