merge fixups

theories/prob/distribution.v

@@ -506,6 +506,10 @@ Section monadic.
     (a ← μ ; b ← f a; g b) = (b ← (a ← μ; f a); g b).
   Proof. apply distr_ext, dbind_assoc_pmf. Qed.
 
+  Lemma dbind_assoc' `{Countable B'} (f : A → distr B) (g : B → distr B') (μ : distr A) :
+    μ ≫= (λ a, f a ≫= g) = (μ ≫= f) ≫= g.
+  Proof. rewrite dbind_assoc //. Qed. 
+
   Lemma dbind_comm `{Countable B'} (f : A → B → distr B') (μ1 : distr A) (μ2 : distr B):
     (a ← μ1 ; b ← μ2; f a b) = (b ← μ2; a ← μ1; f a b).
   Proof.
@@ -723,94 +727,6 @@ Section probabilities.
 
 End probabilities.
 
-Section probability_prop.
-  Context `{Countable A}.
-
-  Lemma prob_dret_true (a : A) (P : A → bool) :
-    P a = true → prob (dret a) P = 1.
-  Proof.
-    intro HP.
-    rewrite /prob/pmf/=/dret_pmf/=.
-    erewrite SeriesC_ext; [apply SeriesC_singleton|].
-    real_solver.
-  Qed.
-
-  Lemma prob_dret_false (a : A) (P : A → bool) :
-    P a = false → prob (dret a) P = 0.
-  Proof.
-    intro HP.
-    rewrite /prob/pmf/=/dret_pmf/=.
-    apply SeriesC_0. real_solver.
-  Qed.
-
-  Lemma prob_dbind `{Countable B} (μ : distr A) (f : A → distr B) (P : B → bool) :
-    prob (dbind f μ) P = SeriesC (λ a, μ a * prob (f a) P).
-  Proof.
-    rewrite /prob{1}/pmf/=/dbind_pmf/=.
-    assert (∀ a,
-               (if P a then SeriesC (λ a0 : A, μ a0 * f a0 a) else 0) =
-               SeriesC (λ a0 : A, if P a then μ a0 * f a0 a else 0)) as Haux.
-    {intro a. destruct (P a); [done|]. rewrite SeriesC_0 //. }
-    setoid_rewrite Haux.
-    rewrite -(fubini_pos_seriesC (λ '(a, a0), if P a then μ a0 * f a0 a else 0)).
-    - apply SeriesC_ext=> a.
-      rewrite -SeriesC_scal_l.
-      apply SeriesC_ext; intro b.
-      real_solver.
-    - real_solver.
-    - intro b.
-      apply (ex_seriesC_le _ μ); [|done].
-      real_solver.
-    - apply (ex_seriesC_le _ (λ a : B, SeriesC (λ b : A, μ b * f b a))).
-      + intro b; split.
-        * apply SeriesC_ge_0'. real_solver.
-        * apply SeriesC_le; [real_solver|].
-          apply pmf_ex_seriesC_mult_fn.
-          exists 1. real_solver.
-      + apply (pmf_ex_seriesC (dbind f μ)).
-  Qed.
-
-  Lemma union_bound (μ : distr A) (P Q : A → bool) :
-    prob μ (λ a, andb (P a) (P a)) <= prob μ P + prob μ Q.
-  Proof.
-    rewrite /prob.
-    rewrite -SeriesC_plus.
-    - apply SeriesC_le.
-      + intro n.
-        pose proof (pmf_pos μ n).
-        destruct (P n); destruct (Q n); real_solver.
-      + apply (ex_seriesC_le _ (λ x, 2 * μ x)).
-        * intro n.
-          pose proof (pmf_pos μ n).
-          destruct (P n); destruct (Q n); real_solver.
-        * by apply ex_seriesC_scal_l.
-    - by apply ex_seriesC_filter_bool_pos.
-    - by apply ex_seriesC_filter_bool_pos.
-  Qed.
-
-End probability_prop.
-
-Section probabilities.
-  Context `{Countable A}.
-  Implicit Types μ d : distr A.
-
-  Definition prob (μ : distr A) (P : A → bool) : R :=
-    SeriesC (λ a : A, if (P a) then μ a else 0).
-
-  Lemma prob_le_1 (μ : distr A) (P : A → bool) :
-    prob μ P <= 1.
-  Proof.
-    transitivity (SeriesC μ); [|done].
-    apply SeriesC_le; [|done].
-    real_solver.
-  Qed.
-
-  Lemma prob_ge_0 (μ : distr A) (P : A → bool) :
-    0 <= prob μ P.
-  Proof. apply SeriesC_ge_0'=> a. real_solver. Qed.
-
-End probabilities.
-
 Section probability_lemmas.
   Context `{Countable A}.
 

theories/prob/markov.v

@@ -655,7 +655,7 @@ Section iter_markov.
       { rewrite /ϵ' /=. pose proof (cond_pos ϵ). nra. }
       edestruct (IHm ϵ') as [k2 Hk2]; [simpl; lra|].
       destruct (iter_markov_terminates_0_eps ϵ' a Ha) as [k1 Hk1].
-      exists (k1 + k2)%nat.
+      exists (S(k1 + k2)).
       eapply Rlt_le_trans; [apply H|].
       etrans; [|eapply iter_markov_plus_ge].
       assert (1 + ϵ' * ϵ' - 2 * ϵ' = (1 - ϵ') * (1 - ϵ')) as -> by lra.