proposition: Lemma IND_CPA_ideal_real : IND_CPA false ≈₀ IND_CPA true.
proof: Proof. eapply eq_rel_perf_ind_eq. simplify_eq_rel m. eapply r_const_sample_L with (op := uniform _). 1: exact _. intro m_val. pose (f := λ (k : Arit (uniform i_key)), words2ch (ch2key k ⊕ ch2words m ⊕ (ch2words m_val)) ). assert (bij_f : bijective f). { subst f. exists (λ x, words2ch (ch2words x ⊕ (ch2words m_val) ⊕ ch2words m)). - intro x. rewrite ch2words_words2ch. rewrite !plus_involutive. apply words2ch_ch2key. - intro x. rewrite ch2key_words2ch. rewrite !plus_involutive. apply words2ch_ch2words. } eapply r_uniform_bij with (1 := bij_f). intro k_val. apply r_ret. intros s₀ s₁ e. intuition auto. subst f. simpl. f_equal. rewrite ch2key_words2ch. rewrite <- plus_assoc. rewrite [X in _ = X]plus_comm. f_equal. rewrite plus_comm. rewrite plus_involutive. reflexivity. Qed.
imports: Relational(OrderEnrichedCategory GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr fingroup.fingroup realsum ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice seq) Crypt(Axioms ChoiceAsOrd SubDistr Couplings UniformDistrLemmas FreeProbProg Theta_dens RulesStateProb UniformStateProb pkg_composition pkg_rhl Package Prelude) Coq(Utf8 Lia) extructures(ord fset fmap) Equations(Equations)