fix after rebase

Author: affeldt-aist

theories/lang_syntax.v

@@ -151,7 +151,7 @@ move/left_right_continuousP.
 apply/not_andP; left.
 move/(@cvgrPdist_le _ R^o).
 apply/existsNP.
-exists (2%:R^-1)%R.
+exists 2%:R^-1%R.
 rewrite not_implyE; split; first by rewrite invr_gt0.
 move=> [e /= e0].
 move/(_ (-(e / 2))%R).
@@ -690,7 +690,7 @@ split.
   exact: exprn_continuous.
 Qed.
 
-Lemma derive_onemXn {R : realType} (n : nat) x :
+Lemma derive_onemXn {R : realType} n x :
   ((fun y : R => `1-y ^+ n.+1 : R^o)^`() x = - n.+1%:R * `1-x ^+ n)%R.
 Proof.
 rewrite (@derive1_comp _ (@onem R) (fun x => GRing.exp x n.+1))//; last first.
@@ -700,7 +700,8 @@ by rewrite -derive1E derive1_cst derive_id sub0r mulrN1 [in RHS]mulNr.
 Qed.
 
 Lemma integral_onemXn {R : realType} n :
-  fine (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (`1-x ^+ n)%:E) = n.+1%:R^-1%R :> R.
+  fine (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (`1-x ^+ n)%:E)
+  = (n.+1%:R^-1)%R :> R.
 Proof.
 rewrite (@continuous_FTC2 _ _ (fun x : R => ((1 - x) ^+ n.+1 / - n.+1%:R))%R)//=.
 - rewrite subrr subr0 expr0n/= mul0r expr1n mul1r sub0r.
@@ -723,7 +724,7 @@ exact: continuous_XMonemX.
 Qed.
 
 Lemma Rintegral_onemXn {R : realType} n :
-  (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (`1-x ^+ n))%R = n.+1%:R^-1%R :> R.
+  (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (`1-x ^+ n) = n.+1%:R^-1 :> R)%R.
 Proof.
 rewrite /Rintegral.
 rewrite (@continuous_FTC2 _ _ (fun x : R => ((1 - x) ^+ n.+1 / - n.+1%:R))%R)//=.
@@ -1991,8 +1992,8 @@ Inductive evalD : forall g t, exp D g t ->
 
 | eval_poisson g n (e : exp D g _) f mf :
   e -D> f ; mf ->
-  exp_poisson n e -D> poisson_pdf n \o f ;
-                      measurableT_comp (measurable_poisson_pdf n) mf
+  exp_poisson n e -D> poisson_pmf ^~ n \o f ;
+                      measurableT_comp (measurable_poisson_pmf n measurableT) mf
 
 | eval_normalize g t (e : exp P g t) k :
   e -P> k ->
@@ -2381,7 +2382,7 @@ all: rewrite {z g t}.
 - by eexists; eexists; exact: eval_uniform.
 - by eexists; eexists; exact: eval_beta.
 - move=> g h e [f [mf H]].
-  by exists (poisson_pdf h \o f); eexists; exact: eval_poisson.
+  by exists (poisson_pmf ^~ h \o f); eexists; exact: eval_poisson.
 - move=> g t e [k ek].
   by exists (normalize_pt k); eexists; exact: eval_normalize.
 - move=> g t1 t2 x e1 [k1 ev1] e2 [k2 ev2].
@@ -2579,8 +2580,9 @@ Proof. exact/execD_evalD/eval_normalize/evalP_execP. Qed.
 
 Lemma execD_poisson g n (e : exp D g Real) :
   execD (exp_poisson n e) =
-    existT _ (poisson_pdf n \o projT1 (execD e))
-             (measurableT_comp (measurable_poisson_pdf n) (projT2 (execD e))).
+    existT _ (poisson_pmf ^~ n \o projT1 (execD e))
+             (measurableT_comp (measurable_poisson_pmf n measurableT)
+                               (projT2 (execD e))).
 Proof. exact/execD_evalD/eval_poisson/evalD_execD. Qed.
 
 Lemma execP_if g st e1 e2 e3 :

theories/lang_syntax_examples.v

@@ -713,7 +713,8 @@ Let ite_3_10 : R.-sfker mbool * munit ~> measurableTypeR R :=
   ite macc0of2 (@ret _ _ _ (measurableTypeR R) R _ (kr 3)) (@ret _ _ _ (measurableTypeR R) R _ (kr 10)).
 
 Let score_poisson4 : R.-sfker measurableTypeR R * (mbool * munit) ~> munit :=
-  score (measurableT_comp (measurable_poisson_pdf 4) (@macc0of2 _ _ (measurableTypeR R) _)).
+  score (measurableT_comp (measurable_poisson_pmf 4 measurableT)
+                          (@macc0of2 _ _ (measurableTypeR R) _)).
 
 Let kstaton_bus' :=
   letin' sample_bern
@@ -755,7 +756,7 @@ Lemma exec_staton_bus : execD staton_bus_syntax =
   existT _ (normalize_pt kstaton_bus') (measurable_normalize_pt _).
 Proof. by rewrite execD_normalize_pt exec_staton_bus0'. Qed.
 
-Let poisson4 := @poisson_pdf R 4%N.
+Let poisson4 := @poisson_pmf R ^~ 4%N.
 
 Let staton_bus_probability U :=
   ((2 / 7)%:E * (poisson4 3)%:E * \d_true U +
@@ -773,13 +774,13 @@ rewrite -!muleA; congr (_ * _ + _ * _)%E.
   rewrite letin'_retk//.
   rewrite letin'_kret//.
   rewrite /score_poisson4.
-  by rewrite /score/= /mscale/= ger0_norm//= poisson_pdf_ge0.
+  by rewrite /score/= /mscale/= ger0_norm//= poisson_pmf_ge0.
 - by rewrite onem27.
 - rewrite letin'_iteF//.
   rewrite letin'_retk//.
   rewrite letin'_kret//.
   rewrite /score_poisson4.
-  by rewrite /score/= /mscale/= ger0_norm//= poisson_pdf_ge0.
+  by rewrite /score/= /mscale/= ger0_norm//= poisson_pmf_ge0.
 Qed.
 
 End staton_bus.
@@ -808,7 +809,8 @@ Let ite_3_10 : R.-sfker mbool * munit ~> measurableTypeR R :=
   ite macc0of2 (@ret _ _ _ (measurableTypeR R) R _ (kr 3)) (@ret _ _ _ (measurableTypeR R) R _ (kr 10)).
 
 Let score_poisson4 : R.-sfker measurableTypeR R * (mbool * munit) ~> munit :=
-  score (measurableT_comp (measurable_poisson_pdf 4) (@macc0of3' _ _ _ (measurableTypeR R) _ _)).
+  score (measurableT_comp (measurable_poisson_pmf 4 measurableT)
+                          (@macc0of3' _ _ _ (measurableTypeR R) _ _)).
 
 (* same as kstaton_bus _ (measurable_poisson 4) but expressed with letin'
    instead of letin *)
@@ -884,7 +886,7 @@ rewrite execP_return exp_var'E/= (execD_var_erefl "x") //=.
 by apply/eq_sfkernel => /= -[[] [a [b []]]] U0.
 Qed.
 
-Let poisson4 := @poisson_pdf R 4%N.
+Let poisson4 := @poisson_pmf R ^~ 4%N.
 
 Lemma exec_staton_busA0 U : execP staton_busA_syntax0 tt U =
   ((2 / 7%:R)%:E * (poisson4 3%:R)%:E * \d_true U +

theories/prob_lang.v

@@ -18,8 +18,6 @@ From mathcomp Require Import lebesgue_integral trigo probability kernel charge.
 (*   ESOP 2017                                                                *)
 (*                                                                            *)
 (* ```                                                                        *)
-(*          poisson_pdf == Poisson pdf                                        *)
-(*      exponential_pdf == exponential distribution pdf                       *)
 (*   measurable_sum X Y == the type X + Y, as a measurable type               *)
 (* ```                                                                        *)
 (*                                                                            *)
@@ -113,61 +111,26 @@ subst p2.
 by f_equal.
 Qed.
 
-(* NB: to be PRed to probability.v *)
-Section poisson_pdf.
-Variable R : realType.
-Local Open Scope ring_scope.
-
-(* density function for Poisson *)
-Definition poisson_pdf k r : R :=
-  if r > 0 then r ^+ k / k`!%:R^-1 * expR (- r) else 1%:R.
-
-Lemma poisson_pdf_ge0 k r : 0 <= poisson_pdf k r.
-Proof.
-rewrite /poisson_pdf; case: ifPn => r0//.
-by rewrite mulr_ge0 ?expR_ge0// mulr_ge0// exprn_ge0 ?ltW.
-Qed.
+Definition poisson3 {R : realType} := @poisson_pmf R 3%:R 4. (* 0.168 *)
+Definition poisson10 {R : realType} := @poisson_pmf R 10%:R 4. (* 0.019 *)
 
-Lemma poisson_pdf_gt0 k r : 0 < r -> 0 < poisson_pdf k.+1 r.
+(* TODO: move *)
+Lemma poisson_pmf_gt0 {R : realType} k (r : R) :
+  (0 < r -> 0 < poisson_pmf r k.+1)%R.
 Proof.
-move=> r0; rewrite /poisson_pdf r0 mulr_gt0  ?expR_gt0//.
+move=> r0; rewrite /poisson_pmf r0 mulr_gt0  ?expR_gt0//.
 by rewrite divr_gt0// ?exprn_gt0// invr_gt0 ltr0n fact_gt0.
 Qed.
 
-Lemma measurable_poisson_pdf k : measurable_fun setT (poisson_pdf k).
-Proof.
-rewrite /poisson_pdf; apply: measurable_fun_if => //.
-  exact: measurable_fun_ltr.
-by apply: measurable_funM => /=;
-  [exact: measurable_funM|exact: measurableT_comp].
-Qed.
-
-Definition poisson3 := poisson_pdf 4 3%:R. (* 0.168 *)
-Definition poisson10 := poisson_pdf 4 10%:R. (* 0.019 *)
-
-End poisson_pdf.
-
-Section exponential_pdf.
-Variable R : realType.
-Local Open Scope ring_scope.
-
-(* density function for exponential *)
-Definition exponential_pdf x r : R := r * expR (- r * x).
-
-Lemma exponential_pdf_gt0 x r : 0 < r -> 0 < exponential_pdf x r.
-Proof. by move=> r0; rewrite /exponential_pdf mulr_gt0// expR_gt0. Qed.
-
-Lemma exponential_pdf_ge0 x r : 0 <= r -> 0 <= exponential_pdf x r.
-Proof. by move=> r0; rewrite /exponential_pdf mulr_ge0// expR_ge0. Qed.
-
-Lemma measurable_exponential_pdf x : measurable_fun setT (exponential_pdf x).
+Lemma exponential_pdf_gt0 {R : realType} (r : R) x :
+  (0 < r -> 0 < x -> 0 < exponential_pdf r x)%R.
 Proof.
-apply: measurable_funM => //=; apply: measurableT_comp => //.
-exact: measurable_funM.
+move=> r0 x0; rewrite /exponential_pdf/=.
+rewrite patchE/= ifT; last first.
+  by rewrite inE/= in_itv/= (ltW x0).
+by rewrite mulr_gt0// expR_gt0.
 Qed.
 
-End exponential_pdf.
-
 (* X + Y is a measurableType if X and Y are *)
 HB.instance Definition _ (X Y : pointedType) :=
   isPointed.Build (X + Y)%type (@inl X Y point).
@@ -1704,8 +1667,8 @@ End staton_bus.
 Section staton_bus_poisson.
 Import Notations.
 Context d (T : measurableType d) (R : realType).
-Let poisson4 := @poisson_pdf R 4%N.
-Let mpoisson4 := @measurable_poisson_pdf R 4%N.
+Let poisson4 r := @poisson_pmf R r 4%N.
+Let mpoisson4 := @measurable_poisson_pmf R setT 4%N measurableT.
 
 Definition kstaton_bus_poisson : R.-sfker R ~> mbool :=
   kstaton_bus _ mpoisson4.
@@ -1720,12 +1683,12 @@ rewrite -!muleA; congr (_ * _ + _ * _).
 - rewrite letin_kret//.
   rewrite letin_iteT//.
   rewrite letin_retk//.
-  by rewrite scoreE//= => r r0; exact: poisson_pdf_ge0.
+  by rewrite scoreE//= => r r0; exact: poisson_pmf_ge0.
 - by rewrite onem27.
   rewrite letin_kret//.
   rewrite letin_iteF//.
   rewrite letin_retk//.
-  by rewrite scoreE//= => r r0; exact: poisson_pdf_ge0.
+  by rewrite scoreE//= => r r0; exact: poisson_pmf_ge0.
 Qed.
 
 (* true -> 2/7 * 0.168 = 2/7 * 3^4 e^-3 / 4! *)
@@ -1740,7 +1703,7 @@ Lemma staton_busE P (t : R) U :
 Proof.
 rewrite /staton_bus normalizeE !kstaton_bus_poissonE !diracT !mule1 ifF //.
 apply/negbTE; rewrite gt_eqF// lte_fin.
-by rewrite addr_gt0// mulr_gt0//= ?divr_gt0// ?ltr0n// poisson_pdf_gt0// ltr0n.
+by rewrite addr_gt0// mulr_gt0//= ?divr_gt0// ?ltr0n// poisson_pmf_gt0// ltr0n.
 Qed.
 
 End staton_bus_poisson.
@@ -1770,12 +1733,14 @@ rewrite -!muleA; congr (_ * _ + _ * _).
 - rewrite letin_kret//.
   rewrite letin_iteT//.
   rewrite letin_retk//.
-  rewrite scoreE//= => r r0; exact: exponential_pdf_ge0.
+  rewrite scoreE//= => r r0; apply: exponential_pdf_ge0 => //.
+  by rewrite ler0q; lra.
 - by rewrite onem27.
   rewrite letin_kret//.
   rewrite letin_iteF//.
   rewrite letin_retk//.
-  by rewrite scoreE//= => r r0; exact: exponential_pdf_ge0.
+  rewrite scoreE//= => r r0; apply: exponential_pdf_ge0.
+  by rewrite ler0q; lra.
 Qed.
 
 (* true -> 5/7 * 0.019 = 5/7 * 10^4 e^-10 / 4! *)
@@ -1791,12 +1756,12 @@ Proof.
 rewrite /staton_bus.
 rewrite normalizeE /= !kstaton_bus_exponentialE !diracT !mule1 ifF //.
 apply/negbTE; rewrite gt_eqF// lte_fin.
-by rewrite addr_gt0// mulr_gt0//= ?divr_gt0// ?ltr0n// exponential_pdf_gt0 ?ltr0n.
+by rewrite addr_gt0// mulr_gt0//= ?divr_gt0// ?ltr0n//;
+  rewrite exponential_pdf_gt0 ?ltr0n// ltr0q; lra.
 Qed.
 
 End staton_bus_exponential.
 
-
 Section von_neumann_trick.
 Context d {T : measurableType d} {R : realType}.
 

theories/prob_lang_wip.v

@@ -28,27 +28,27 @@ Variable R : realType.
 Local Open Scope ring_scope.
 Notation mu := (@lebesgue_measure R).
 Hypothesis integral_poisson_density : forall k,
-  (\int[mu]_x (@poisson_pdf R k x)%:E = 1%E)%E.
+  (\int[mu]_x (@poisson_pmf R x k)%:E = 1%E)%E.
 
 (* density function for poisson *)
-Definition poisson1 := @poisson_pdf R 1%N.
+Definition poisson1 r := @poisson_pmf R r 1%N.
 
 Lemma poisson1_ge0 (x : R) : 0 <= poisson1 x.
-Proof. exact: poisson_pdf_ge0. Qed.
+Proof. exact: poisson_pmf_ge0. Qed.
 
 Definition mpoisson1 (V : set R) : \bar R :=
   (\int[lebesgue_measure]_(x in V) (poisson1 x)%:E)%E.
 
 Lemma measurable_fun_poisson1 : measurable_fun setT poisson1.
-Proof. exact: measurable_poisson_pdf. Qed.
+Proof. exact: measurable_poisson_pmf. Qed.
 
 Let mpoisson10 : mpoisson1 set0 = 0%E.
 Proof. by rewrite /mpoisson1 integral_set0. Qed.
 
 Lemma mpoisson1_ge0 A : (0 <= mpoisson1 A)%E.
 Proof.
 apply: integral_ge0 => x Ax.
-by rewrite lee_fin poisson1_ge0.
+rewrite lee_fin poisson1_ge0//.
 Qed.
 
 Let mpoisson1_sigma_additive : semi_sigma_additive mpoisson1.
@@ -57,12 +57,12 @@ move=> /= F mF tF mUF.
 rewrite /mpoisson1/= integral_bigcup//=; last first.
   apply/integrableP; split.
     apply/measurable_EFinP.
-    exact: measurable_funS (measurable_poisson_pdf _).
+    exact: measurable_funS (measurable_poisson_pmf _ measurableT).
   rewrite (_ : (fun x => _) = (EFin \o poisson1)); last first.
     by apply/funext => x; rewrite gee0_abs// lee_fin poisson1_ge0//.
   apply: le_lt_trans.
     apply: (@ge0_subset_integral _ _ _ _ _ setT) => //=.
-      by apply/measurable_EFinP; exact: measurable_poisson_pdf.
+      by apply/measurable_EFinP; exact: measurable_poisson_pmf.
     by move=> ? _; rewrite lee_fin poisson1_ge0//.
   by rewrite /= integral_poisson_density// ltry.
 apply: is_cvg_ereal_nneg_natsum_cond => n _ _.
@@ -90,19 +90,19 @@ Variable R : realType.
 Notation mu := (@lebesgue_measure R).
 Import Notations.
 Hypothesis integral_poisson_density : forall k,
-  (\int[mu]_x (@poisson_pdf R k x)%:E = 1%E)%E.
+  (\int[mu]_x (@poisson_pmf R x k)%:E = 1%E)%E.
 
-Let f1 x := ((poisson1 (x : R)) ^-1)%R.
+Let f1 x := ((poisson1 (x : R))^-1)%R.
 
 Let mf1 : measurable_fun setT f1.
-rewrite /f1 /poisson1 /poisson_pdf.
+rewrite /f1 /poisson1 /poisson_pmf.
 apply: (measurable_comp (F := [set r : R | r != 0%R])) => //.
 - exact: open_measurable.
 - move=> /= r [t ? <-].
   by case: ifPn => // t0; rewrite gt_eqF ?mulr_gt0 ?expR_gt0//= invrK ltr0n.
 - apply: open_continuous_measurable_fun => //.
   by apply/in_setP => x /= x0; exact: inv_continuous.
-- exact: measurable_poisson_pdf.
+- exact: measurable_poisson_pmf.
 Qed.
 
 Definition staton_counting : R.-sfker X ~> _ :=