proposition: Lemma CRmult_plus_distr_r : ∀ x y z : CR, ((x + y) * z == x * z + y * z).
proof: Proof. intros x y z. pose ((CR_b (1#1) x + CR_b (1#1) y + CR_b (1#1) z))%Qpos as b. assert (forall u v, QboundAbs u v <= `u)%Q as qbound_bound. { intros. apply Qmax_lub. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. apply Qpos_nonneg. apply Qmin_lb_l. } assert ( ' (- ` b)%Q <= x)%CR as xlower. { apply (@CRle_trans _ ('(-(proj1_sig (CR_b (1#1) x)))%Q)). 2: apply CR_b_lowerBound. apply CRle_Qle, Qopp_le_compat. rewrite <- Qplus_0_r. simpl. rewrite <- (Qplus_assoc (Qabs (approximate x (Qpos2QposInf (1#1))) + 1)). apply Qplus_le_r. apply (Qpos_nonneg (CR_b (1#1) y + CR_b (1#1) z)). } assert (x <= ' (` b)%Q)%CR as xupper. { apply (@CRle_trans _ ('((proj1_sig (CR_b (1#1) x)))%Q)). apply CR_b_upperBound. apply CRle_Qle. rewrite <- Qplus_0_r. simpl. rewrite <- (Qplus_assoc (Qabs (approximate x (Qpos2QposInf (1#1))) + 1)). apply Qplus_le_r. apply (Qpos_nonneg (CR_b (1#1) y + CR_b (1#1) z)). } assert ( ' (- ` b)%Q <= y)%CR as ylower. { apply (@CRle_trans _ ('(-(proj1_sig (CR_b (1#1) y)))%Q)). 2: apply CR_b_lowerBound. apply CRle_Qle, Qopp_le_compat. rewrite <- Qplus_0_l. simpl. rewrite <- Qplus_assoc. apply Qplus_le_compat. apply (Qpos_nonneg ((CR_b (1#1) x))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. apply (Qpos_nonneg ((CR_b (1#1) z))). } assert (y <= ' (` b)%Q)%CR as yupper. { apply (@CRle_trans _ ('((proj1_sig (CR_b (1#1) y)))%Q)). apply CR_b_upperBound. apply CRle_Qle. rewrite <- Qplus_0_l. simpl. rewrite <- Qplus_assoc. apply Qplus_le_compat. apply (Qpos_nonneg ((CR_b (1#1) x))). rewrite <- Qplus_0_r at 1. apply Qplus_le_r. apply (Qpos_nonneg ((CR_b (1#1) z))). } rewrite <- (CRboundAbs_Eq _ (CR_b_lowerBound (1#1) y) (CR_b_upperBound (1#1) y)). rewrite <- (CRboundAbs_Eq _ (CR_b_lowerBound (1#1) x) (CR_b_upperBound (1#1) x)). assert ( ' (- ` b)%Q <= z)%CR as zlower. { apply (@CRle_trans _ ('(-(proj1_sig (CR_b (1#1) z)))%Q)). 2: apply CR_b_lowerBound. apply CRle_Qle, Qopp_le_compat. rewrite <- Qplus_0_l. apply Qplus_le_compat. apply Qpos_nonneg. apply Qle_refl. } assert (z <= ' (` b)%Q)%CR as zupper. { apply (@CRle_trans _ ('((proj1_sig (CR_b (1#1) z)))%Q)). apply CR_b_upperBound. apply CRle_Qle. rewrite <- Qplus_0_l. apply Qplus_le_compat. apply Qpos_nonneg. apply Qle_refl. } rewrite <- (@CRmult_bounded_mult b (CRboundAbs _ x) z). 2: exact zlower. 2: exact zupper. rewrite <- (@CRmult_bounded_mult b (CRboundAbs _ y) z). 2: exact zlower. 2: exact zupper. rewrite <- (@CRmult_bounded_mult b). 2: exact zlower. 2: exact zupper. rewrite (@CRmult_uncurry_eq b (CRboundAbs _ x) z). 2: rewrite (CRboundAbs_Eq _ (CR_b_lowerBound (1#1) x) (CR_b_upperBound (1#1) x)) ; exact xlower. 2: rewrite (CRboundAbs_Eq _ (CR_b_lowerBound (1#1) x) (CR_b_upperBound (1#1) x)) ; exact xupper. rewrite (@CRmult_uncurry_eq b (CRboundAbs _ y) z). 2: rewrite (CRboundAbs_Eq _ (CR_b_lowerBound (1#1) y) (CR_b_upperBound (1#1) y)) ; exact ylower. 2: rewrite (CRboundAbs_Eq _ (CR_b_lowerBound (1#1) y) (CR_b_upperBound (1#1) y)) ; exact yupper. rewrite CRmult_uncurry_eq. intros e1 e2. rewrite Qplus_0_r. change (Qball (`e1 + `e2) (QboundAbs b (approximate (CRboundAbs (CR_b (1#1) x) x) ((1 # 2) * ((1 # 2) * e1 * Qpos_inv b))%Qpos + approximate (CRboundAbs (CR_b (1#1) y) y) ((1 # 2) * ((1 # 2) * e1 * Qpos_inv b))%Qpos)%Q * QboundAbs b (approximate z (Qmult_modulus b ((1 # 2) * e1)))) (QboundAbs b (approximate (CRboundAbs (CR_b (1#1) x) x) (Qmult_modulus b ((1 # 2) * ((1 # 2) * e2)))) * QboundAbs b (approximate z (Qmult_modulus b ((1 # 2) * ((1 # 2) * e2)))) + QboundAbs b (approximate (CRboundAbs (CR_b (1#1) y) y) (Qmult_modulus b ((1 # 2) * ((1 # 2) * e2)))) * QboundAbs b (approximate z (Qmult_modulus b ((1 # 2) * ((1 # 2) * e2)))))). rewrite <- Qmult_plus_distr_l. unfold Qmult_modulus. apply AbsSmall_Qabs. assert (forall i j k l : Q, Qabs (i*j-k*l) <= Qabs i * Qabs(j-l) + Qabs(i-k)*Qabs l)%Q as multMaj. { intros. setoid_replace (i*j-k*l)%Q with (i*(j-l)+ (i-k)*l)%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply (Qle_trans _ _ _ (Qabs_triangle _ _)). rewrite Qabs_Qmult, Qabs_Qmult. apply Qle_refl. } apply (Qle_trans _ ((1#2)*`e1 + (1#2)*`e2 +((1#2)*`e1 +(1#2)*`e2))). 2: ring_simplify; apply Qle_refl. apply (Qle_trans _ _ _ (multMaj _ _ _ _)). clear multMaj. apply Qplus_le_compat. - apply (Qle_trans _ (`b * Qabs (QboundAbs b (approximate z ((1 # 2) * e1 * Qpos_inv b)%Qpos) - QboundAbs b (approximate z ((1 # 2) * ((1 # 2) * e2) * Qpos_inv b)%Qpos)))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. rewrite QboundAbs_abs. apply Qmin_lb_r. rewrite Qmult_comm. apply (Qle_trans _ (Qabs (approximate z ((1 # 2) * e1 * Qpos_inv b)%Qpos - approximate z ((1 # 2) * ((1 # 2) * e2) * Qpos_inv b)%Qpos) * ` b)). apply Qmult_le_compat_r. 2: apply Qpos_nonneg. apply QboundAbs_contract. apply (Qle_trans _ (((1#2)*`e1 / `b + (1#2)*`e2 / `b) * `b)). apply Qmult_le_r. apply Qpos_ispos. pose proof (regFun_prf z ((1 # 2) * e1 * Qpos_inv b)%Qpos ((1 # 2) * ((1 # 2) * e2) * Qpos_inv b)%Qpos) as H4. apply AbsSmall_Qabs in H4. apply (Qle_trans _ _ _ H4). apply Qplus_le_r. simpl. rewrite Qmult_assoc. apply Qmult_le_r. apply Qinv_lt_0_compat, (Qpos_ispos b). apply Qmult_le_r. apply Qpos_ispos. discriminate. rewrite Qmult_comm. rewrite Qmult_plus_distr_r. apply Qplus_le_compat. unfold Qdiv. rewrite Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. unfold Qdiv. rewrite Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. - assert (forall u, Qabs u <= `b -> QboundAbs b u == u)%Q. { intros u H. apply QboundAbs_elim. intros. apply Qle_antisym. exact H0. apply (Qle_trans _ (Qabs u)). apply Qle_Qabs. exact H. intros. apply Qle_antisym. 2: exact H0. rewrite <- (Qopp_involutive u). apply Qopp_le_compat. rewrite <- Qabs_opp in H. exact (Qle_trans _ _ _ (Qle_Qabs _) H). intros. reflexivity. } rewrite H, H, H; clear H. rewrite QboundAbs_abs. rewrite Qmult_comm. apply (Qle_trans _ (` b * Qabs (approximate (CRboundAbs (CR_b (1#1) x) x) ((1 # 2) * ((1 # 2) * e1 * Qpos_inv b))%Qpos + approximate (CRboundAbs (CR_b (1#1) y) y) ((1 # 2) * ((1 # 2) * e1 * Qpos_inv b))%Qpos - (approximate (CRboundAbs (CR_b (1#1) x) x) ((1 # 2) * ((1 # 2) * e2) * Qpos_inv b)%Qpos + approximate (CRboundAbs (CR_b (1#1) y) y) ((1 # 2) * ((1 # 2) * e2) * Qpos_inv b)%Qpos)))). + apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply Qmin_lb_r. + rewrite Qmult_comm. apply (Qle_trans _ (((1#2)*`e1 / `b + (1#2)*`e2 / `b) * `b)). apply Qmult_le_r. apply Qpos_ispos. assert (forall a b c d, a + b - (c+d) == a - c + (b-d))%Q by (intros; ring). rewrite H; clear H. apply (Qle_trans _ _ _ (Qabs_triangle _ _)). apply (Qle_trans _ (((1#2) * ((1 # 2) * ` e1 / ` b) + (1#2) * ((1 # 2) * ` e2) / ` b) + ((1#2) * ((1 # 2) * ` e1 / ` b) + (1#2) * ((1 # 2) * ` e2) / ` b))). apply Qplus_le_compat. pose proof (regFun_prf (CRboundAbs (CR_b (1#1) x) x) ((1 # 2) * ((1 # 2) * e1 * Qpos_inv b))%Qpos ((1 # 2) * ((1 # 2) * e2) * Qpos_inv b)%Qpos) as H4. apply AbsSmall_Qabs in H4. apply (Qle_trans _ _ _ H4). clear H4. apply Qle_refl. pose proof (regFun_prf (CRboundAbs (CR_b (1#1) y) y) ((1 # 2) * ((1 # 2) * e1 * Qpos_inv b))%Qpos ((1 # 2) * ((1 # 2) * e2) * Qpos_inv b)%Qpos) as H4. apply AbsSmall_Qabs in H4. apply (Qle_trans _ _ _ H4). clear H4. apply Qle_refl. unfold Qdiv. ring_simplify. setoid_replace (8#16)%Q with (1#2)%Q by reflexivity. apply Qle_refl. rewrite Qmult_comm, Qmult_plus_distr_r. apply Qplus_le_compat. unfold Qdiv. rewrite Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. unfold Qdiv. rewrite Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. + change (Qabs (QboundAbs (CR_b (1#1) y) (approximate y ((1 # 2) * ((1 # 2) * e2) * Qpos_inv b)%Qpos)) <= `b)%Q. rewrite QboundAbs_abs. apply (Qle_trans _ _ _ (Qmin_lb_r _ _)). rewrite <- Qplus_0_r. apply Qplus_le_compat. 2: apply Qpos_nonneg. rewrite <- Qplus_0_l. apply Qplus_le_l. apply Qpos_nonneg. + change (Qabs (QboundAbs (CR_b (1#1) x) (approximate x ((1 # 2) * ((1 # 2) * e2) * Qpos_inv b)%Qpos)) <= `b)%Q. rewrite QboundAbs_abs. apply (Qle_trans _ _ _ (Qmin_lb_r _ _)). rewrite <- Qplus_0_r. apply Qplus_le_compat. 2: apply Qpos_nonneg. rewrite <- Qplus_0_r. apply Qplus_le_r. apply Qpos_nonneg. + apply (Qle_trans _ _ _ (Qabs_triangle _ _)). setoid_replace (proj1_sig b) with (proj1_sig (CR_b (1#1) x) + (proj1_sig (CR_b (1#1) y) + proj1_sig (CR_b (1#1) z)))%Q by (simpl; unfold equiv, stdlib_rationals.Q_eq; ring). apply Qplus_le_compat. change (Qabs (QboundAbs (CR_b (1#1) x) (approximate x ((1 # 2) * ((1 # 2) * e1 * Qpos_inv b))%Qpos)) <= proj1_sig (CR_b (1#1) x))%Q. rewrite QboundAbs_abs. apply Qmin_lb_r. change (Qabs (QboundAbs (CR_b (1#1) y) (approximate y ((1 # 2) * ((1 # 2) * e1 * Qpos_inv b))%Qpos)) <= proj1_sig (CR_b (1#1) y) + proj1_sig (CR_b (1#1) z))%Q. rewrite QboundAbs_abs. apply (Qle_trans _ (proj1_sig (CR_b (1#1) y) + 0)). rewrite Qplus_0_r. apply Qmin_lb_r. apply Qplus_le_r. apply Qpos_nonneg. - simpl. intro e. simpl. unfold Cap_raw; simpl. unfold Cap_raw; simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply (Qle_trans _ (- (Qabs (approximate x (Qpos2QposInf (1#1))) + 1) - (Qabs (approximate y (Qpos2QposInf (1#1))) + 1))). 2: apply Qplus_le_compat; apply Qmax_ub_l. setoid_replace (- (Qabs (approximate x (Qpos2QposInf (1#1))) + 1) - (Qabs (approximate y (Qpos2QposInf (1#1))) + 1))%Q with (- ((Qabs (approximate x (Qpos2QposInf (1#1))) + 1) + (Qabs (approximate y (Qpos2QposInf (1#1))) + 1)))%Q by (unfold equiv, stdlib_rationals.Q_eq; ring). apply Qopp_le_compat. rewrite <- Qplus_0_r. apply Qplus_le_r. apply (Qpos_nonneg (CR_b (1#1) z)). - simpl. intro e. simpl. unfold Cap_raw; simpl. unfold Cap_raw; simpl. apply (Qle_trans _ 0). apply (Qopp_le_compat 0), Qpos_nonneg. rewrite <- Qle_minus_iff. apply (Qle_trans _ (Qabs (approximate x (Qpos2QposInf (1#1))) + 1 + (Qabs (approximate y (Qpos2QposInf (1#1))) + 1))). apply Qplus_le_compat. apply (qbound_bound (CR_b (1#1) x)). apply (qbound_bound (CR_b (1#1) y)). rewrite <- Qplus_0_r. apply Qplus_le_r. apply (Qpos_nonneg (CR_b (1#1) z)). Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax Coq.setoid_ring.Ring_theory Coq.Setoids.Setoid Coq.QArith.QArith Coq.QArith.Qabs Coq.QArith.Qround CoRN.metric2.Complete CoRN.metric2.ProductMetric CoRN.reals.fast.CRFieldOps CoRN.model.metric2.Qmetric CoRN.logic.Stability Coq.Logic.ConstructiveEpsilon CoRN.util.Qdlog MathClasses.interfaces.abstract_algebra MathClasses.interfaces.orders