proposition: Theorem RndInAdaptive_prob : forall (c : OracleComp A B C)(q : nat), queries_at_most c q -> forall (S : Set)(evt : S -> bool)(eqd : EqDec S)(o : S -> A -> Comp (B * S))(k : Rat), (forall a b, evt a = false -> Pr[ d <-$ o a b; ret (evt (snd d))] <= k)-> (forall a b x y, In (a, b) (getSupport (o x y)) -> evt x = true -> evt b = true) -> forall (s : S), evt s = false -> Pr[ d <-$ c _ _ o s; ret (evt (snd d))] <= q / 1 * k.
proof: Proof. induction 1; intuition. Opaque evalDist. simpl. assert ( Pr [d <-$ (z0 <-$ c S eqd o s; [z, s']<-2 z0; (f z) S eqd o s'); ret evt (snd d) ] == Pr [a <-$ c S eqd o s; d <-$ (f (fst a)) S eqd o (snd a); ret (evt (snd a) || evt (snd d)) ]). inline_first. comp_skip. comp_simp. comp_skip. simpl. intuition. simpl. destruct x; simpl in*. case_eq (evt s0); intuition. assert (evt s1 = true). eapply oc_comp_invariant_f; eauto. rewrite H8. simpl; intuition. rewrite orb_false_l. intuition. rewrite H5. clear H5. assert (Pr [a <-$ c S eqd o s; d <-$ (f (fst a)) S eqd o (snd a); ret evt (snd a) || evt (snd d) ] <= q1 / 1 * k + q2 / 1 * k). eapply orb_prob. eapply IHqueries_at_most; eauto. intros. eapply H1; eauto. destruct a; repeat econstructor; eauto. rewrite H5. eapply eqRat_impl_leRat. rewrite ratAdd_den_same. rewrite ratMult_distrib_r. intuition. Opaque evalDist. simpl. rewrite H; intuition. eapply eqRat_impl_leRat. symmetry. eapply ratMult_1_l. simpl. inline_first. comp_at comp_ret leftc 1%nat. simpl. Transparent evalDist. simpl. eapply leRat_trans. eapply eqRat_impl_leRat. eapply sumList_0. intuition. rewrite H1. destruct (EqDec_dec bool_EqDec false true). discriminate. eapply ratMult_0_r. eapply rat0_le_all. Opaque evalDist. assert (A -> B). intuition. assert (B * S). eapply oc_base_exists; eauto. intuition. assert (B' * S0). eapply comp_base_exists; eauto. intuition. intuition. assert (EqDec C). eapply oc_EqDec; eauto. simpl. specialize (IHqueries_at_most (S * S0)%type (fun p => evt (snd p)) _ (fun (x : S * S0) (y : A) => p <-$ (oc (fst x) y) S0 eqd o (snd x); ret (fst (fst p), (snd (fst p), snd p))) (q2 / 1 * k)). inline_first. comp_at comp_ret leftc 1%nat. eapply leRat_trans. eapply IHqueries_at_most. intuition. simpl in H7. inline_first. simpl. comp_at comp_ret leftc 1%nat. eapply H1; eauto. intuition. simpl. repeat simp_in_support. destruct x. simpl. eapply oc_comp_invariant_f; eauto. trivial. rewrite <- ratMult_assoc. eapply ratMult_leRat_compat; intuition. rewrite <- ratMult_num_den. eapply eqRat_impl_leRat. eapply eqRat_terms; intuition. eapply leRat_trans. eapply IHqueries_at_most; eauto. eapply ratMult_leRat_compat; intuition. eapply leRat_terms; intuition. Qed.
imports: FCF.FCF FCF.CompFold