proposition: Lemma MonadLaw4 : forall (f:X --> Y) a, (Cmap_slow_fun f (Cjoin_fun a)) =m (Cjoin_fun ((Cmap_slow_fun (Cmap_slow f)) a)).
proof: Proof. intros f x e1 e2. pose (exist (Qlt 0) (1#2) eq_refl) as half. pose (exist (Qlt 0) (1#4) eq_refl) as quarter. pose (exist (Qlt 0) (1#8) eq_refl) as eightth. set (e2' := (half*e2)%Qpos). set (d0 := (QposInf_min (Qpos2QposInf quarter*(mu f e1)) (Qpos2QposInf (exist (Qlt 0) (1#8) eq_refl) *(mu f (half*e2))))%QposInf). simpl. unfold Cmap_slow_raw; simpl. unfold Cjoin_raw; simpl. unfold Cmap_slow_raw; simpl. assert (halfhalf: forall q, QposEq (quarter * q) (half * (half * q))%Qpos). { unfold QposEq. intro. simpl. ring. } apply ball_triangle with (f (approximate (approximate x d0) d0)). rewrite Qplus_0_r. apply uc_prf. destruct (mu f e1) as [q|]; try constructor. simpl. do 2 rewrite <- ball_Cunit. unfold d0. assert (QposEq q ((quarter*q + quarter*q) + (quarter*q+ quarter*q))%Qpos) as qeq. { unfold QposEq. simpl. ring. } pose proof (ball_wd (Complete (Complete X)) qeq) as bwd. apply (bwd _ _ (reflexivity _) _ _ (reflexivity _)). apply ball_triangle with x. apply ball_triangle with (Cunit (approximate x (half * (half * q))%Qpos)). rewrite -> ball_Cunit. unfold QposEq in halfhalf. rewrite halfhalf. apply ball_approx_l. unfold QposEq in halfhalf. rewrite halfhalf. apply ball_approx_l. apply ball_triangle with (Cunit (approximate x d0)). change (ball_ex (quarter * q)%Qpos x (Cunit (approximate x d0))). apply ball_ex_weak_le with (d0)%QposInf. apply QposInf_min_lb_l. destruct d0 as [d0|]; try constructor. apply ball_approx_r. rewrite -> ball_Cunit. change (ball_ex (quarter * q)%Qpos (approximate x d0) (Cunit (approximate (approximate x d0) d0))). apply ball_ex_weak_le with (d0)%QposInf. apply QposInf_min_lb_l. destruct d0 as [d0|]; try constructor. apply ball_approx_r. apply ball_sym. apply ball_weak_le with (proj1_sig (half*e2)%Qpos). simpl. rewrite <- (Qmult_1_l (proj1_sig e2)), Qmult_assoc. apply Qmult_le_r. apply Qpos_ispos. discriminate. apply uc_prf. unfold half. simpl. unfold half in d0. simpl in d0. destruct (@mu X Y f (exist (Qlt 0) (1 # 2) (@eq_refl comparison Lt) * e2)); try constructor. simpl. do 2 rewrite <- ball_Cunit. assert (QposEq q ((half*q + quarter*q)+ (eightth*q+ eightth*q))%Qpos) as qeq. { unfold QposEq. simpl. ring. } pose proof (ball_wd (Complete (Complete X)) qeq) as bwd. apply (bwd _ _ (reflexivity _) _ _ (reflexivity _)). apply ball_triangle with x. apply ball_triangle with (Cunit (approximate x (half * (half * q))%Qpos)). - rewrite -> ball_Cunit. apply ball_approx_l. - unfold QposEq in halfhalf. rewrite halfhalf. apply ball_approx_l. - apply ball_triangle with (Cunit (approximate x d0)). change (ball_ex (eightth * q)%Qpos x (Cunit (approximate x d0))). apply ball_ex_weak_le with (d0)%QposInf. apply QposInf_min_lb_r. destruct d0 as [d0|]; try constructor. apply ball_approx_r. rewrite -> ball_Cunit. change (ball_ex (eightth * q)%Qpos (approximate x d0) (Cunit (approximate (approximate x d0) d0))). apply ball_ex_weak_le with (d0)%QposInf. apply QposInf_min_lb_r. destruct d0 as [d0|]; try constructor. apply ball_approx_r. Qed.
imports: CoRN.metric2.UniformContinuity CoRN.model.structures.QposInf CoRN.metric2.Classification CoRN.model.totalorder.QposMinMax CoRN.model.totalorder.QMinMax