proposition: Lemma CRmult_uncurry_eq_3 : forall (c:Qpos) (x y z : CR), (' (- ` c)%Q <= x)%CR -> (x <= 'proj1_sig c)%CR -> (' (- ` c)%Q <= CRmult_bounded c x y)%CR -> (CRmult_bounded c x y <= 'proj1_sig c)%CR -> (CRmult_bounded c (CRmult_bounded c x y) z == Cmap (ProductMS_prelength (ProductMS_prelength QPrelengthSpace QPrelengthSpace) QPrelengthSpace) (uc_compose (Qmult_uncurry c) (together (Qmult_uncurry c) (uc_id Q_as_MetricSpace))) (undistrib_Complete (undistrib_Complete (x,y), z)))%CR.
proof: Proof. intros. assert (forall a, Qabs (QboundAbs c a) <= `c) as qbound_bound. { intros a. rewrite QboundAbs_abs. apply Qmin_lb_r. } rewrite (@CRmult_uncurry_eq c (CRmult_bounded c x y) z); try assumption. assert (msp_eq (undistrib_Complete (CRmult_bounded c x y, z)) (undistrib_Complete ((Cmap (ProductMS_prelength QPrelengthSpace QPrelengthSpace) (Qmult_uncurry c) (undistrib_Complete (x,y))), z))) as H4. { intros e1 e2. split. apply (@CRmult_uncurry_eq c x y H H0). rewrite Qplus_0_r. apply regFun_prf. } rewrite H4. clear H4. rewrite fast_MonadLaw2. apply Cmap_wd. reflexivity. intros e1 e2. split. - simpl. 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 _ (`c * (Qabs (Qmax (- ` c) (Qmin (` c) (approximate y (Qmult_modulus c ((1 # 2) ↾ eq_refl * e1)))) - Qmax (- ` c) (Qmin (` c) (approximate y (Qpos_min ((1 # 2) ↾ eq_refl * e2 * Qpos_inv c) e2))))))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply qbound_bound. rewrite Qmult_comm. apply (Qle_trans _ (Qabs (approximate y (Qmult_modulus c ((1 # 2) ↾ eq_refl * e1)) - approximate y (Qpos_min ((1 # 2) ↾ eq_refl * e2 * Qpos_inv c) e2)) * `c)). apply Qmult_le_compat_r. 2: apply Qpos_nonneg. apply QboundAbs_contract. apply (Qle_trans _ (((1#2)*`e1 / `c + (1#2)*`e2 / `c) * `c)). apply Qmult_le_r. apply Qpos_ispos. unfold Qmult_modulus. pose proof (regFun_prf y ((1 # 2) * e1 * Qpos_inv c)%Qpos (Qpos_min ((1 # 2) * e2 * Qpos_inv c)%Qpos e2)) as H4. apply AbsSmall_Qabs in H4. apply (Qle_trans _ _ _ H4). clear H4. apply Qplus_le_r. rewrite Q_Qpos_min. simpl. apply Qmin_lb_l. rewrite Qmult_plus_distr_l. apply Qplus_le_compat. unfold Qdiv. rewrite Qmult_comm, Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. unfold Qdiv. rewrite Qmult_comm, Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. + rewrite Qmult_comm. apply (Qle_trans _ (`c * (Qabs (Qmax (- ` c) (Qmin (` c) (approximate x (Qmult_modulus c ((1 # 2) ↾ eq_refl * e1)))) - Qmax (- ` c) (Qmin (` c) (approximate x (Qpos_min ((1 # 2) ↾ eq_refl * e2 * Qpos_inv c) e2))))))). apply Qmult_le_compat_r. 2: apply Qabs_nonneg. apply qbound_bound. rewrite Qmult_comm. apply (Qle_trans _ (Qabs (approximate x (Qmult_modulus c ((1 # 2) ↾ eq_refl * e1)) - approximate x (Qpos_min ((1 # 2) ↾ eq_refl * e2 * Qpos_inv c) e2)) * `c)). apply Qmult_le_compat_r. 2: apply Qpos_nonneg. apply QboundAbs_contract. apply (Qle_trans _ (((1#2)*`e1 / `c + (1#2)*`e2 / `c) * `c)). apply Qmult_le_r. apply Qpos_ispos. unfold Qmult_modulus. pose proof (regFun_prf x ((1 # 2) * e1 * Qpos_inv c)%Qpos (Qpos_min ((1 # 2) * e2 * Qpos_inv c)%Qpos e2)) as H4. apply AbsSmall_Qabs in H4. apply (Qle_trans _ _ _ H4). clear H4. apply Qplus_le_r. rewrite Q_Qpos_min. simpl. apply Qmin_lb_l. rewrite Qmult_plus_distr_l. apply Qplus_le_compat. unfold Qdiv. rewrite Qmult_comm, Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. unfold Qdiv. rewrite Qmult_comm, Qmult_assoc. apply Qle_shift_div_r. apply Qpos_ispos. rewrite Qmult_comm. apply Qle_refl. - simpl. assert (`e1 + proj1_sig (Qpos_min ((1 # 2) ↾ eq_refl * e2 * Qpos_inv c) e2) <= `e1 + `e2) as H4. { apply Qplus_le_r. apply Qpos_min_lb_r. } rewrite Qplus_0_r. apply (ball_weak_le _ _ _ H4). apply regFun_prf. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.model.totalorder.QposMinMax CoRN.model.lattice.CRlattice CoRN.model.totalorder.QMinMax Coq.QArith.Qabs CoRN.model.metric2.Qmetric CoRN.metric2.ProductMetric MathClasses.interfaces.canonical_names