Skip to content

Commit

Permalink
minor fixes
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Oct 10, 2023
1 parent 0a94990 commit ce0b897
Show file tree
Hide file tree
Showing 2 changed files with 26 additions and 55 deletions.
53 changes: 16 additions & 37 deletions theories/lang_syntax_examples.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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") /=.
Expand All @@ -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.

Expand All @@ -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") /=.
Expand All @@ -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.
Expand All @@ -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.
Expand All @@ -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.
Expand Down Expand Up @@ -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//.
Expand Down
28 changes: 10 additions & 18 deletions theories/measure.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1177,32 +1177,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.
Expand Down

0 comments on commit ce0b897

Please sign in to comment.