diff options
Diffstat (limited to 'theories/Numbers/NatInt/NZMulOrder.v')
| -rw-r--r-- | theories/Numbers/NatInt/NZMulOrder.v | 221 |
1 files changed, 158 insertions, 63 deletions
diff --git a/theories/Numbers/NatInt/NZMulOrder.v b/theories/Numbers/NatInt/NZMulOrder.v index 09e468ff..97306f93 100644 --- a/theories/Numbers/NatInt/NZMulOrder.v +++ b/theories/Numbers/NatInt/NZMulOrder.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,13 +8,11 @@ (* Evgeny Makarov, INRIA, 2007 *) (************************************************************************) -(*i $Id: NZMulOrder.v 14641 2011-11-06 11:59:10Z herbelin $ i*) - Require Import NZAxioms. Require Import NZAddOrder. -Module Type NZMulOrderPropSig (Import NZ : NZOrdAxiomsSig'). -Include NZAddOrderPropSig NZ. +Module Type NZMulOrderProp (Import NZ : NZOrdAxiomsSig'). +Include NZAddOrderProp NZ. Theorem mul_lt_pred : forall p q n m, S p == q -> (p * n < p * m <-> q * n + m < q * m + n). @@ -26,17 +24,16 @@ Qed. Theorem mul_lt_mono_pos_l : forall p n m, 0 < p -> (n < m <-> p * n < p * m). Proof. -nzord_induct p. -intros n m H; false_hyp H lt_irrefl. -intros p H IH n m H1. nzsimpl. -le_elim H. assert (LR : forall n m, n < m -> p * n + n < p * m + m). -intros n1 m1 H2. apply add_lt_mono; [now apply -> IH | assumption]. -split; [apply LR |]. intro H2. apply -> lt_dne; intro H3. -apply <- le_ngt in H3. le_elim H3. -apply lt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 lt_irrefl. -rewrite <- H; now nzsimpl. -intros p H1 _ n m H2. destruct (lt_asymm _ _ H1 H2). +intros p n m Hp. revert n m. apply lt_ind with (4:=Hp). solve_proper. +intros. now nzsimpl. +clear p Hp. intros p Hp IH n m. nzsimpl. +assert (LR : forall n m, n < m -> p * n + n < p * m + m) + by (intros n1 m1 H; apply add_lt_mono; trivial; now rewrite <- IH). +split; intros H. +now apply LR. +destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. +rewrite EQ in H. order. +apply LR in GT. order. Qed. Theorem mul_lt_mono_pos_r : forall p n m, 0 < p -> (n < m <-> n * p < m * p). @@ -48,19 +45,19 @@ Qed. Theorem mul_lt_mono_neg_l : forall p n m, p < 0 -> (n < m <-> p * m < p * n). Proof. nzord_induct p. -intros n m H; false_hyp H lt_irrefl. -intros p H1 _ n m H2. apply lt_succ_l in H2. apply <- nle_gt in H2. -false_hyp H1 H2. -intros p H IH n m H1. apply <- le_succ_l in H. -le_elim H. assert (LR : forall n m, n < m -> p * m < p * n). -intros n1 m1 H2. apply (le_lt_add_lt n1 m1). -now apply lt_le_incl. rewrite <- 2 mul_succ_l. now apply -> IH. -split; [apply LR |]. intro H2. apply -> lt_dne; intro H3. -apply <- le_ngt in H3. le_elim H3. -apply lt_asymm in H2. apply H2. now apply LR. -rewrite H3 in H2; false_hyp H2 lt_irrefl. -rewrite (mul_lt_pred p (S p)) by reflexivity. -rewrite H; do 2 rewrite mul_0_l; now do 2 rewrite add_0_l. +order. +intros p Hp _ n m Hp'. apply lt_succ_l in Hp'. order. +intros p Hp IH n m _. apply le_succ_l in Hp. +le_elim Hp. +assert (LR : forall n m, n < m -> p * m < p * n). + intros n1 m1 H. apply (le_lt_add_lt n1 m1). + now apply lt_le_incl. rewrite <- 2 mul_succ_l. now rewrite <- IH. +split; intros H. +now apply LR. +destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. +rewrite EQ in H. order. +apply LR in GT. order. +rewrite (mul_lt_pred p (S p)), Hp; now nzsimpl. Qed. Theorem mul_lt_mono_neg_r : forall p n m, p < 0 -> (n < m <-> m * p < n * p). @@ -72,7 +69,7 @@ Qed. Theorem mul_le_mono_nonneg_l : forall n m p, 0 <= p -> n <= m -> p * n <= p * m. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_pos_l. +le_elim H2. apply lt_le_incl. now apply mul_lt_mono_pos_l. apply eq_le_incl; now rewrite H2. apply eq_le_incl; rewrite <- H1; now do 2 rewrite mul_0_l. Qed. @@ -80,7 +77,7 @@ Qed. Theorem mul_le_mono_nonpos_l : forall n m p, p <= 0 -> n <= m -> p * m <= p * n. Proof. intros n m p H1 H2. le_elim H1. -le_elim H2. apply lt_le_incl. now apply -> mul_lt_mono_neg_l. +le_elim H2. apply lt_le_incl. now apply mul_lt_mono_neg_l. apply eq_le_incl; now rewrite H2. apply eq_le_incl; rewrite H1; now do 2 rewrite mul_0_l. Qed. @@ -99,20 +96,13 @@ Qed. Theorem mul_cancel_l : forall n m p, p ~= 0 -> (p * n == p * m <-> n == m). Proof. -intros n m p H; split; intro H1. -destruct (lt_trichotomy p 0) as [H2 | [H2 | H2]]. -apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * m < p * n); [now apply -> mul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 lt_irrefl. -assert (H4 : p * n < p * m); [now apply -> mul_lt_mono_neg_l |]. -rewrite H1 in H4; false_hyp H4 lt_irrefl. -false_hyp H2 H. -apply -> eq_dne; intro H3. apply -> lt_gt_cases in H3. destruct H3 as [H3 | H3]. -assert (H4 : p * n < p * m) by (now apply -> mul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 lt_irrefl. -assert (H4 : p * m < p * n) by (now apply -> mul_lt_mono_pos_l). -rewrite H1 in H4; false_hyp H4 lt_irrefl. -now rewrite H1. +intros n m p Hp; split; intro H; [|now f_equiv]. +apply lt_gt_cases in Hp; destruct Hp as [Hp|Hp]; + destruct (lt_trichotomy n m) as [LT|[EQ|GT]]; trivial. +apply (mul_lt_mono_neg_l p) in LT; order. +apply (mul_lt_mono_neg_l p) in GT; order. +apply (mul_lt_mono_pos_l p) in LT; order. +apply (mul_lt_mono_pos_l p) in GT; order. Qed. Theorem mul_cancel_r : forall n m p, p ~= 0 -> (n * p == m * p <-> n == m). @@ -183,17 +173,17 @@ Qed. Theorem mul_pos_pos : forall n m, 0 < n -> 0 < m -> 0 < n * m. Proof. -intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_pos_r. +intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_pos_r. Qed. Theorem mul_neg_neg : forall n m, n < 0 -> m < 0 -> 0 < n * m. Proof. -intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r. +intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r. Qed. Theorem mul_pos_neg : forall n m, 0 < n -> m < 0 -> n * m < 0. Proof. -intros n m H1 H2. rewrite <- (mul_0_l m). now apply -> mul_lt_mono_neg_r. +intros n m H1 H2. rewrite <- (mul_0_l m). now apply mul_lt_mono_neg_r. Qed. Theorem mul_neg_pos : forall n m, n < 0 -> 0 < m -> n * m < 0. @@ -206,9 +196,33 @@ Proof. intros. rewrite <- (mul_0_l m). apply mul_le_mono_nonneg; order. Qed. +Theorem mul_pos_cancel_l : forall n m, 0 < n -> (0 < n*m <-> 0 < m). +Proof. +intros n m Hn. rewrite <- (mul_0_r n) at 1. + symmetry. now apply mul_lt_mono_pos_l. +Qed. + +Theorem mul_pos_cancel_r : forall n m, 0 < m -> (0 < n*m <-> 0 < n). +Proof. +intros n m Hn. rewrite <- (mul_0_l m) at 1. + symmetry. now apply mul_lt_mono_pos_r. +Qed. + +Theorem mul_nonneg_cancel_l : forall n m, 0 < n -> (0 <= n*m <-> 0 <= m). +Proof. +intros n m Hn. rewrite <- (mul_0_r n) at 1. + symmetry. now apply mul_le_mono_pos_l. +Qed. + +Theorem mul_nonneg_cancel_r : forall n m, 0 < m -> (0 <= n*m <-> 0 <= n). +Proof. +intros n m Hn. rewrite <- (mul_0_l m) at 1. + symmetry. now apply mul_le_mono_pos_r. +Qed. + Theorem lt_1_mul_pos : forall n m, 1 < n -> 0 < m -> 1 < n * m. Proof. -intros n m H1 H2. apply -> (mul_lt_mono_pos_r m) in H1. +intros n m H1 H2. apply (mul_lt_mono_pos_r m) in H1. rewrite mul_1_l in H1. now apply lt_1_l with m. assumption. Qed. @@ -229,7 +243,7 @@ Qed. Theorem neq_mul_0 : forall n m, n ~= 0 /\ m ~= 0 <-> n * m ~= 0. Proof. intros n m; split; intro H. -intro H1; apply -> eq_mul_0 in H1. tauto. +intro H1; apply eq_mul_0 in H1. tauto. split; intro H1; rewrite H1 in H; (rewrite mul_0_l in H || rewrite mul_0_r in H); now apply H. Qed. @@ -241,16 +255,22 @@ Qed. Theorem eq_mul_0_l : forall n m, n * m == 0 -> m ~= 0 -> n == 0. Proof. -intros n m H1 H2. apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1]. +intros n m H1 H2. apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. assumption. false_hyp H1 H2. Qed. Theorem eq_mul_0_r : forall n m, n * m == 0 -> n ~= 0 -> m == 0. Proof. -intros n m H1 H2; apply -> eq_mul_0 in H1. destruct H1 as [H1 | H1]. +intros n m H1 H2; apply eq_mul_0 in H1. destruct H1 as [H1 | H1]. false_hyp H1 H2. assumption. Qed. +(** Some alternative names: *) + +Definition mul_eq_0 := eq_mul_0. +Definition mul_eq_0_l := eq_mul_0_l. +Definition mul_eq_0_r := eq_mul_0_r. + Theorem lt_0_mul : forall n m, 0 < n * m <-> (0 < n /\ 0 < m) \/ (m < 0 /\ n < 0). Proof. intros n m; split; [intro H | intros [[H1 H2] | [H1 H2]]]. @@ -283,25 +303,100 @@ Theorem square_lt_simpl_nonneg : forall n m, 0 <= m -> n * n < m * m -> n < m. Proof. intros n m H1 H2. destruct (lt_ge_cases n 0). now apply lt_le_trans with 0. -destruct (lt_ge_cases n m). -assumption. assert (F : m * m <= n * n) by now apply square_le_mono_nonneg. -apply -> le_ngt in F. false_hyp H2 F. +destruct (lt_ge_cases n m) as [LT|LE]; trivial. +apply square_le_mono_nonneg in LE; order. Qed. Theorem square_le_simpl_nonneg : forall n m, 0 <= m -> n * n <= m * m -> n <= m. Proof. intros n m H1 H2. destruct (lt_ge_cases n 0). apply lt_le_incl; now apply lt_le_trans with 0. -destruct (le_gt_cases n m). -assumption. assert (F : m * m < n * n) by now apply square_lt_mono_nonneg. -apply -> lt_nge in F. false_hyp H2 F. +destruct (le_gt_cases n m) as [LE|LT]; trivial. +apply square_lt_mono_nonneg in LT; order. +Qed. + +Theorem mul_2_mono_l : forall n m, n < m -> 1 + 2 * n < 2 * m. +Proof. +intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m two). +rewrite two_succ. nzsimpl. now rewrite le_succ_l. +order'. +Qed. + +Lemma add_le_mul : forall a b, 1<a -> 1<b -> a+b <= a*b. +Proof. + assert (AUX : forall a b, 0<a -> 0<b -> (S a)+(S b) <= (S a)*(S b)). + intros a b Ha Hb. + nzsimpl. rewrite <- succ_le_mono. apply le_succ_l. + rewrite <- add_assoc, <- (add_0_l (a+b)), (add_comm b). + apply add_lt_mono_r. + now apply mul_pos_pos. + intros a b Ha Hb. + assert (Ha' := lt_succ_pred 1 a Ha). + assert (Hb' := lt_succ_pred 1 b Hb). + rewrite <- Ha', <- Hb'. apply AUX; rewrite succ_lt_mono, <- one_succ; order. +Qed. + +(** A few results about squares *) + +Lemma square_nonneg : forall a, 0 <= a * a. +Proof. + intros. rewrite <- (mul_0_r a). destruct (le_gt_cases a 0). + now apply mul_le_mono_nonpos_l. + apply mul_le_mono_nonneg_l; order. +Qed. + +Lemma crossmul_le_addsquare : forall a b, 0<=a -> 0<=b -> b*a+a*b <= a*a+b*b. +Proof. + assert (AUX : forall a b, 0<=a<=b -> b*a+a*b <= a*a+b*b). + intros a b (Ha,H). + destruct (le_exists_sub _ _ H) as (d & EQ & Hd). + rewrite EQ. + rewrite 2 mul_add_distr_r. + rewrite !add_assoc. apply add_le_mono_r. + rewrite add_comm. apply add_le_mono_l. + apply mul_le_mono_nonneg_l; trivial. order. + intros a b Ha Hb. + destruct (le_gt_cases a b). + apply AUX; split; order. + rewrite (add_comm (b*a)), (add_comm (a*a)). + apply AUX; split; order. +Qed. + +Lemma add_square_le : forall a b, 0<=a -> 0<=b -> + a*a + b*b <= (a+b)*(a+b). +Proof. + intros a b Ha Hb. + rewrite mul_add_distr_r, !mul_add_distr_l. + rewrite add_assoc. + apply add_le_mono_r. + rewrite <- add_assoc. + rewrite <- (add_0_r (a*a)) at 1. + apply add_le_mono_l. + apply add_nonneg_nonneg; now apply mul_nonneg_nonneg. +Qed. + +Lemma square_add_le : forall a b, 0<=a -> 0<=b -> + (a+b)*(a+b) <= 2*(a*a + b*b). +Proof. + intros a b Ha Hb. + rewrite !mul_add_distr_l, !mul_add_distr_r. nzsimpl'. + rewrite <- !add_assoc. apply add_le_mono_l. + rewrite !add_assoc. apply add_le_mono_r. + apply crossmul_le_addsquare; order. Qed. -Theorem mul_2_mono_l : forall n m, n < m -> 1 + (1 + 1) * n < (1 + 1) * m. +Lemma quadmul_le_squareadd : forall a b, 0<=a -> 0<=b -> + 2*2*a*b <= (a+b)*(a+b). Proof. -intros n m. rewrite <- le_succ_l, (mul_le_mono_pos_l (S n) m (1 + 1)). -rewrite !mul_add_distr_r; nzsimpl; now rewrite le_succ_l. -apply add_pos_pos; now apply lt_0_1. + intros. + nzsimpl'. + rewrite !mul_add_distr_l, !mul_add_distr_r. + rewrite (add_comm _ (b*b)), add_assoc. + apply add_le_mono_r. + rewrite (add_shuffle0 (a*a)), (mul_comm b a). + apply add_le_mono_r. + rewrite (mul_comm a b) at 1. + now apply crossmul_le_addsquare. Qed. -End NZMulOrderPropSig. +End NZMulOrderProp. |