cleaning/rebase

coq-mathcomp-analysis.opam

@@ -23,8 +23,8 @@ depends: [
   "coq-mathcomp-solvable" { (>= "2.0.0") | (= "dev") }
   "coq-mathcomp-field"
   "coq-mathcomp-bigenough" { (>= "1.0.0") }
-  "coq-mathcomp-algebra-tactics" { (>= "1.2.0") }
-  "coq-mathcomp-zify" { (>= "1.4.0") }
+  "coq-mathcomp-algebra-tactics" { (>= "1.2.3") }
+  "coq-mathcomp-zify" { (>= "1.5.0") }
 ]
 
 tags: [

theories/kernel.v

@@ -765,8 +765,6 @@ HB.instance Definition _ (P : probability Y R):=
 
 End knormalize.
 
-<<<<<<< HEAD
-(* TODO: useful? *)
 Lemma measurable_fun_mnormalize d d' (X : measurableType d)
     (Y : measurableType d') (R : realType) (k : R.-ker X ~> Y) :
   measurable_fun [set: X] (fun x =>
@@ -797,8 +795,6 @@ apply: measurable_fun_if => //.
   + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel.
 Qed.
 
-=======
->>>>>>> ea7f1064 (rm duplicate, more uniform naming)
 Section kcomp_def.
 Context d1 d2 d3 (X : measurableType d1) (Y : measurableType d2)
   (Z : measurableType d3) (R : realType).

theories/lang_syntax.v

@@ -6,7 +6,7 @@ From mathcomp Require Import functions cardinality fsbigop.
 Require Import signed reals ereal topology normedtype sequences esum exp.
 Require Import measure lebesgue_measure numfun lebesgue_integral itv kernel.
 Require Import charge prob_lang lang_syntax_util.
-From mathcomp Require Import ring lra.
+From mathcomp Require Import lra.
 
 (**md**************************************************************************)
 (* # Syntax and Evaluation for a Probabilistic Programming Language           *)
@@ -168,10 +168,10 @@ rewrite /ubeta_nat_pdf /=; apply: measurable_fun_if => //=; last first.
   by rewrite setTI; apply: measurable_funTS; exact: measurable_fun_expn_onem.
 apply: measurable_and => /=.
   apply: (measurable_fun_bool true).
-  rewrite [X in measurable X](_ : _ = `[0, +oo[%classic)//.
+  rewrite setTI [X in measurable X](_ : _ = `[0, +oo[%classic)//.
   by rewrite set_interval.set_itv_c_infty.
 apply: (measurable_fun_bool true).
-by rewrite [X in measurable X](_ : _ = `]-oo, 1]%classic)//.
+by rewrite setTI [X in measurable X](_ : _ = `]-oo, 1]%classic)//.
 Qed.
 
 Local Notation mu := lebesgue_measure.
@@ -696,21 +696,20 @@ move=> /andP[x0 x1]; rewrite ler_norml; apply/andP; split.
 by rewrite lerBlDr lerDl.
 Qed.
 
-Lemma beta_nat_bernE a' b' U : (a > 0)%N -> (b > 0)%N ->
+Lemma beta_nat_bernoulliE a' b' U : (a > 0)%N -> (b > 0)%N ->
   beta_nat_bernoulli a' b' U = bernoulli (div_beta_nat_norm a' b') U.
 Proof.
 move=> a0 b0.
 rewrite /beta_nat_bernoulli.
 under eq_integral => x.
   rewrite inE/= in_itv/= => x01.
-  rewrite bernoulliE_ext/= ?ubeta_nat_pdf_ge0 ?ubeta_nat_pdf_le1//.
+  rewrite bernoulliE/= ?ubeta_nat_pdf_ge0 ?ubeta_nat_pdf_le1//.
   over.
 rewrite /=.
-rewrite [in RHS]bernoulliE_ext/= ?div_beta_nat_norm_ge0 ?div_beta_nat_norm_le1//=.
+rewrite [in RHS]bernoulliE/= ?div_beta_nat_norm_ge0 ?div_beta_nat_norm_le1//=.
 under eq_integral => x x01.
-  rewrite /ubeta_nat_pdf.
   rewrite inE /=in_itv/= in x01.
-  rewrite x01.
+  rewrite /ubeta_nat_pdf x01.
   over.
 rewrite /=.
 rewrite integralD//=; last 2 first.
@@ -785,7 +784,8 @@ rewrite integralZl//=; last first.
       by rewrite mulr_ile1// ?exprn_ge0 ?exprn_ile1// ?onem_ge0 ?onem_le1//; case/andP: t01.
   - exact: integrableS (integrable_ubeta_nat_pdf _ _).
 transitivity (((beta_nat_norm a b)^-1)%:E *
-    \int[mu]_(x in `[0%R, 1%R]) ((ubeta_nat_pdf a b x)%:E - (ubeta_nat_pdf (a+a') (b+b') x)%:E) : \bar R)%E.
+    \int[mu]_(x in `[0%R, 1%R]) ((ubeta_nat_pdf a b x)%:E -
+                                 (ubeta_nat_pdf (a + a') (b + b') x)%:E) : \bar R)%E.
   congr (_ * _)%E.
   apply: eq_integral => x x01.
   rewrite /onem -EFinM mulrBl mul1r EFinB.
@@ -1280,7 +1280,7 @@ Inductive evalD : forall g t, exp D g t ->
 
 | eval_binomial g n e r mr :
   e -D> r ; mr -> (exp_binomial n e : exp D g _) -D> binomial_prob n \o r ;
-                   measurableT_comp (measurable_binomial_probT n) mr
+                   measurableT_comp (measurable_binomial_prob n) mr
 
 | eval_uniform g (a b : R) (ab : (a < b)%R) :
   (exp_uniform a b ab : exp D g _) -D> cst (uniform_prob ab) ;
@@ -1858,7 +1858,7 @@ Proof. exact/execD_evalD/eval_bernoulli/evalD_execD. Qed.
 Lemma execD_binomial g n e :
   @execD g _ (exp_binomial n e) =
     existT _ ((binomial_prob n : R -> pprobability nat R) \o projT1 (execD e))
-             (measurableT_comp (measurable_binomial_probT n) (projT2 (execD e))).
+             (measurableT_comp (measurable_binomial_prob n) (projT2 (execD e))).
 Proof. exact/execD_evalD/eval_binomial/evalD_execD. Qed.
 
 Lemma execD_uniform g a b ab0 :
@@ -1926,10 +1926,13 @@ Lemma congr_letinl {R : realType} g t1 t2 str (e1 e2 : @exp _ _ g t1)
   @execP R g t2 [let str := e2 in e] x U.
 Proof. by move=> + mU; move/eq_sfkernel => He; rewrite !execP_letin He. Qed.
 
-Lemma congr_letinr {R : realType} g t1 t2 str (e : @exp _ _ _ t1) (e1 e2 : @exp _ _ (_ :: g) t2) x U :
+Lemma congr_letinr {R : realType} g t1 t2 str (e : @exp _ _ _ t1)
+  (e1 e2 : @exp _ _ (_ :: g) t2) x U :
   (forall y V, execP e1 (y, x) V = execP e2 (y, x) V) ->
   @execP R g t2 [let str := e in e1] x U = @execP R g t2 [let str := e in e2] x U.
-Proof. by move=> He; rewrite !execP_letin !letin'E; apply: eq_integral => ? _; exact: He. Qed.
+Proof.
+by move=> He; rewrite !execP_letin !letin'E; apply: eq_integral => ? _; exact: He.
+Qed.
 
 Lemma congr_normalize {R : realType} g t (e1 e2 : @exp R _ g t) :
   (forall x U, execP e1 x U = execP e2 x U) ->

theories/lang_syntax_examples.v

@@ -69,6 +69,7 @@ Local Close Scope lang_scope.
 Module bidi_tests.
 Local Open Scope lang_scope.
 Import Notations.
+Section bidi_tests.
 Context (R : realType).
 
 Definition bidi_test1 x : @exp R P [::] _ := [
@@ -106,6 +107,7 @@ Definition bidi_test4 (a b c d : string)
   return {exp_poisson O [#c(*{exp_var c erefl}*)]}].
 
 End bidi_tests.
+End bidi_tests.
 
 Section trivial_example.
 Local Open Scope lang_scope.
@@ -277,7 +279,7 @@ rewrite ger0_norm//.
 rewrite !integral_dirac//= !diracT !mul1e ger0_norm//.
 rewrite exp_var'E (execD_var_erefl "x")/=.
 rewrite !indicT/= !mulr1.
-rewrite bernoulliE_ext//=; last lra.
+rewrite bernoulliE//=; last lra.
 by rewrite muleDl//; congr (_ + _)%E;
   rewrite -!EFinM; congr (_%:E);
   rewrite !indicE /onem /=; case: (_ \in _); field.
@@ -317,7 +319,7 @@ rewrite !ge0_integral_mscale//=.
 rewrite ger0_norm//.
 rewrite !integral_dirac//= !diracT !mul1e ger0_norm//.
 rewrite exp_var'E (execD_var_erefl "x")/=.
-rewrite bernoulliE_ext//=; last lra.
+rewrite bernoulliE//=; last lra.
 rewrite !mul1r.
 rewrite muleDl//; congr (_ + _)%E;
   rewrite -!EFinM;
@@ -361,7 +363,7 @@ rewrite !letin'E/= !iteE/=.
 rewrite !ge0_integral_mscale//=.
 rewrite ger0_norm//.
 rewrite !integral_dirac//= !diracT !mul1e ger0_norm//.
-rewrite bernoulliE_ext//=; last lra.
+rewrite bernoulliE//=; last lra.
 rewrite muleDl//; congr (_ + _)%E;
   rewrite -!EFinM;
   congr (_%:E);
@@ -648,7 +650,7 @@ transitivity (beta_nat_bernoulli 6 4 1 0 U : \bar R).
     by rewrite expr0 expr1 mulr1.
   rewrite !mul0r !mule0.
   by case: ifPn.
-rewrite beta_nat_bernE// !bernoulliE_ext//=; last 2 first.
+rewrite beta_nat_bernoulliE// !bernoulliE//=; last 2 first.
   lra.
   by rewrite div_beta_nat_norm_ge0 div_beta_nat_norm_le1.
 congr (_ * _ + _ * _)%:E.

theories/lang_syntax_table_game.v

@@ -9,7 +9,7 @@ Require Import prob_lang lang_syntax_util lang_syntax lang_syntax_examples.
 From mathcomp Require Import ring lra.
 
 (**md**************************************************************************)
-(* # Edd's table game example                                                 *)
+(* # Eddy's table game example                                                *)
 (*                                                                            *)
 (* ref:                                                                       *)
 (* - Chung-chieh Shan, Equational reasoning for probabilistic programming,    *)
@@ -185,7 +185,7 @@ apply: (@le_lt_trans _ _ (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (beta_nat_pd
     by apply/EFin_measurable_fun; exact: measurable_beta_nat_pdf.
   - move=> x _ /=; rewrite patchE; case: ifPn => // _.
     by rewrite lee_fin beta_nat_pdf_ge0.
-  - apply: (measurable_restrict (E := setT) _ _ _ _).1 => //.
+  - apply/(measurable_restrict _ _ _) => //.
     apply/measurable_funTS/measurableT_comp => //.
     exact: measurable_beta_nat_pdf.
   - move=> x _.
@@ -276,7 +276,7 @@ rewrite (@execD_bin _ _ binop_minus) !execD_real/= !execD_nat.
 rewrite !exp_var'E !(execD_var_erefl "p") !(execD_var_erefl "a2")/=.
 rewrite !letin'E/=.
 move: r01 => /andP[r0 r1].
-by apply/integral_binomial_bernoulli/andP.
+by apply/integral_binomial_prob/andP.
 Qed.
 
 Lemma casino12 : execD casino1 = execD casino2.
@@ -443,7 +443,7 @@ transitivity (\int[beta_nat 6 4]_(y in `[0%R, 1%R]%classic : set R)
   rewrite patchE; case: ifPn => //.
   rewrite /beta_nat_pdf /ubeta_nat_pdf notin_setE/= in_itv/= => /negP/negbTE ->.
   by rewrite mul0r mule0.
-have := (@beta_nat_bernE R 6 4 0 3 U) isT isT.
+have := (@beta_nat_bernoulliE R 6 4 0 3 U) isT isT.
 rewrite /beta_nat_bernoulli /ubeta_nat_pdf /=.
 under eq_integral.
   move=> x.
@@ -468,7 +468,7 @@ have f1 x : x \in (`[0%R, 1%R]%classic : set R) -> (f x <= 1)%R.
   by move => /f01/andP[].
 under eq_integral => x.
   move=> x01.
-  rewrite bernoulliE_ext//=; last first.
+  rewrite bernoulliE//=; last first.
     by rewrite subr_ge0 f1//= lerBlDr addrC -lerBlDr subrr f0.
   over.
 rewrite /=.
@@ -501,8 +501,7 @@ rewrite [X in _ + X = _]ge0_integralZr//=; last 2 first.
   by apply/EFin_measurable_fun; exact: measurable_beta_nat_pdf.
   by move=> x x01; rewrite mule_ge0// lee_fin// ?f0// ?inE// beta_nat_pdf_ge0.
 under [in RHS]eq_integral => x x01.
-  rewrite bernoulliE_ext//=; last first.
-    by rewrite f0//= f1.
+  rewrite bernoulliE//=; last by rewrite f0//= f1.
   rewrite muleDl//.
   over.
 rewrite /= ge0_integralD//=; last 4 first.
@@ -653,7 +652,7 @@ rewrite (@execD_bin _ _ binop_minus) execD_pow/= (@execD_bin _ _ binop_minus).
 rewrite !execD_real/= exp_var'E (execD_var_erefl "p")/=.
 transitivity (\int[beta_nat 6 4]_y bernoulli (1 - (1 - y) ^+ 3) U : \bar R)%E.
   by rewrite /beta_nat_bernoulli !letin'E/= /onem.
-rewrite bernoulliE_ext//=; last lra.
+rewrite bernoulliE//=; last lra.
 rewrite integral_beta_nat//; last first.
   by have := @integral_beta_bernoulli_onem_lty R _ _ _ U.
   apply: (measurableT_comp (measurable_bernoulli2 _)) => //.
@@ -678,28 +677,17 @@ rewrite (@integral_bernoulli_beta_nat_pdf (fun x => (1 - x) ^+ 3)%R U (1 / 11))/
     rewrite [RHS]integral_beta_nat//; last 2 first.
       apply: (measurableT_comp (measurable_bernoulli2 _)) => //.
       apply: measurable_fun_if => //.
-        apply: measurable_and => //.
-          apply: (measurable_fun_bool true) => //=.
-          rewrite (_ : _ @^-1` _ = `[0%R, +oo[%classic)//.
-          by apply/seteqP; split => [z|z] /=; rewrite in_itv/= andbT.
-        apply: (measurable_fun_bool true) => //=.
-        by rewrite (_ : _ @^-1` _ = `]-oo, 1%R]%classic).
+        by apply: measurable_and => //; exact: measurable_fun_ler.
       apply: measurable_funTS; apply: measurable_funM => //.
-      apply: measurable_fun_pow => //.
-      by apply: measurable_funB => //.
+      by apply: measurable_fun_pow => //; exact: measurable_funB.
     rewrite (le_lt_trans _ (integral_beta_bernoulli_expn_lty 3 6 4 U))//.
     rewrite integral_mkcond /=; apply: ge0_le_integral => //=.
       by move=> z _; rewrite patchE expr0 mul1r; case: ifPn.
-      apply: (measurable_restrict _ _ _ _).1 => //.
+      apply/(measurable_restrict _ _ _) => //.
       apply: measurable_funTS; apply: measurableT_comp => //=.
       apply: (measurableT_comp (measurable_bernoulli2 _)) => //=.
       apply: measurable_fun_if => //=.
-        apply: measurable_and => //.
-        apply: (measurable_fun_bool true) => //=.
-          rewrite (_ : _ @^-1` _ = `[0%R, +oo[%classic)//.
-          by apply/seteqP; split => [z|z] /=; rewrite in_itv/= andbT.
-        apply: (measurable_fun_bool true) => //=.
-        by rewrite (_ : _ @^-1` _ = `]-oo, 1%R]%classic).
+        by apply: measurable_and => //; exact: measurable_fun_ler.
       apply: measurable_funTS; apply: measurable_funM => //.
       by apply: measurable_fun_pow => //; exact: measurable_funB.
       by apply/measurableT_comp => //; exact: measurable_bernoulli_expn.
@@ -709,7 +697,7 @@ rewrite (@integral_bernoulli_beta_nat_pdf (fun x => (1 - x) ^+ 3)%R U (1 / 11))/
     apply: eq_integral => z z01.
     rewrite inE/= in_itv/= in z01.
     by rewrite z01 expr0 mul1r.
-  rewrite beta_nat_bernE//= bernoulliE_ext//=; last first.
+  rewrite beta_nat_bernoulliE//= bernoulliE//=; last first.
     by rewrite div_beta_nat_norm_ge0// div_beta_nat_norm_le1.
   rewrite probability_setT.
   by congr (_ * _ + _ * _)%:E; rewrite /onem;
@@ -730,20 +718,20 @@ rewrite !execP_sample !execD_bernoulli !execD_real/=.
 apply: funext=> x.
 apply: eq_probability=> /= y.
 rewrite !normalizeE/=.
-rewrite !bernoulliE_ext//=; [|lra..].
+rewrite !bernoulliE//=; [|lra..].
 rewrite !diracT !mule1 -EFinD add_onemK onee_eq0/=.
 rewrite !letin'E.
 under eq_integral.
   move=> x0 _ /=.
-  rewrite !bernoulliE_ext//=; [|lra..].
+  rewrite !bernoulliE//=; [|lra..].
   rewrite !diracT !mule1 -EFinD add_onemK.
   over.
 rewrite !ge0_integral_mscale//= (ger0_norm (ltW p0))//.
 rewrite integral_dirac// !diracT !indicT /= !mule1.
 rewrite gt_eqF ?lte_fin//=.
 rewrite integral_dirac//= diracT !mul1e !mulr1.
 rewrite addrCA subrr addr0 invr1 mule1.
-rewrite !bernoulliE_ext//=; [|lra..].
+rewrite !bernoulliE//=; [|lra..].
 by rewrite muleAC -EFinM divff// ?gt_eqF// mul1r EFinD.
 Qed.
 

theories/lebesgue_measure.v

@@ -1728,7 +1728,7 @@ Lemma measurable_fun_pow D f n : measurable_fun D f ->
   measurable_fun D (fun x => f x ^+ n).
 Proof.
 move=> mf.
-apply: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f) => //.
+exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f).
 Qed.
 
 Lemma measurable_fun_ltr D f g : measurable_fun D f -> measurable_fun D g ->
@@ -1747,20 +1747,6 @@ under eq_fun do rewrite -subr_ge0.
 by rewrite preimage_true -preimage_itv_c_infty; exact: measurable_funB.
 Qed.
 
-Lemma measurable_fun_ler D f g : measurable_fun D f -> measurable_fun D g ->
-  measurable_fun D (fun x => f x <= g x).
-Proof.
-move=> mf mg mD Y mY; have [| | |] := set_bool Y => /eqP ->.
-- under eq_fun do rewrite -subr_ge0.
-  rewrite preimage_true -preimage_itv_c_infty.
-  by apply: (measurable_funB mg mf) => //; exact: measurable_itv.
-- under eq_fun do rewrite leNgt -subr_gt0.
-  rewrite preimage_false set_predC setCK -preimage_itv_o_infty.
-  by apply: (measurable_funB mf mg) => //; exact: measurable_itv.
-- by rewrite preimage_set0 setI0.
-- by rewrite preimage_setT setIT.
-Qed.
-
 (* setT should be D? (derived from measurable_and) *)
 Lemma measurable_fun_eqr D f g : measurable_fun D f -> measurable_fun D g ->
   measurable_fun D (fun x => f x == g x).
@@ -1876,7 +1862,7 @@ have [Y0|Y0] := boolP (0%E \in Y).
     rewrite [X in _ -> X](_ : _ = Y (\d_r U)) //.
     rewrite diracE.
     move/mem_set.
-    case (_ \in _) => //= _.
+    case: (_ \in _) => //= _.
     by rewrite inE in Y1.
   + rewrite [X in measurable X](_ : _ = set0).
       exact: measurable0.
@@ -1922,13 +1908,6 @@ under eq_fun do rewrite -mulr_natr.
 by do 2 apply: measurable_funM => //.
 Qed.
 
-Lemma measurable_fun_pow {R : realType} D (f : R -> R) n : measurable_fun D f ->
-  measurable_fun D (fun x => f x ^+ n).
-Proof.
-move=> mf.
-exact: (@measurable_comp _ _ _ _ _ _ setT (fun x : R => x ^+ n) _ f).
-Qed.
-
 Lemma measurable_powR (R : realType) p :
   measurable_fun [set: R] (@powR R ^~ p).
 Proof.

theories/measure.v

@@ -1682,6 +1682,21 @@ rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `&`
 by apply: measurableI; [exact: mf|exact: mg].
 Qed.
 
+Lemma measurable_or D (f : T1 -> bool) (g : T1 -> bool) :
+  measurable_fun D f -> measurable_fun D g ->
+  measurable_fun D (fun x => f x || g x).
+Proof.
+move=> mf mg mD; apply: (measurable_fun_bool true) => //.
+rewrite [X in measurable X](_ : _ = D `&` f @^-1` [set true] `|`
+                                    (D `&` g @^-1` [set true])); last first.
+  apply/seteqP; split=> [x [Dx/= /orP[]->]|x [|]/=].
+  by left.
+  by right.
+  by move=> [Dx ->]; split.
+  by move=> [Dx ->]; split => //; apply/orP; right.
+by apply: measurableU; [exact: mf|exact: mg].
+Qed.
+
 End measurable_fun_measurableType.
 #[global] Hint Extern 0 (measurable_fun _ (fun=> _)) =>
   solve [apply: measurable_cst] : core.