proposition: Theorem ExpROM_query_swap_spec : forall (D2 R2 : Set) (A2 : Set) (c2 : OracleComp D2 R2 A2) (D1 R1 : Set) (A1 : Set) (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 d, (forall s d1 d2, comp_spec eq ([x2, s2] <-$2 o1 s d1; [x3, s3] <-$2 o2 s2 d2; ret ((x2, x3), s3)) ([x3, s2] <-$2 o2 s d2; [x2, s3] <-$2 o1 s2 d1; ret ((x2, x3), s3)) ) -> comp_spec eq ([x2, s2] <-$2 o1 s d; [x3, s3] <-$2 c2 _ _ o2 s2; ret ((x2, x3), s3)) ([x3, s2] <-$2 c2 _ _ o2 s; [x2, s3] <-$2 o1 s2 d; ret ((x2, x3), s3)).
proof: Proof. induction c2; intuition idtac; simpl in *. specialize (@H s d 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 eqdr1 eqda2) eqds (fst x0) (a1, b0, b)); intros. case_eq (eqbPair (pair_EqDec eqdr1 eqdr2) 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 eqdr2) 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 eqdr1 eqda2) eqds (snd x0) (a1, b0, b)); intros. case_eq (eqbPair (pair_EqDec eqdr1 eqdr2) 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 eqdr2) 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 R1 as r1_ex. assert (R1 * S0). eapply comp_base_exists. eauto. intuition idtac. assert (A' -> B') as b'_ex. intros. assert (B' * S0). eapply comp_base_exists; eauto. intuition idtac. assert (A -> B) as b_ex. intros. assert (B * S). eapply oc_base_exists. eapply o. trivial. trivial. trivial. intuition idtac. assert C as c_ex. eapply oc_base_exists. eauto. intuition idtac. fcf_inline_first. assert (EqDec C). eapply EqDec_pair_l; eauto. eapply (@comp_spec_eq_trans_l _ _ _ _ _ (y <-$ (z <-$ (fun p d => r <-$ o1 (snd p) d; ret (fst r, (fst p, snd r))) (s, s0) d; [x2, s2]<-2 z; z0 <-$ c2 (S * S0)%type (pair_EqDec e eqds) (fun (x : S * S0) (y : A) => p <-$ (o (fst x) y) S0 eqds o2 (snd x); ret (fst (fst p), (snd (fst p), snd p))) s2; [x3, s3]<-2 z0; ret (x2, x3, s3)); ret ((fst (fst y)), (snd (fst y), fst (snd y)), snd (snd y))) ). fcf_inline_first. fcf_skip. fcf_simp. fcf_inline_first. fcf_skip. fcf_simp. eapply comp_spec_ret; intuition idtac. specialize (@IHc2 _ _ _ _ _ _ _ (S * S0)%type _ (fun p d => r <-$ o1 (snd p) d; ret (fst r, (fst p, snd r))) (fun (x : S * S0) (y : A) => p <-$ (o (fst x) y) S0 eqds o2 (snd x); ret (fst (fst p), (snd (fst p), snd p))) ). eapply (@comp_spec_eq_trans_r _ _ _ _ _ (y <-$ (z <-$ c2 (S * S0)%type (pair_EqDec e eqds) (fun (x : S * S0) (y : A) => p <-$ (o (fst x) y) S0 eqds o2 (snd x); ret (fst (fst p), (snd (fst p), snd p))) (s, s0); [x3, s2]<-2 z; z0 <-$ (fun (p : S * S0) (d0 : D1) => r <-$ o1 (snd p) d0; ret (fst r, (fst p, snd r))) s2 d; [x2, s3]<-2 z0; ret (x2, x3, s3)); ret (fst (fst y), (snd (fst y), fst (snd y)), snd (snd y))) ). eapply comp_spec_seq. intuition idtac. intuition idtac. eapply IHc2. intuition idtac. simpl. eapply (@comp_spec_eq_trans_l _ _ _ _ _ ([a, b, c] <-$3 (r <-$ o1 b d1; [x2, s2] <-2 r; z0 <-$ (o a d2) S0 eqds o2 s2; [x3, s3]<-2 z0; ret (x2, x3, s3)); ret (a, (fst b), (snd b, c))) ). fcf_inline_first. fcf_skip. fcf_inline_first. simpl. fcf_skip. fcf_simp. eapply comp_spec_ret; intuition idtac. eapply (@comp_spec_eq_trans_r _ _ _ _ _ ([a, b, c] <-$3 (z <-$ (o a d2) S0 eqds o2 b; [x3, s2]<-2 z; z0 <-$ o1 s2 d1; [x2, s3]<-2 z0; ret (x2, x3, s3)); ret (a, (fst b), (snd b, c))) ). eapply comp_spec_seq_eq. intuition idtac. intuition idtac. eapply H; intuition idtac. eauto. intuition idtac. eapply comp_spec_eq_refl. fcf_inline_first. fcf_skip. fcf_simp. simpl. fcf_inline_first. fcf_skip. fcf_simp. apply comp_spec_ret; intuition idtac. intuition idtac. subst. simpl in *. eapply comp_spec_ret; intuition idtac. fcf_inline_first. fcf_skip. fcf_inline_first. fcf_simp. fcf_skip. simpl. eapply comp_spec_ret; intuition idtac. assert R1 as r1_ex. assert (R1 * S). eapply comp_base_exists; eauto. intuition idtac. assert C as c_ex. apply comp_base_exists; eauto. fcf_inline_first. eapply comp_spec_eq_symm. eapply (@comp_spec_eq_trans _ _ _ (a <-$ c; z0 <-$ o1 s d; [x2, s3]<-2 z0; ret (x2, a, s3)) ). fcf_skip. fcf_swap leftc. fcf_skip. fcf_inline_first. fcf_skip. fcf_simp. eapply comp_spec_ret; intuition idtac. assert R1 as r1_ex. assert (R1 * S). eapply comp_base_exists; eauto. intuition idtac. assert (A -> B). intros. assert (B * S). eapply comp_base_exists; eauto. intuition idtac. assert C as c_ex. eapply oc_base_exists; eauto. assert C' as c'_ex. eapply oc_base_exists. eapply o. trivial. intuition idtac. fcf_inline_first. eapply (@comp_spec_eq_trans_l _ _ _ _ _ ([a, b, c] <-$3 (z <-$ o1 s d; [x2, s2]<-2 z; z0 <-$ c2 S eqds o2 s2; [z1, s']<-2 z0; ret (x2, z1, s')); z1 <-$ ((o b) S eqds o2 c); [x3, s3]<-2 z1; ret (a, x3, s3)) ). fcf_inline_first. fcf_skip. fcf_inline_first. fcf_skip. fcf_simp. eapply comp_spec_eq_refl. eapply (@comp_spec_eq_trans _ _ _ ([a, b, c] <-$3 (z <-$ c2 S eqds o2 s; [x3, s2]<-2 z; z0 <-$ o1 s2 d; [x2, s3]<-2 z0; ret (x2, x3, s3)); z1 <-$ ((o b) S eqds o2 c); [x3, s3]<-2 z1; ret (a, x3, s3)) ). eapply comp_spec_seq_eq. intuition idtac. intuition idtac. eapply IHc2; intuition idtac. eauto. intuition idtac. eapply comp_spec_eq_refl. fcf_inline_first. fcf_skip. eapply comp_spec_eq_trans. 2:{ eapply H; intuition idtac. eauto. } fcf_inline_first. fcf_skip. Unshelve. eapply pair_EqDec; intuition idtac. eapply oc_EqDec. eauto. intuition idtac. intuition idtac. eapply oc_EqDec. eauto. intuition idtac. intuition idtac. eapply pair_EqDec; intuition idtac. eapply oc_EqDec. eauto. intuition idtac. intuition idtac. Qed.
imports: FCF FCF.PRF Permutation