From f95fb3c986ead89b500be55b805c208e4204d790 Mon Sep 17 00:00:00 2001 From: Alejandro Aguirre Date: Thu, 21 Nov 2024 14:48:16 +0100 Subject: [PATCH] Multiplicative approximate lifting --- theories/prob/couplings_exp.v | 240 ++++++++++++++++++++++++++++++++++ 1 file changed, 240 insertions(+) create mode 100644 theories/prob/couplings_exp.v diff --git a/theories/prob/couplings_exp.v b/theories/prob/couplings_exp.v new file mode 100644 index 00000000..42dfd13f --- /dev/null +++ b/theories/prob/couplings_exp.v @@ -0,0 +1,240 @@ +From Coq Require Import Reals Psatz. +From Coq.ssr Require Import ssreflect ssrfun. +From Coquelicot Require Import Rcomplements Lim_seq Rbar. +From stdpp Require Export countable. +From clutch.prelude Require Export base Coquelicot_ext Reals_ext stdpp_ext. +From clutch.prob Require Export countable_sum distribution couplings graded_predicate_lifting. + +Open Scope R. + + +Section couplings. + Context `{Countable A, Countable B, Countable A', Countable B'}. + Context (μ1 : distr A) (μ2 : distr B) (S : A -> B -> Prop). + + Definition ARcoupl (ε : R) := + forall (f: A → R) (g: B -> R), + (forall a, 0 <= f a <= 1) -> + (forall b, 0 <= g b <= 1) -> + (forall a b, S a b -> f a <= g b) -> + SeriesC (λ a, μ1 a * f a) <= exp(ε) * SeriesC (λ b, μ2 b * g b). + +End couplings. + +Section couplings_theory. + Context `{Countable A, Countable B, Countable A', Countable B'}. + + + Lemma exp_mono (r s : R) : r <= s -> exp r <= exp s. + Proof. + intros [| ->]. + + left. + by apply exp_increasing. + + lra. + Qed. + + + Lemma exp_pos_ge_1 (r : R) : 0 <= r -> 1 <= exp r. + Proof. + intros. + trans (exp 0); last by apply exp_mono. + by rewrite exp_0. + Qed. + + + Lemma ARcoupl_mono (μ1 μ1': distr A') (μ2 μ2': distr B') R R' ε ε': + (∀ a, μ1 a = μ1' a) -> + (∀ b, μ2 b = μ2' b) -> + (∀ x y, R x y -> R' x y) -> + (ε <= ε') -> + ARcoupl μ1 μ2 R ε -> + ARcoupl μ1' μ2' R' ε'. + Proof. + intros Hμ1 Hμ2 HR Hε Hcoupl f g Hf Hg Hfg. + specialize (Hcoupl f g Hf Hg). + replace (μ1') with μ1; last by apply distr_ext. + replace (μ2') with μ2; last by apply distr_ext. + trans (exp(ε) * SeriesC (λ b, μ2 b * g b)). + - apply Hcoupl. + naive_solver. + - apply Rmult_le_compat_r; first by series. + by apply exp_mono. + Qed. + + + Lemma ARcoupl_mon_grading (μ1 : distr A') (μ2 : distr B') (R : A' → B' → Prop) ε1 ε2 : + (ε1 <= ε2) -> + ARcoupl μ1 μ2 R ε1 -> + ARcoupl μ1 μ2 R ε2. + Proof. + intros Hleq. + by apply ARcoupl_mono. + Qed. + + + Lemma ARcoupl_dret (a : A) (b : B) (R : A → B → Prop) r : + 0 <= r → + R a b → ARcoupl (dret a) (dret b) R r. + Proof. + intros Hr HR f g Hf Hg Hfg. + assert (SeriesC (λ a0 : A, dret a a0 * f a0) = f a) as ->. + { rewrite <-(SeriesC_singleton a (f a)). + rewrite /pmf/=/dret_pmf ; series. + } + assert (SeriesC (λ b0 : B, dret b b0 * g b0) = g b) as ->. + { rewrite <-(SeriesC_singleton b (g b)). + rewrite /pmf/=/dret_pmf ; series. + } + specialize (Hfg _ _ HR). + rewrite <- (Rmult_1_l (f a)). + apply Rmult_le_compat; [real_solver | real_solver | | auto]. + by apply exp_pos_ge_1. + Qed. + + + (* The hypothesis (0 ≤ ε1) is not really needed, I just kept it for symmetry *) + Lemma ARcoupl_dbind (f : A → distr A') (g : B → distr B') + (μ1 : distr A) (μ2 : distr B) (R : A → B → Prop) (S : A' → B' → Prop) ε1 ε2 : + (Rle 0 ε1) -> (Rle 0 ε2) -> + (∀ a b, R a b → ARcoupl (f a) (g b) S ε2) → ARcoupl μ1 μ2 R ε1 → ARcoupl (dbind f μ1) (dbind g μ2) S (ε1 + ε2). + Proof. + intros Hε1 Hε2 Hcoup_fg Hcoup_R h1 h2 Hh1pos Hh2pos Hh1h2S. + rewrite /pmf/=/dbind_pmf. + (* To use the hypothesis that we have an R-ACoupling up to ε1 for μ1, μ2, + we have to rewrite the sums in such a way as to isolate (the expectation + of) a random variable X on the LHS and Y on the RHS, and ε1 on the + RHS. *) + (* First step: rewrite the LHS into a RV X on μ1. *) + setoid_rewrite <- SeriesC_scal_r. + rewrite <-(fubini_pos_seriesC (λ '(a,x), μ1 x * f x a * h1 a)). + + (* Boring Fubini sideconditions. *) + 2: { real_solver. } + 2: { intro a'. + (* specialize (Hh1pos a'). *) + apply (ex_seriesC_le _ μ1); auto. + intro a; split. + + apply Rmult_le_pos. + * real_solver. + * real_solver. + + rewrite <- Rmult_1_r. + rewrite Rmult_assoc. + apply Rmult_le_compat_l; auto. + rewrite <- Rmult_1_r. + apply Rmult_le_compat; real_solver. } + 2: { setoid_rewrite SeriesC_scal_r. + apply (ex_seriesC_le _ (λ a : A', SeriesC (λ x : A, μ1 x * f x a))); auto. + + series. + + apply (pmf_ex_seriesC (dbind f μ1)). } + + (* LHS: Pull the (μ1 b) factor out of the inner sum. *) + assert (SeriesC (λ b : A, SeriesC (λ a : A', μ1 b * f b a * h1 a)) = + SeriesC (λ b : A, μ1 b * SeriesC (λ a : A', f b a * h1 a))) as ->. + { setoid_rewrite <- SeriesC_scal_l. series. } + + (* Second step: rewrite the RHS into a RV Y on μ2. *) + (* RHS: Fubini. *) + rewrite <-(fubini_pos_seriesC (λ '(b,x), μ2 x * g x b * h2 b)). + 2: by series. + 2:{ intro b'. + specialize (Hh2pos b'). + apply (ex_seriesC_le _ μ2) ; auto. + intro b; split. + - series. + - do 2 rewrite <- Rmult_1_r. series. } + 2:{ setoid_rewrite SeriesC_scal_r. + apply (ex_seriesC_le _ (λ a : B', SeriesC (λ b : B, μ2 b * g b a))); auto. + - intros b'; specialize (Hh2pos b'); split. + + apply Rmult_le_pos; [ | lra]. + apply (pmf_pos ((dbind g μ2)) b'). + + rewrite <- Rmult_1_r. + apply Rmult_le_compat_l; auto. + * apply SeriesC_ge_0'. real_solver. + * real_solver. + - apply (pmf_ex_seriesC (dbind g μ2)). } + + (* RHS: Factor out (μ2 b) *) + assert (SeriesC (λ b : B, SeriesC (λ a : B', μ2 b * g b a * h2 a)) + = SeriesC (λ b : B, μ2 b * SeriesC (λ a : B', g b a * h2 a))) as ->. + { apply SeriesC_ext; intro. + rewrite <- SeriesC_scal_l. + apply SeriesC_ext; real_solver. } + + + (* To construct X, we want to push ε2 into the inner sum. We don't do this + directly, because X might be larger than 1, but + our assumption on the ε1 R-ACoupling requires it to be valued in [0,1]. + Instead, we take min(1, exp(ε2) * (Σ(a:A')(f b a * h1 a))). + ALT: could use a more fine-grained min inside the sum? + *) + + assert (exp (ε1) * SeriesC (λ b : B, μ2 b * (Rmin 1 (exp (ε2) * SeriesC (λ a : B', g b a * h2 a)))) + <= exp (ε1 + ε2) * SeriesC (λ b : B, μ2 b * SeriesC (λ a : B', g b a * h2 a))) as <-. + { + rewrite exp_plus. + rewrite Rmult_assoc. + rewrite -(SeriesC_scal_l _ (exp ε2)). + apply Rmult_le_compat_l; [left; apply exp_pos |]. + apply SeriesC_le. + - intros b; split. + + apply Rmult_le_pos; auto. + apply Rmin_glb; [lra |]. + apply Rmult_le_pos; [left; apply exp_pos |]. + apply SeriesC_ge_0'. + real_solver. + + rewrite Rmult_min_distr_l; auto. + etrans; [apply Rmin_r | lra]. + - apply ex_seriesC_scal_l. + apply (ex_seriesC_le _ μ2); auto. + intro b; split. + + apply Rmult_le_pos; auto. + apply SeriesC_ge_0'. + intro; apply Rmult_le_pos; auto. + apply Hh2pos. + + rewrite <- Rmult_1_r. + apply Rmult_le_compat_l; auto. + apply (Rle_trans _ (SeriesC (g b))); auto. + apply SeriesC_le; auto. + real_solver. + } + + (* + Now we instantiate the lifting definitions and use them to prove the + inequalities + *) + rewrite /ARcoupl in Hcoup_R. + apply Hcoup_R. + + intro; split; series. + apply (Rle_trans _ (SeriesC (f a))); auto. + apply SeriesC_le; auto. + intro a'. + specialize (Hh1pos_l a'); real_solver. + + intro; split. + * apply Rmin_glb; [lra |]. + apply Rmult_le_pos. + ** left. apply exp_pos. + ** apply SeriesC_ge_0'; intro b'. + specialize (Hh2pos b'); real_solver. + * apply Rmin_l. + + + intros a b Rab. + apply Rmin_glb. + * apply (Rle_trans _ (SeriesC (f a))); auto. + apply SeriesC_le; auto. + intro a'. + real_solver. + * by apply Hcoup_fg. + Qed. + + + Lemma ARcoupl_dbind' (ε1 ε2 ε : R) (f : A → distr A') (g : B → distr B') + (μ1 : distr A) (μ2 : distr B) (R : A → B → Prop) (S : A' → B' → Prop) : + (0 <= ε1) → (0 <= ε2) → + ε = ε1 + ε2 → + (∀ a b, R a b → ARcoupl (f a) (g b) S ε2) → + ARcoupl μ1 μ2 R ε1 → + ARcoupl (dbind f μ1) (dbind g μ2) S ε. + Proof. intros ? ? ->. by eapply ARcoupl_dbind. Qed. + +End couplings_theory. +