proposition: Lemma lowDistApprox_bind_evalDist_limit : forall (A B :Set)(c1 : Comp B)(c2 : B -> Comp A) a, well_formed_comp c1 -> (forall b, In b (getSupport c1) -> well_formed_comp (c2 b)) -> (forall (a : B), rat_inf_limit (lowDistApprox c1 a) (evalDist c1 a)) -> (forall (b : B) (a : A), In b (getSupport c1) -> rat_inf_limit (lowDistApprox (c2 b) a) (evalDist (c2 b) a)) -> rat_inf_limit (lowDistApprox_bind c1 c2 a) (evalDist (Bind c1 c2) a).
proof: Proof. unfold rat_inf_limit, inf_limit. intuition. assert (forall (epsilon : Rat), ~ epsilon == 0 -> exists n : nat, forall n': nat, n' >= n -> (forall (b : B) r, lowDistApprox c1 b n' r -> (ratDistance r (evalDist c1 b)) <= epsilon)). assert (forall (epsilon : Rat), (epsilon == 0 -> False) -> forall (a : B), exists n : nat, forall n' : nat, n' >= n -> forall r, lowDistApprox c1 a n' r -> (ratDistance r (evalDist c1 a) <= epsilon)). intuition. intuition. specialize (H4 _ H5). edestruct (rel_map_left_total _ (getSupport c1) H4). Local Open Scope rat_scope. econstructor. intuition. assert (n' >= (maxList x)). eapply H7. edestruct (in_dec (comp_eq_dec c1) b (getSupport c1)). edestruct (rel_map_in_inv H6); eauto. intuition. eapply H12. eapply Nat.le_trans. eapply maxList_correct; eauto. eauto. trivial. eapply leRat_trans. eapply eqRat_impl_leRat. eapply (ratIdentityIndiscernables r). eapply eqRat_trans. eapply getSupport_not_In_lowDistApprox; eauto. eapply eqRat_symm. eapply getSupport_not_In_evalDist; eauto. eapply rat0_le_all. clear H1. assert (forall (epsilon : Rat), ~ epsilon == 0 -> exists n : nat, forall n' : nat, n' >= n -> (forall a b r, In b (getSupport c1) -> lowDistApprox (c2 b) a n' r -> (ratDistance r (evalDist (c2 b) a)) <= epsilon)). assert (forall (epsilon : Rat), (epsilon == 0 -> False) -> forall (x : (B * A)), In (fst x) (getSupport c1) -> exists n : nat, forall n' : nat, n' >= n -> forall r, lowDistApprox (c2 (fst x)) (snd x) n' r -> (ratDistance r (evalDist (c2 (fst x)) (snd x)) <= epsilon)). intuition. intuition. specialize (H1 epsilon0). intuition. edestruct (@rel_map_left_total_strong' _ nat (getSupport_bind_cp c1 c2) (fun y => In (fst y) (getSupport c1)) (fun x n => forall n', n' >= n -> forall r : Rat, lowDistApprox (c2 (fst x)) (snd x) n' r -> (ratDistance r (evalDist (c2 (fst x)) (snd x))) <= epsilon0)). eapply H6. eapply in_getSupport_bind_cp_fst. exists (maxList x). intuition. edestruct (in_dec (EqDec_dec (pair_EqDec (comp_EqDec c1) (bind_EqDec c1 c2))) (b, a0) (getSupport_bind_cp c1 c2)). edestruct (rel_map_in_inv H1); eauto. intuition. simpl in *. eapply H12. eapply Nat.le_trans. eapply maxList_correct; eauto. eauto. trivial. eapply leRat_trans. eapply eqRat_impl_leRat. eapply (ratIdentityIndiscernables r). apply not_In_getSupport_bind_cp in n. edestruct n. intuition. eapply eqRat_trans. eapply getSupport_not_In_lowDistApprox; eauto. eapply eqRat_symm. eapply getSupport_not_In_evalDist; eauto. eauto. eapply comp_eq_dec; eauto. eapply bind_eq_dec; eauto. eapply rat0_le_all. clear H2. assert (nz (length (getSupport c1))). econstructor. eapply getSupport_length_nz. trivial. specialize (H4 ((1 / 3 ) * (epsilon * (RatIntro 1 (natToPosnat H2))))). specialize (H1 ((1 / 3 ) * (epsilon * (RatIntro 1 (natToPosnat H2))))). edestruct H4. eapply ratMult_nz; econstructor. discriminate. eapply ratMult_nz; econstructor; intuition. clear H4. edestruct H1. eapply ratMult_nz; econstructor. discriminate. eapply ratMult_nz; econstructor; intuition. clear H1. exists (max x x0). intuition. inversion H6; clear H6; subst. eapply (@leRat_trans _ (epsilon * (RatIntro 1 (natToPosnat H2)) * (length (getSupport c1) / 1))). simpl. eapply sumList_rel_distance; eauto. intuition. 2:{ eapply sumList_rel_sumList. } simpl in *. subst. assert (well_formed_comp (c2 a0)). eapply H0. trivial. destruct (@lowDistApprox_left_total _ (comp_eq_dec c1) c1 a0 H n'). destruct (@lowDistApprox_left_total _ (bind_eq_dec c1 c2) (c2 a0) a H9 n'). erewrite H8; eauto. eapply leRat_trans. eapply ratDistance_ratMult_le. eapply H5. eapply Nat.max_lub_l. eapply H1. trivial. eapply H4. eapply Nat.max_lub_r. eapply H1. trivial. trivial. eapply lowDistApprox_le_1; eauto. eapply lowDistApprox_le_1; eauto. eapply evalDist_le_1. eapply evalDist_le_1. rewrite <- ratMult_assoc. rewrite <- ratMult_num_den. rewrite num_dem_same_rat1. rewrite ratMult_1_l. eapply leRat_refl. unfold posnatMult, natToPosnat, posnatToNat. trivial. rewrite ratMult_assoc. rewrite ratMult_comm. rewrite <- ratMult_num_den. rewrite num_dem_same_rat1. rewrite ratMult_1_l. eapply leRat_refl. unfold posnatMult, natToPosnat, posnatToNat. rewrite Nat.mul_comm. trivial. Qed.
imports: FCF.Comp FCF.DetSem FCF.DistSem FCF.Rat Arith FCF.StdNat FCF.Fold FCF.Limit Permutation ZifyNat