proposition: Theorem sortedRandomFunc_swap : forall s d1 d2, comp_spec eq ([x2, s2] <-$2 sortedRandomFunc s d1; [x3, s3] <-$2 sortedRandomFunc s2 d2; ret ((x2, x3), s3)) ([x3, s2] <-$2 sortedRandomFunc s d2; [x2, s3] <-$2 sortedRandomFunc s2 d1; ret ((x2, x3), s3)).
proof: Proof. intuition idtac. assert B. eapply comp_base_exists; eauto. unfold sortedRandomFunc. case_eq (eqb d1 d2); intros. rewrite eqb_leibniz in H0. subst. matchOpt. fcf_simp. rewrite H0. fcf_simp. eapply comp_spec_eq_refl. fcf_inline_first. fcf_skip. fcf_simp. rewrite arrayLookup_insertInOrder_same. fcf_simp. eapply comp_spec_eq_refl. matchOpt. fcf_simp. matchOpt. fcf_simp. rewrite H1. fcf_simp. eapply comp_spec_ret; intuition idtac. fcf_inline_first. fcf_skip. fcf_simp. rewrite arrayLookup_insertInOrder_ne. rewrite H1. fcf_simp. apply comp_spec_eq_refl. intuition idtac; subst. rewrite eqb_refl in *. discriminate. matchOpt. fcf_simp. rewrite H1. fcf_inline_first. fcf_skip. rewrite arrayLookup_insertInOrder_ne. rewrite H2. fcf_simp. eapply comp_spec_eq_refl. intuition idtac; subst. rewrite eqb_refl in *. discriminate. fcf_inline_first. eapply (@comp_spec_eq_trans _ _ _ (a <-$ rndB; b1 <-$ rndB; z <-$ ret (a, insertInOrder s d1 a); [x2, s2]<-2 z; z0 <-$ ( ret (b1, insertInOrder s2 d2 b1)); [x3, s3]<-2 z0; ret (x2, x3, s3)) ). fcf_skip. rewrite arrayLookup_insertInOrder_ne. rewrite H2. fcf_inline_first. fcf_skip. fcf_simp. eapply comp_spec_eq_refl. intuition idtac; subst. rewrite eqb_refl in *. discriminate. fcf_swap leftc. fcf_skip. fcf_simp. rewrite arrayLookup_insertInOrder_ne. rewrite H1. fcf_inline_first. fcf_skip. fcf_simp. eapply comp_spec_ret; intuition idtac. f_equal. eapply insertInOrder_twice_eq. intuition idtac; subst. rewrite eqb_refl in *; discriminate. intuition idtac; subst. rewrite eqb_refl in *; discriminate. Qed.
imports: FCF FCF.PRF Permutation