proposition: Theorem RPS_G1_equiv : Pr[x <-$ RPS_G_2; ret fst x] == Pr[RPS_G1].
proof: Proof. unfold RPS_G_2, RPS_G1. inline_first. eapply comp_spec_eq_impl_eq. comp_skip. eapply (@oc_comp_spec_eq _ _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a b => fst a = b)); trivial. intuition. unfold GenRP, GenRP_bad. subst. simpl. case_eq (arrayLookup eqdd a0 a); intuition. eapply comp_spec_ret; intuition. unfold rndNotBad. assert ( comp_spec eq (r <-$ (r <-$ RndR; if (negb (fBad a0 a r)) then (ret r) else (Repeat RndR (fun r : R => negb (fBad a0 a r)))); ret (r, (a, r) :: a0)) (r <-$ Repeat RndR (fun r : R => negb (fBad a0 a r)); ret (r, (a, r) :: a0)) ). eapply eq_impl_comp_spec_eq. intuition. symmetry. comp_skip. eapply repeat_unroll_eq. trivial. edestruct goodExists; eauto. admit. eexists. eapply filter_In; intuition. eauto. rewrite H2. trivial. eapply comp_spec_eq_trans_r. 2:{ eapply H0. } clear H0. inline_first. comp_skip. eapply comp_base_exists; eauto. eapply comp_base_exists; eauto. case_eq (fBad a0 a b0); intuition. simpl. comp_skip. eapply comp_spec_ret; intuition. simpl. comp_simp. eapply comp_spec_ret; intuition. comp_simp. simpl in *. intuition; subst. eapply comp_spec_eq_refl. Admitted. Theorem RPS_G0_1_close : | Pr[RPS_G0] - Pr[RPS_G1] | <= (A2_queries / 1) * badProb A2_queries. rewrite RPS_G0_equiv. rewrite <- RPS_G1_equiv. eapply RPS_G_1_2_close. Qed.
imports: FCF PRF RndInList