minor fixes

Author: affeldt-aist

theories/lang_syntax_examples.v

@@ -209,11 +209,11 @@ Definition sample_pair_syntax : exp _ [::] _ :=
 Lemma exec_sample_pair0 (A : set (bool * bool)) :
   @execP R [::] _ sample_pair_syntax0 tt A =
   ((1 / 2)%:E *
-   ((1 / 3)%:E * ((true, true) \in A)%:R%:E +
-    (1 - 1 / 3)%:E * ((true, false) \in A)%:R%:E) +
+   ((1 / 3)%:E * \d_(true, true) A +
+    (1 - 1 / 3)%:E * \d_(true, false) A) +
    (1 - 1 / 2)%:E *
-   ((1 / 3)%:E * ((false, true) \in A)%:R%:E +
-    (1 - 1 / 3)%:E * ((false, false) \in A)%:R%:E))%E.
+   ((1 / 3)%:E * \d_(false, true) A +
+    (1 - 1 / 3)%:E * \d_(false, false) A))%E.
 Proof.
 rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=.
 rewrite execD_pair !exp_var'E (execD_var_erefl "x") (execD_var_erefl "y") /=.
@@ -226,31 +226,31 @@ Qed.
 Lemma exec_sample_pair0_TandT :
   @execP R [::] _ sample_pair_syntax0 tt [set (true, true)] = (1 / 6)%:E.
 Proof.
-rewrite exec_sample_pair0 mem_set//; do 3 rewrite memNset//=.
+rewrite exec_sample_pair0 !diracE mem_set//; do 3 rewrite memNset//=.
 by rewrite /= !mule0 mule1 !add0e mule0 adde0; congr (_%:E); lra.
 Qed.
 
 Lemma exec_sample_pair0_TandF :
   @execP R [::] _ sample_pair_syntax0 tt [set (true, false)] = (1 / 3)%:E.
 Proof.
-rewrite exec_sample_pair0 memNset// mem_set//; do 2 rewrite memNset//.
+rewrite exec_sample_pair0 !diracE memNset// mem_set//; do 2 rewrite memNset//.
 by rewrite /= !mule0 mule1 !add0e mule0 adde0; congr (_%:E); lra.
 Qed.
 
 Lemma exec_sample_pair0_TandT' :
   @execP R [::] _ sample_pair_syntax0 tt [set p | p.1 && p.2] = (1 / 6)%:E.
 Proof.
-rewrite exec_sample_pair0 mem_set//; do 3 rewrite memNset//=.
+rewrite exec_sample_pair0 !diracE mem_set//; do 3 rewrite memNset//=.
 by rewrite /= !mule0 mule1 !add0e mule0 adde0; congr (_%:E); lra.
 Qed.
 
 Lemma exec_sample_pair_TorT :
   (projT1 (execD sample_pair_syntax)) tt [set p | p.1 || p.2] = (2 / 3)%:E.
 Proof.
 rewrite execD_normalize_pt normalizeE/= exec_sample_pair0.
-do 4 rewrite mem_set//=.
+rewrite !diracE; do 4 rewrite mem_set//=.
 rewrite eqe ifF; last by apply/negbTE/negP => /orP[/eqP|//]; lra.
-rewrite exec_sample_pair0; do 3 rewrite mem_set//; rewrite memNset//=.
+rewrite exec_sample_pair0 !diracE; do 3 rewrite mem_set//; rewrite memNset//=.
 by rewrite !mule1; congr (_%:E); field.
 Qed.
 
@@ -260,9 +260,8 @@ Definition sample_and_syntax0 : @exp R _ [::] _ :=
    return #{"x"} && #{"y"}].
 
 Lemma exec_sample_and0 (A : set bool) :
-  @execP R [::] _ sample_and_syntax0 tt A =
-  ((1 / 6)%:E * (true \in A)%:R%:E +
-  (1 - 1 / 6)%:E * (false \in A)%:R%:E)%E.
+  @execP R [::] _ sample_and_syntax0 tt A = ((1 / 6)%:E * \d_true A +
+                                             (1 - 1 / 6)%:E * \d_false A)%E.
 Proof.
 rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=.
 rewrite (@execD_bin _ _ binop_and) !exp_var'E (execD_var_erefl "x") (execD_var_erefl "y") /=.
@@ -271,7 +270,7 @@ rewrite !integral_dirac//= !indicE !in_setT/= !mul1e.
 rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem.
 rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE.
 rewrite muleDr// -addeA; congr (_ + _)%E.
-by rewrite !muleA; congr (_%:E); congr (_ * _); field.
+  by rewrite !muleA; congr (_%:E); congr (_ * _); field.
 rewrite -muleDl// !muleA -muleDl//.
 by congr (_%:E); congr (_ * _); field.
 Qed.
@@ -283,9 +282,8 @@ Definition sample_bernoulli_and3 : @exp R _ [::] _ :=
    return #{"x"} && #{"y"} && #{"z"}].
 
 Lemma exec_sample_bernoulli_and3 t U :
-  execP sample_bernoulli_and3 t U =
-  ((1 / 8)%:E * (true \in U)%:R%:E +
-  (1 - 1 / 8)%:E * (false \in U)%:R%:E)%E.
+  execP sample_bernoulli_and3 t U = ((1 / 8)%:E * \d_true U +
+                                     (1 - 1 / 8)%:E * \d_false U)%E.
 Proof.
 rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=.
 rewrite !(@execD_bin _ _ binop_and) !exp_var'E.
@@ -307,25 +305,6 @@ Definition sample_add_syntax0 : @exp R _ [::] _ :=
    let "z" := Sample {exp_bernoulli (1 / 2)%:nng (p1S 1)} in
    return #{"x"} && #{"y"} && #{"z"}].
 
-Lemma exec_sample_bernoulli_and3 t U :
-  execP sample_bernoulli_and3 t U =
-  ((1 / 8)%:E * (true \in U)%:R%:E +
-  (1 - 1 / 8)%:E * (false \in U)%:R%:E)%E.
-Proof.
-rewrite !execP_letin !execP_sample !execD_bernoulli execP_return /=.
-rewrite !(@execD_bin _ _ binop_and) !exp_var'E.
-rewrite (execD_var_erefl "x") (execD_var_erefl "y") (execD_var_erefl "z") /=.
-rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e.
-rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e.
-rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem.
-rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE.
-rewrite !muleDr// -!addeA.
-by congr (_ + _)%E; rewrite ?addeA !muleA -?muleDl//;
-congr (_ * _)%E; congr (_%:E); field.
-Qed.
-
 End sample_pair.
 
 Section bernoulli_examples.
@@ -447,8 +426,8 @@ under eq_integral.
   over.
 rewrite !integral_measure_add //=; last by move=> b _; rewrite integral_ge0.
 rewrite !ge0_integral_mscale //=; last 2 first.
-  by move=> b _; rewrite integral_ge0.
-  by move=> b _; rewrite integral_ge0.
+  by move=> b _; exact: integral_ge0.
+  by move=> b _; exact: integral_ge0.
 rewrite !integral_dirac// !indicE !in_setT !mul1e.
 rewrite iteE/= !ge0_integral_mscale//=.
 rewrite ger0_norm//.

theories/measure.v

@@ -1217,32 +1217,24 @@ Lemma measurable_and (f : T1 -> bool) (g : T1 -> bool) :
   measurable_fun setT f -> measurable_fun setT g ->
   measurable_fun setT (fun x => f x && g x).
 Proof.
-move=> mf mg.
-apply: (@measurable_fun_bool _ _ true).
+move=> mf mg; apply: (@measurable_fun_bool _ _ true).
 rewrite [X in measurable X](_ : _ = f @^-1` [set true] `&` g @^-1` [set true]).
-apply: measurableI.
-rewrite -[X in measurable X]setTI.
-exact: mf.
-rewrite -[X in measurable X]setTI.
-exact: mg.
-apply/seteqP.
-by split; move=> x/andP.
+  apply: measurableI.
+  - rewrite -[X in measurable X]setTI; exact: mf.
+  - rewrite -[X in measurable X]setTI; exact: mg.
+by apply/seteqP; split => x /andP.
 Qed.
 
 Lemma measurable_or (f : T1 -> bool) (g : T1 -> bool) :
   measurable_fun setT f -> measurable_fun setT g ->
   measurable_fun setT (fun x => f x || g x).
 Proof.
-move=> mf mg.
-apply: (@measurable_fun_bool _ _ true).
+move=> mf mg; apply: (@measurable_fun_bool _ _ true).
 rewrite [X in measurable X](_ : _ = f @^-1` [set true] `|` g @^-1` [set true]).
-apply: measurableU.
-rewrite -[X in measurable X]setTI.
-exact: mf.
-rewrite -[X in measurable X]setTI.
-exact: mg.
-apply/seteqP.
-split; move=> x => /orP//.
+  apply: measurableU.
+  - rewrite -[X in measurable X]setTI; exact: mf.
+  - rewrite -[X in measurable X]setTI; exact: mg.
+by apply/seteqP; split=> x /orP.
 Qed.
 
 End measurable_fun.