proposition: Theorem ExpROM_swap_spec_h : forall (D1 R1 : Set) (A1 : Set) (c1 : OracleComp D1 R1 A1) (D2 R2 : Set) (A2 : Set) (c2 : OracleComp D2 R2 A2) (eqdr1 : EqDec R1)(eqdr2 : EqDec R2) (eqda1 : EqDec A1)(eqda2 : EqDec A2) (S : Set)(eqds : EqDec S) (o1 : S -> D1 -> Comp (R1 * S)) (o2 : S -> D2 -> Comp (R2 * S)) s, (forall s d1, comp_spec eq ([x2, s2] <-$2 o1 s d1; [x3, s3] <-$2 c2 _ _ o2 s2; ret ((x2, x3), s3)) ([x3, s2] <-$2 c2 _ _ o2 s; [x2, s3] <-$2 o1 s2 d1; ret ((x2, x3), s3)) ) -> comp_spec eq ([x2, s2] <-$2 c1 _ _ o1 s; [x3, s3] <-$2 c2 _ _ o2 s2; ret ((x2, x3), s3)) ([x3, s2] <-$2 c2 _ _ o2 s; [x2, s3] <-$2 c1 _ _ o1 s2; ret ((x2, x3), s3)).
proof: Proof. induction c1; intuition idtac; simpl in *. specialize (@H s a). despec. intuition idtac. exists x. intuition idtac. eapply eqRat_trans. 2:{ eapply eqRat_trans. eapply H0. unfold marginal_l. fcf_skip. eapply evalDist_ret_eq. simpl. case_eq (eqbPair (pair_EqDec eqda1 eqda2) eqds (fst x0) (a1, b0, b)); intros. case_eq (eqbPair (pair_EqDec eqdr1 eqda2) eqds (fst x0) (a1, b0, b)); intros. eauto. apply eqbPair_prop in H3. destruct x0; simpl in *; subst. rewrite eqbPair_refl in H4. discriminate. case_eq (eqbPair (pair_EqDec eqdr1 eqda2) eqds (fst x0) (a1, b0, b)); intros. apply eqbPair_prop in H4. destruct x0; simpl in *; subst. rewrite eqbPair_refl in H3. discriminate. trivial. } fcf_skip. fcf_simp. fcf_skip. fcf_simp. fcf_compute. eapply eqRat_trans. 2:{ eapply eqRat_trans. eapply H. unfold marginal_r. fcf_skip. eapply evalDist_ret_eq. simpl. case_eq (eqbPair (pair_EqDec eqda1 eqda2) eqds (snd x0) (a1, b0, b)); intros. case_eq (eqbPair (pair_EqDec eqdr1 eqda2) eqds (snd x0) (a1, b0, b)); intros. eauto. apply eqbPair_prop in H3. destruct x0; simpl in *; subst. rewrite eqbPair_refl in H4. discriminate. case_eq (eqbPair (pair_EqDec eqdr1 eqda2) eqds (snd x0) (a1, b0, b)); intros. apply eqbPair_prop in H4. destruct x0; simpl in *; subst. rewrite eqbPair_refl in H3. discriminate. trivial. } fcf_skip. fcf_simp. fcf_skip. fcf_simp. fcf_compute. assert (A -> B * S) as bs. intros. eapply oc_base_exists; eauto. intuition idtac. assert (B' * S0). eapply comp_base_exists; eauto. intuition idtac. assert C as c. eapply oc_base_exists; eauto. intuition idtac. assert (D2 -> R2) as r2. intuition idtac. assert (R2 * S0). eapply comp_base_exists; eauto. intuition idtac. assert A2 as a2. eapply oc_base_exists; eauto. fcf_inline_first. assert (EqDec C). eapply EqDec_pair_l; eauto. eapply (@comp_spec_eq_trans_l _ _ _ _ _ (y <-$ (a <-$ c1 (S * S0)%type (pair_EqDec e eqds) (fun (x : S * S0) (y : A) => p <-$ (o (fst x) y) S0 eqds o1 (snd x); ret (fst (fst p), (snd (fst p), snd p))) (s, s0); [x2, s3]<-2 a; z0 <-$ c2 (S * S0)%type _ (fun p d => r <-$ o2 (snd p) d; ret (fst r, (fst p, snd r))) s3; [x3, s4]<-2 z0; ret (x2, x3, s4)); ret (((fst (fst y), fst (snd y)), (snd (fst y))), (snd (snd y)))) ). fcf_inline_first. fcf_skip. fcf_inline_first. fcf_skip. simpl. eapply (@fcf_oracle_eq _ _ (fun p1 p2 => p1 = (snd p2) /\ fst p2 = a)); intuition idtac. subst. eapply comp_spec_eq_trans_l. eapply comp_spec_symm. eapply comp_spec_consequence. eapply comp_spec_right_ident. intros; subst; trivial. fcf_skip. simpl. eapply comp_spec_ret; intuition idtac. simpl. fcf_simp. simpl in *; intuition idtac; subst. eapply comp_spec_ret; intuition idtac. specialize (@IHc1 _ _ _ c2 _ _ _ _ (S * S0)%type _ (fun (x : S * S0) (y : A) => p <-$ (o (fst x) y) S0 eqds o1 (snd x); ret (fst (fst p), (snd (fst p), snd p))) (fun (p : S * S0) (d : D2) => r <-$ o2 (snd p) d; ret (fst r, (fst p, snd r)))). eapply (@ comp_spec_eq_trans_r _ _ _ _ _ (y <-$ (z <-$ c2 _ _ (fun (p : S * S0) (d : D2) => r <-$ o2 (snd p) d; ret (fst r, (fst p, snd r))) (s, s0); [x3, s3]<-2 z; z0 <-$ c1 _ _ (fun (x : S * S0) (y : A) => p <-$ (o (fst x) y) S0 eqds o1 (snd x); ret (fst (fst p), (snd (fst p), snd p))) s3; [x2, s4]<-2 z0; ret (x2, x3, s4)); ret (((fst (fst y), fst (snd y)), (snd (fst y))), (snd (snd y)))) ). eapply comp_spec_seq_eq. intuition idtac. intuition idtac. eapply IHc1. intuition idtac. simpl in *. subst. eapply (@ comp_spec_eq_trans_l _ _ _ _ _ (y <-$(z <-$ (o a d1) S0 eqds o1 b; [x2, s3]<-2 z; z0 <-$ c2 _ _ o2 s3; [x3, s4]<-2 z0; ret (x2, x3, s4)); ret ((fst (fst (fst y)), (snd (fst y))), (snd (fst (fst y)), (snd y))) ) ). fcf_inline_first. fcf_skip. simpl. fcf_inline_first. fcf_skip. eapply (@fcf_oracle_eq _ _ (fun p1 p2 => (snd p1) = p2 /\ fst p1 = b2)); intuition idtac. subst. eapply comp_spec_eq_trans_r. 2:{ eapply comp_spec_right_ident. } fcf_skip. eapply comp_spec_ret; intuition idtac. fcf_simp. simpl in *; intuition idtac. subst. eapply comp_spec_ret; intuition idtac. eapply (@ comp_spec_eq_trans_r _ _ _ _ _ (y <-$ (z <-$ c2 _ _ o2 b; [x2, s3] <-2 z; z0 <-$ (o a d1) _ _ o1 s3; [x3, s4] <-2 z0; ret (x3, x2, s4)); ret ((fst (fst (fst y)), (snd (fst y))), (snd (fst (fst y)), (snd y))) ) ). eapply comp_spec_seq. intuition idtac. intuition idtac. eapply H; eauto. intuition idtac. subst. eapply comp_spec_ret; intuition idtac. fcf_inline_first. fcf_skip. eapply (@fcf_oracle_eq _ _ (fun p1 p2 => p1 = (snd p2) /\ fst p2 = a)); intuition idtac. subst. eapply comp_spec_eq_trans_l. eapply comp_spec_symm. eapply comp_spec_consequence. eapply comp_spec_right_ident. intros; subst; trivial. fcf_skip. eapply comp_spec_ret; intuition idtac. simpl in *; intuition idtac; subst. fcf_inline_first. fcf_simp. fcf_inline_first. fcf_skip. fcf_simp. eapply comp_spec_eq_refl. intros. eapply comp_spec_eq_refl. fcf_inline_first. fcf_skip. eapply (@fcf_oracle_eq _ _ (fun p1 p2 => snd p1 = p2 /\ fst p1 = s)); intuition idtac. subst. simpl. eapply comp_spec_eq_trans_r. 2:{ eapply comp_spec_right_ident. } fcf_skip. eapply comp_spec_ret; simpl in *; intuition idtac. simpl in *; intuition idtac; subst. fcf_simp. fcf_inline_first. fcf_skip. simpl. fcf_simp. eapply comp_spec_ret; intuition idtac. assert C as c_ex. eapply comp_base_exists; eauto. assert A2 as a2_ex. eapply oc_base_exists; eauto. intuition idtac. assert (R2 * S). eapply comp_base_exists; eauto. intuition idtac. fcf_inline_first. eapply (@comp_spec_eq_trans_l _ _ _ _ _ (a <-$ c; z0 <-$ c2 S eqds o2 s; [x3, s4]<-2 z0; ret (a, x3, s4)) ). fcf_skip. fcf_swap leftc. fcf_skip. fcf_inline_first. fcf_skip. fcf_simp. eapply comp_spec_ret; intuition idtac. assert C as c_ex. eapply oc_base_exists; eauto. intuition idtac. assert (B * S). eapply comp_base_exists; eauto. intuition idtac. assert C' as c'_ex. eapply oc_base_exists. eapply o. intuition idtac. intuition idtac. assert (B * S). eapply comp_base_exists; eauto. intuition idtac. assert A2 as a2_ex. eapply oc_base_exists; eauto. intuition idtac. assert (R2 * S). eapply comp_base_exists; eauto. intuition idtac. fcf_inline_first. eapply (@comp_spec_eq_trans_l _ _ _ _ _ (a <-$ c1 S eqds o1 s; [z, s']<-2 a; z <-$ ((o z) S eqds o1 s'); [x2, s3]<-2 z; z0 <-$ c2 S eqds o2 s3; [x3, s4]<-2 z0; ret (x2, x3, s4)) ). fcf_skip. eapply (@comp_spec_eq_trans _ _ _ (a <-$ c1 S eqds o1 s; [z, s']<-2 a; z1 <-$ c2 S eqds o2 s'; [x2, s3]<-2 z1; z0 <-$ ((o z) S eqds o1 s3); [x3, s4]<-2 z0; ret (x3, x2, s4)) ). fcf_skip. eapply H; intuition idtac. eapply (@comp_spec_eq_trans_l _ _ _ _ _ (y <-$ (a <-$ c1 S eqds o1 s; [z, s']<-2 a; z1 <-$ c2 S eqds o2 s'; [x2, s3]<-2 z1; ret (z, x2, s3) ); z0 <-$ (o (fst (fst y))) S eqds o1 (snd y); [x3, s4]<-2 z0; ret (x3, (snd (fst y)), s4)) ). fcf_inline_first. fcf_skip. fcf_inline_first. fcf_skip. fcf_simp. simpl. fcf_inline_first. eapply comp_spec_eq_refl. eapply (@comp_spec_eq_trans_r _ _ _ _ _ (y <-$ (a <-$ c2 S eqds o2 s; [z, s']<-2 a; z1 <-$ c1 S eqds o1 s'; [x2, s3]<-2 z1; ret (x2, z, s3) ); z0 <-$ (o (fst (fst y))) S eqds o1 (snd y); [x3, s4]<-2 z0; ret (x3, (snd (fst y)), s4)) ). eapply comp_spec_seq. intuition idtac. intuition idtac. eapply IHc1; intuition idtac. intuition idtac. subst. fcf_skip. fcf_inline_first. fcf_skip. fcf_inline_first. fcf_skip. simpl. fcf_skip. Unshelve. eapply pair_EqDec; intuition idtac. eapply oc_EqDec. eauto. intuition idtac. assert (B * S). eapply comp_base_exists; eauto. intuition idtac. intuition idtac. eapply pair_EqDec; intuition idtac. eapply oc_EqDec. eauto. intuition idtac. assert (B * S). eapply comp_base_exists; eauto. intuition idtac. intuition idtac. eapply pair_EqDec; intuition idtac. eapply oc_EqDec. eauto. intuition idtac. assert (B * S). eapply comp_base_exists; eauto. intuition idtac. intuition idtac. eapply oc_EqDec. eauto. intuition idtac. assert (B * S). eapply comp_base_exists; eauto. intuition idtac. intuition idtac. eapply pair_EqDec; intuition idtac. eapply oc_EqDec. eauto. intuition idtac. assert (B * S). eapply comp_base_exists; eauto. intuition idtac. intuition idtac. Qed.
imports: FCF FCF.PRF Permutation