proposition: Theorem fundamental_lemma : forall (A B : Set)(eqda : EqDec A)(eqdb : EqDec B)(c1 c2 : Comp A)(badness : A -> bool)(proj : A -> B), Pr [a <-$ c1; ret (badness a)] == Pr[a <-$ c2; ret (badness a)] -> (forall x, evalDist (a <-$ c1; ret (proj a, badness a)) (x, false) == evalDist (a <-$ c2; ret (proj a, badness a)) (x, false)) -> forall x, | (evalDist (a <-$ c1; ret (proj a)) x) - (evalDist (a <-$ c2; ret (proj a)) x) | <= Pr [a <-$ c1; ret (badness a)].
proof: Proof. intuition. specialize (@fundamental_lemma_h B eqdb (a <-$ c1; ret (proj a, badness a)) (a <-$ c2; ret (proj a, badness a)) ); intuition. assert ( | evalDist (x <-$ (a0 <-$ c1; ret (proj a0, badness a0)); ret fst x) x - evalDist (x <-$ (a0 <-$ c2; ret (proj a0, badness a0)); ret fst x) x | == | evalDist (a <-$ c1; ret proj a) x - evalDist (a <-$ c2; ret proj a) x |). eapply ratDistance_eqRat_compat. eapply eqRat_trans. eapply evalDist_assoc_eq. cbv beta. eapply eqRat_trans. eapply evalDist_seq_eq. intuition. eapply eqRat_refl. intuition. eapply eqRat_trans. eapply evalDist_left_ident_eq. eapply eqRat_refl. cbv beta. unfold fst. intuition. eapply eqRat_trans. eapply evalDist_assoc_eq. cbv beta. eapply evalDist_seq_eq; intuition. eapply evalDist_left_ident_eq. rewrite <- H2. rewrite H1. eapply leRat_trans. eapply eqRat_impl_leRat. eapply eqRat_trans. eapply evalDist_assoc_eq. cbv beta. eapply evalDist_seq_eq; intuition. eapply eqRat_refl. eapply eqRat_trans. eapply evalDist_left_ident_eq. cbv beta. eapply eqRat_refl. cbv beta. unfold snd. intuition. eapply eqRat_trans. eapply evalDist_assoc_eq. eapply eqRat_trans. eapply evalDist_seq_eq; intuition. eapply eqRat_refl. eapply eqRat_trans. eapply evalDist_left_ident_eq. cbv beta. eapply eqRat_refl. rewrite H. symmetry. eapply eqRat_trans. eapply evalDist_assoc_eq. eapply eqRat_trans. eapply evalDist_seq_eq; intuition. eapply eqRat_refl. eapply eqRat_trans. eapply evalDist_left_ident_eq. eapply eqRat_refl. cbv beta. simpl. intuition. intuition. Qed.
imports: FCF.DistSem FCF.Fold Permutation FCF.SemEquiv FCF.DetSem FCF.NotationV1 micromega.Lia