proposition: Theorem le_impl_comp_spec : forall (A B : Set){eqda : EqDec A}{eqdb : EqDec B}(c1 : Comp A)(c2 : Comp B), well_formed_comp c1 -> well_formed_comp c2 -> forall x y, evalDist c1 x <= evalDist c2 y -> comp_spec (fun a b => a = x -> b = y) c1 c2.
proof: Proof. intuition. destruct (eq_Rat_dec (evalDist c2 y) 1). exists (a <-$ c1; b <-$ c2; ret (a, b)). intuition. unfold marginal_l; intuition. dist_inline_first. rewrite <- evalDist_right_ident. dist_skip. dist_inline_first. dist_irr_r. dist_compute. unfold marginal_l; intuition. dist_inline_first. rewrite <- evalDist_right_ident. dist_irr_r. dist_inline_first. dist_skip. dist_compute. repeat simp_in_support. simpl in *. erewrite evalDist_1 in H5; eauto. simpl in *. intuition. destruct (eq_Rat_dec (evalDist c1 x) 0). exists (a <-$ c1; b <-$ c2; ret (a, b)). intuition. unfold marginal_l; intuition. dist_inline_first. rewrite <- evalDist_right_ident. dist_skip. dist_inline_first. dist_irr_r. dist_compute. unfold marginal_l; intuition. dist_inline_first. rewrite <- evalDist_right_ident. dist_irr_r. dist_inline_first. dist_skip. dist_compute. repeat simp_in_support. simpl in *. exfalso. eapply getSupport_In_evalDist. eapply H4. trivial. destruct (eq_Rat_dec (evalDist c1 x) (evalDist c2 y)). eapply comp_spec_consequence. eapply eq_impl_comp_spec; intuition. eauto. intuition. subst. intuition. Local Open Scope rat_scope. exists (a <-$ c1; b <-$ if (eqb a x) then (ret y) else mDiff <- (ratSubtract (evalDist c2 y) (evalDist c1 x)); c <-$ Bernoulli (mDiff * (ratInverse (ratSubtract 1 (evalDist c1 x)))); if c then (ret y) else (Repeat c2 (fun z => negb (eqb z y))); ret (a, b)). intuition. unfold marginal_l. dist_inline_first. rewrite <- evalDist_right_ident. dist_skip. dist_inline_first. dist_irr_r. remember (getSupport c2) as s. destruct s. exfalso. specialize (getSupport_length_nz H0); intuition. rewrite <- Heqs in H3. simpl in *. lia. destruct (EqDec_dec _ b y). subst. destruct s. exfalso. eapply n. rewrite <- (evalDist_lossless H0). rewrite <- Heqs. rewrite sumList_cons. unfold sumList. simpl. eapply ratAdd_0_r. wftac. eapply Bernoulli_wf. eapply (@well_formed_Repeat _ _ _ _ b). intuition. eapply filter_In; intuition. rewrite <- Heqs. simpl. intuition. case_eq (eqb b y); intuition. rewrite eqb_leibniz in H4. subst. specialize (getSupport_NoDup c2); intuition. rewrite <- Heqs in H4. inversion H4; clear H4; subst. simpl in *. intuition. wftac. eapply Bernoulli_wf. eapply (@well_formed_Repeat _ _ _ _ b). intuition. eapply filter_In; intuition. rewrite <- Heqs. simpl. intuition. case_eq (eqb b y); intuition. rewrite eqb_leibniz in H4. subst. intuition. dist_compute. symmetry. unfold marginal_r. dist_inline_first. rewrite evalDist_seq_step. rewrite (sumList_filter_partition (eqb x)). eapply eqRat_trans. eapply ratAdd_eqRat_compat. eapply sumList_body_eq. intros. eapply ratMult_eqRat_compat. eapply eqRat_refl. apply filter_In in H2. intuition. rewrite eqb_leibniz in H4. subst. rewrite eqb_refl. dist_inline_l. simpl snd. eapply eqRat_refl. eapply sumList_body_eq; intuition. apply filter_In in H2. intuition. case_eq (eqb a x); intuition. rewrite eqb_leibniz in H2. subst. rewrite eqb_refl in H4. simpl in *. discriminate. rewrite evalDist_assoc at 1. rewrite evalDist_assoc at 1. rewrite (evalDist_seq_step) at 1. rewrite (sumList_filter_partition (fun z => z)) at 1. rewrite (@sumList_exactly_one _ true) at 1. rewrite (@sumList_exactly_one _ false) at 1. rewrite Bernoulli_correct at 1. rewrite Bernoulli_correct_complement at 1. dist_simp. assert (Pr [a0 <-$ ret y; x0 <-$ ret (a, a0); ret eqb (snd x0) r2 ] == Pr [ret eqb y r2 ]). dist_simp. simpl. intuition. rewrite H5 at 1. clear H5. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply ratAdd_eqRat_compat. eapply eqRat_refl. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply evalDist_seq_eq. intuition. eapply eqRat_refl. intuition. dist_simp. unfold snd. eapply eqRat_refl. eapply ratFraction_le_1. eapply ratSubtract_leRat. eapply evalDist_le_1. intuition. eapply ratFraction_le_1. eapply ratSubtract_leRat. eapply evalDist_le_1. intuition. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_In; intuition. eapply getSupport_In_evalDist. intuition. rewrite Bernoulli_correct_complement in H5. apply ratSubtract_0_inv in H5. apply ratFraction_ge_1_inv in H5. eapply ratSubtract_leRat_same_r in H5. eapply n. eapply leRat_impl_eqRat. eapply evalDist_le_1. trivial. eapply evalDist_le_1. intuition. eapply ratFraction_le_1. eapply ratSubtract_leRat. eapply evalDist_le_1. intuition. intuition. destruct b; intuition. apply filter_In in H5. intuition. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_In. intuition. eapply getSupport_In_evalDist. intuition. rewrite Bernoulli_correct in H5. apply ratMult_0 in H5. intuition. apply ratSubtract_0_inv in H6. eapply n1. eapply leRat_impl_eqRat; intuition. eapply ratInverse_nz;eauto. eapply ratFraction_le_1. eapply ratSubtract_leRat. eapply evalDist_le_1. intuition. intuition. destruct b; intuition. apply filter_In in H5; intuition. discriminate. intuition. intuition. rewrite (@sumList_exactly_one _ x). rewrite sumList_factor_constant_r. assert (sumList (filter (fun a : A => negb (eqb x a)) (getSupport c1)) (evalDist c1) == ratSubtract 1 (evalDist c1 x)). eapply sumList_filter_complement. trivial. rewrite H2. clear H2. rewrite ratMult_distrib. eapply eqRat_trans. eapply ratAdd_eqRat_compat. eapply eqRat_refl. eapply ratAdd_eqRat_compat. rewrite <- ratMult_assoc. eapply ratMult_eqRat_compat. rewrite ratMult_comm. rewrite ratMult_assoc. rewrite ratInverse_prod_1. eapply ratMult_1_r. intuition. eapply n. eapply leRat_impl_eqRat. eapply evalDist_le_1. intuition. eapply leRat_trans; eauto. apply ratSubtract_0_inv. trivial. eapply eqRat_refl. rewrite <- ratMult_assoc. eapply ratMult_eqRat_compat. rewrite ratMult_comm. rewrite ratMult_ratSubtract_distrib_r. rewrite ratMult_1_l. eapply ratSubtract_eqRat_compat. eapply eqRat_refl. rewrite ratMult_assoc. rewrite ratInverse_prod_1. eapply ratMult_1_r. intuition. eapply n. eapply leRat_impl_eqRat. eapply evalDist_le_1. intuition. eapply leRat_trans; eauto. apply ratSubtract_0_inv. trivial. eapply eqRat_refl. case_eq (eqb y r2); intuition. rewrite eqb_leibniz in H2. subst. assert (Pr [ret true] == 1). dist_compute. rewrite H2. clear H2. repeat rewrite ratMult_1_r. assert (Pr [x0 <-$ Repeat c2 (fun z : B => negb (eqb z r2)); ret eqb x0 r2 ] == Pr [x0 <-$ Repeat c2 (fun z : B => negb (eqb z r2)); ret eqb r2 x0 ]). dist_skip; dist_compute. rewrite H2; clear H2. rewrite <- evalDist_event_equiv. rewrite evalDist_Repeat_0. rewrite ratMult_0_r. rewrite <- ratAdd_0_r. eapply ratSubtract_ratAdd_inverse_2. trivial. intuition. subst. rewrite eqb_refl in H3. simpl in *. discriminate. assert (Pr [ret false] == 0). dist_compute. rewrite H3. clear H3. repeat rewrite ratMult_0_r. repeat rewrite <- ratAdd_0_l. rewrite <- ratSubtract_ratAdd_distr. rewrite ratSubtract_ratAdd_inverse_2; trivial. simpl. destruct (in_dec (EqDec_dec _) r2 (getSupport c2)). rewrite (@sumList_exactly_one _ r2). rewrite eqb_refl. destruct (EqDec_dec bool_EqDec true true); intuition. unfold indicator. case_eq (eqb r2 y); intuition. rewrite eqb_leibniz in H3. subst. rewrite eqb_refl in H2. discriminate. simpl. rewrite ratMult_1_l. rewrite ratMult_1_r. assert ((sumList (filter (fun z : B => negb (eqb y z)) (getSupport c2)) (evalDist c2) == (ratSubtract 1 (evalDist c2 y)))). eapply sumList_filter_complement. trivial. eapply eqRat_trans. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply ratMult_eqRat_compat. eapply ratInverse_eqRat_compat. intuition. assert ((filter (fun z : B => negb (eqb y z)) (getSupport c2)) = (filter (fun z : B => negb (eqb z y)) (getSupport c2))). eapply filter_ext; intuition. rewrite eqb_symm. trivial. rewrite H6 in H4. clear H6. rewrite H4 in H5. eapply n. eapply leRat_impl_eqRat. eapply evalDist_le_1. eapply ratSubtract_0_inv. trivial. assert ((filter (fun z : B => negb (eqb z y)) (getSupport c2)) = (filter (fun z : B => negb (eqb y z)) (getSupport c2))). eapply filter_ext. intuition. rewrite eqb_symm. trivial. rewrite H5. clear H5. eapply H4. eapply eqRat_refl. clear H4. rewrite <- ratMult_assoc. symmetry. rewrite <- ratMult_1_l at 1. eapply ratMult_eqRat_compat; intuition. symmetry. rewrite ratMult_comm. eapply ratInverse_prod_1. intuition. eapply n. eapply leRat_impl_eqRat. eapply evalDist_le_1. intuition. eapply ratSubtract_0_inv. trivial. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_In; intuition. case_eq (eqb r2 y); intuition. rewrite eqb_leibniz in H3; subst. rewrite eqb_refl in H2. discriminate. intuition. apply filter_In in H3. intuition. case_eq (eqb b r2); intuition. rewrite eqb_leibniz in H3. subst. intuition. destruct (EqDec_dec bool_EqDec false true ). discriminate. rewrite ratMult_0_r. intuition. eapply eqRat_trans. eapply ratMult_eqRat_compat. eapply eqRat_refl. eapply sumList_0. intuition. apply filter_In in H3. destruct ( EqDec_dec bool_EqDec (eqb a r2) true); intuition. rewrite eqb_leibniz in e; subst. intuition. eapply ratMult_0_r. rewrite ratMult_0_r. symmetry. eapply getSupport_not_In_evalDist. intuition. eapply filter_NoDup. eapply getSupport_NoDup. eapply filter_In; intuition. eapply getSupport_In_evalDist; intuition. apply eqb_refl. intuition. apply filter_In in H2. intuition. dist_compute. repeat simp_in_support; simpl in *; trivial. simpl in *. rewrite eqb_refl in Heqx2. discriminate. Unshelve. intuition. intuition. intuition. intuition. intuition. unfold eq_dec; intuition. eapply (EqDec_dec _). unfold eq_dec; intuition. eapply (EqDec_dec _). Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1