proposition: Theorem rf_rp_oc_eq_until_bad : comp_spec (fun y1 y2 => snd (snd y1) = snd (snd y2) /\ (snd (snd y1) = false -> fst (snd y1) = fst (snd y2) /\ fst y1 = fst y2)) (A2 (list (D * R) * bool)%type _ randomFunc_bad (nil, false)) (A2 (list (D * R) * bool)%type _ GenRP_bad (nil, false)).
proof: Proof. eapply comp_spec_consequence. eapply (@oc_comp_spec_eq_until_bad _ _ _ _ _ _ _ _ _ _ _ _ _ (fun a => snd a) (fun a => snd a) (fun a b => (fst a = fst b))). intros. eapply randomFunc_bad_wf. intros. eapply GenRP_bad_wf. admit. intuition. simpl in *. subst. case_eq (arrayLookup eqdd a0 a1); intuition. eapply comp_spec_ret; intuition. comp_skip. eapply comp_base_exists; eauto. eapply comp_base_exists; eauto. destruct ( fBad a0 a1 b) eqn:?. comp_irr_r. unfold rndNotBad. edestruct goodExists. eauto. admit. econstructor. unfold eq_dec; intuition. eapply (EqDec_dec _). trivial. eapply filter_In; intuition. eauto. match goal with H5:_|-_ => rewrite H5; reflexivity end. eapply comp_spec_ret. simpl. split. intuition. intros. rewrite orb_true_r in *. discriminate. eapply comp_spec_ret; intuition. intuition. simpl in *. case_eq (arrayLookup eqdd a1 d); intuition. rewrite H1 in H0. repeat simp_in_support. trivial. rewrite H1 in H0. repeat simp_in_support. trivial. intuition. simpl in *. case_eq (arrayLookup eqdd a1 d ); intuition; rewrite H1 in H0; repeat simp_in_support; trivial. trivial. trivial. intuition. Grab Existential Variables. admit. admit. trivial. Admitted. Theorem RPS_G_1_2_bad_same : Pr [x <-$ RPS_G_1; ret snd x ] == Pr [x <-$ RPS_G_2; ret snd x ]. unfold RPS_G_1, RPS_G_2. inline_first. eapply comp_spec_impl_eq. comp_skip. eapply rf_rp_oc_eq_until_bad. intuition. simpl in *. intuition. destruct b. simpl in *. destruct p; simpl in *. subst. comp_simp. simpl. eapply comp_spec_ret; intuition. Qed.
imports: FCF PRF RndInList