proposition: Theorem ExpROM_swap : forall (A B C : Set) (c1 : OracleComp DomainRO RangeRO A) (c2 : OracleComp DomainRO RangeRO B) (c3 : A -> B -> OracleComp DomainRO RangeRO C) (E : Set)(eqde : EqDec E)(f2 : C -> E -> (DomainRO * RangeRO) -> E) (init : E) s x, (forall c e d1 d2, f2 c (f2 c e d1) d2 = f2 c (f2 c e d2) d1) -> evalDist (ExpROM_gen_s (x1 <--$ c1; x2 <--$ c2; c3 x1 x2) _ (fun c ls => fold_left (fun e d => (f2 c e d)) ls init) s ) x == evalDist (ExpROM_gen_s (x2 <--$ c2; x1 <--$ c1; c3 x1 x2) _ (fun c ls => fold_left (fun e d => (f2 c e d)) ls init) s ) x.
proof: Proof. intuition idtac. assert RangeRO as RangeRO_ex. eapply comp_base_exists; eauto. assert A as a_ex. eapply oc_base_exists; eauto. assert B as b_ex. eapply oc_base_exists; eauto. assert C as c_ex. eapply oc_base_exists. eapply c3; intuition idtac. intuition idtac. unfold ExpROM_gen_s. eapply (@eqRat_trans _ (evalDist (z <-$ (x1 <--$ c1; x2 <--$ c2; c3 x1 x2) (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (sortedRandomFunc _ _ leDom rndRange) (sortDom leDom s); [t, s0]<-2 z; ret fold_left (fun (e : E) (d : DomainRO * RangeRO) => f2 t e d) s0 init) x) ). eapply comp_spec_eq_impl_eq. fcf_skip. eapply fcf_oracle_eq. 2:{ intros. assert ((fun x1 x2 => x2 = sortDom leDom x1) x1 x2). eapply H0. simpl in *. subst. eapply sortedRandomFunc_sorted_equiv; intuition idtac. } simpl in *. trivial. simpl in *; intuition idtac. destruct b0; simpl in *; subst. eapply comp_spec_ret; intuition idtac. eapply fold_left_comm_perm_eq; intuition idtac. eapply sortDom_perm. eauto. symmetry. eapply (@eqRat_trans _ (evalDist (z <-$ (x1 <--$ c2; x2 <--$ c1; c3 x2 x1) (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (sortedRandomFunc _ _ leDom rndRange) (sortDom leDom s); [t, s0]<-2 z; ret fold_left (fun (e : E) (d : DomainRO * RangeRO) => f2 t e d) s0 init) x) ). eapply comp_spec_eq_impl_eq. fcf_skip. eapply fcf_oracle_eq. 2:{ intros. assert ((fun x1 x2 => x2 = sortDom leDom x1) x1 x2). eapply H0. simpl in *. subst. eapply sortedRandomFunc_sorted_equiv; intuition idtac. } simpl in *. trivial. simpl in *; intuition idtac. destruct b0; simpl in *; subst. eapply comp_spec_ret; intuition idtac. eapply fold_left_comm_perm_eq; intuition idtac. eapply sortDom_perm. eauto. eapply comp_spec_eq_impl_eq. simpl. eapply (@comp_spec_eq_trans _ _ _ (z <-$ ([z, z2, s'0] <-$3 (z0 <-$ c2 (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (sortedRandomFunc DomainRO_EqDec RangeRO_EqDec leDom rndRange) (sortDom leDom s); [z, s']<-2 z0; z1 <-$ c1 (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (sortedRandomFunc DomainRO_EqDec RangeRO_EqDec leDom rndRange) s'; [z2, s'0]<-2 z1; ret (z, z2, s'0)); (c3 z2 z) (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (sortedRandomFunc DomainRO_EqDec RangeRO_EqDec leDom rndRange) s'0); [t, s0]<-2 z; ret fold_left (fun (e : E) (d : DomainRO * RangeRO) => f2 t e d) s0 init) ). fcf_inline_first. fcf_skip. fcf_inline_first. fcf_skip. fcf_simp. eapply comp_spec_eq_refl. eapply comp_spec_eq_symm. eapply (@comp_spec_eq_trans _ _ _ (z <-$ ([z, z2, s'0] <-$3 (z0 <-$ c1 (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (sortedRandomFunc DomainRO_EqDec RangeRO_EqDec leDom rndRange) (sortDom leDom s); [z, s']<-2 z0; z1 <-$ c2 (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (sortedRandomFunc DomainRO_EqDec RangeRO_EqDec leDom rndRange) s'; [z2, s'0]<-2 z1; ret (z2, z, s'0)); (c3 z2 z) (list (DomainRO * RangeRO)) (list_EqDec (pair_EqDec DomainRO_EqDec RangeRO_EqDec)) (sortedRandomFunc DomainRO_EqDec RangeRO_EqDec leDom rndRange) s'0); [t, s0]<-2 z; ret fold_left (fun (e : E) (d : DomainRO * RangeRO) => f2 t e d) s0 init) ). fcf_inline_first. fcf_skip. fcf_inline_first. fcf_skip. fcf_simp. eapply comp_spec_eq_refl. eapply comp_spec_seq_eq; trivial. eapply comp_spec_seq_eq; trivial. intuition idtac. intuition idtac. eapply comp_spec_eq_symm. eapply ExpROM_swap_spec; intuition idtac. eapply sortedRandomFunc_swap; intuition idtac. intuition idtac. eapply comp_spec_eq_refl. intuition idtac. eapply comp_spec_eq_refl. Unshelve. eapply oc_EqDec. eapply c3; intuition idtac. intuition idtac. intuition idtac. eapply oc_EqDec. eapply c3; intuition idtac. intuition idtac. intuition idtac. eapply pair_EqDec. eapply oc_EqDec; eauto. eapply list_EqDec. eapply pair_EqDec; intuition idtac. eapply pair_EqDec. eapply oc_EqDec; eauto. eapply list_EqDec. eapply pair_EqDec; eauto. eapply pair_EqDec. eapply oc_EqDec; eauto. eapply list_EqDec. eapply pair_EqDec; eauto. eapply pair_EqDec. eapply oc_EqDec; eauto. eapply list_EqDec. eapply pair_EqDec; eauto. eapply pair_EqDec. eapply oc_EqDec; eauto. eapply list_EqDec. eapply pair_EqDec; eauto. eapply oc_EqDec; eauto. eapply oc_EqDec; eauto. Qed.
imports: FCF FCF.PRF Permutation