proposition: Theorem oc_eventProb : forall (A B C : Set)(c : OracleComp A B C) n, queries_at_most' c n -> forall (S : Set)(eqds : EqDec S)(o : S -> A -> Comp (B * S)) (count : S -> nat)(evt : S -> bool)(s : S)(k : nat -> Rat) i, (forall (n1 n2 : nat), (n1 <= n2)%nat -> (k n1 <= k n2)) -> evt s = false -> (forall s a, evt s = false -> Pr[p <-$ o s a; ret (evt (snd p))] <= (k (i + (count s))%nat)) -> (forall s s' a b, In (b, s') (getSupport (o s a)) -> count s' <= i + (count s))%nat -> Pr[p <-$ c _ _ o s; ret (evt (snd p))] <= (n / 1) * (k (i * n + (count s))%nat).
proof: Proof. Local Opaque evalDist. induction 1; intuition; simpl in *. inline_first. assert ( Pr [a <-$ c S eqds o s; p <-$ ([z, s']<-2 a; (f z) S eqds o s'); ret evt (snd p) ] <= q1 / 1 * k (i * q1 + count s)%nat + q2 / 1 * k (i * q2 + (i * q1 + count s))%nat ). eapply evalDist_bind_event_le. eapply (@IHqueries_at_most' _ _ _ count evt); intuition. intros. comp_simp. eapply leRat_trans. eapply (@H1 _ _ _ _ _ count evt). eapply H2. trivial. intuition. intuition. eapply ratMult_leRat_compat; intuition. eapply H2. eapply plus_le_compat; intuition. Require Import RndInList. eapply le_trans. eapply (qam_count_gen' _ _ _ _ _ i). intuition. eapply H5. eauto. eauto. rewrite mult_comm. intuition. rewrite H6. clear H6. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. rewrite ratAdd_num. eapply ratMult_distrib_r. } eapply ratAdd_leRat_compat; eapply ratMult_leRat_compat. reflexivity. intuition. reflexivity. eapply H2. rewrite mult_plus_distr_l. rewrite plus_comm. repeat rewrite <- plus_assoc. eapply plus_le_compat; intuition. rewrite H1; intuition. rewrite <- ratMult_1_l. eapply ratMult_leRat_compat; intuition. eapply leRat_terms; intuition. inline_first. eapply distro_irr_le. intuition. comp_simp. simpl. rewrite H0. rewrite evalDist_ret_0. eapply rat0_le_all. congruence. inline_first. assert (EqDec C). eapply oc_EqDec; intros. eapply c. assert (B * S). eapply oc_base_exists. eapply oc. trivial. trivial. intuition. assert (B' * S0). eapply comp_base_exists. eapply o. trivial. trivial. intuition. intuition. trivial. assert ( (evalDist (Bind (c (prod S S0) (pair_EqDec eqds eqds0) (fun (x : prod S S0) (y : A) => Bind ((oc (fst x) y) S0 eqds0 o (snd x)) (fun p : prod (prod B S) S0 => Ret (EqDec_dec (pair_EqDec eqdb (pair_EqDec eqds eqds0))) (pair (fst (fst p)) (pair (snd (fst p)) (snd p))))) (pair s s0)) (fun a : prod C (prod S S0) => Bind (Ret (EqDec_dec (pair_EqDec (pair_EqDec (oc_EqDec c (fun x : A => fst (oc_base_exists (oc s x) (fun y : A' => fst (comp_base_exists (o s0 y))))) (fun x : A => EqDec_pair_l (oc_EqDec (oc s x) (fun y : A' => fst (comp_base_exists (o s0 y))) (fun y : A' => EqDec_pair_l (comp_EqDec (o s0 y)) s0)) s)) eqds) eqds0)) (pair (pair (fst a) (fst (snd a))) (snd (snd a)))) (fun p : prod (prod C S) S0 => Ret (EqDec_dec bool_EqDec) (evt (snd p))))) true) == Pr [a <-$ c (S * S0)%type (pair_EqDec eqds eqds0) (fun (x : S * S0) (y : A) => p <-$ (oc (fst x) y) S0 eqds0 o (snd x); ret (fst (fst p), (snd (fst p), snd p))) (s, s0); ret (evt (snd (snd a))) ] ). comp_skip. simpl. intuition. rewrite H7. clear H7. eapply leRat_trans. eapply (@IHqueries_at_most' _ _ ((fun (x : S * S0) (y : A) => p <-$ (oc (fst x) y) S0 eqds0 o (snd x); ret (fst (fst p), (snd (fst p), snd p)))) (fun p => count (snd p)) (fun p => evt (snd p)) _ (fun x => q2 / 1 * k (x)%nat) (i * q2)%nat). intuition. eapply ratMult_leRat_compat; intuition. trivial. intuition. comp_inline_l. assert ( Pr [a1 <-$ (oc (fst (a, b)) a0) S0 eqds0 o (snd (a, b)); p <-$ ret (fst (fst a1), (snd (fst a1), snd a1)); ret evt (snd (snd p)) ] == Pr [a1 <-$ (oc (fst (a, b)) a0) S0 eqds0 o (snd (a, b)); ret evt (snd a1) ] ). comp_skip. simpl. intuition. rewrite H8. clear H8. simpl. eapply leRat_trans. eapply (@H1 ); intuition. reflexivity. intuition. repeat simp_in_support. destruct x. simpl in *. rewrite mult_comm. eapply qam_count_gen'. eapply H0. intuition. eapply H5. eapply H7. eapply H8. simpl. rewrite <- ratMult_assoc. eapply ratMult_leRat_compat. eapply eqRat_impl_leRat. rewrite <- ratMult_num_den. eapply eqRat_terms; intuition. eapply H2. eapply plus_le_compat. 2: reflexivity. rewrite <- mult_assoc. eapply mult_le_compat. reflexivity. rewrite mult_comm. reflexivity. rewrite IHqueries_at_most'. eapply ratMult_leRat_compat; intuition. eapply leRat_terms; intuition. intuition. trivial. intuition. intuition. Grab Existential Variables. trivial. eapply in_oc_supp_complete; eauto. Qed.
imports: FCF PRF RndInList