From 32e2918e3ab50add806e472cb148f381bf32df81 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 10 Oct 2023 10:05:01 +0900 Subject: [PATCH] minor fixes, updates, rebases --- coq-mathcomp-analysis.opam | 2 +- theories/lang_syntax.v | 18 +++--- theories/lang_syntax_examples.v | 104 +++++++++++++------------------- theories/lang_syntax_toy.v | 6 +- theories/lang_syntax_util.v | 3 +- theories/measure.v | 28 +++------ theories/prob_lang.v | 54 ++++++++--------- theories/prob_lang_wip.v | 10 +-- 8 files changed, 94 insertions(+), 131 deletions(-) diff --git a/coq-mathcomp-analysis.opam b/coq-mathcomp-analysis.opam index a449b7aec5..d2363e0088 100644 --- a/coq-mathcomp-analysis.opam +++ b/coq-mathcomp-analysis.opam @@ -22,7 +22,7 @@ depends: [ "coq-mathcomp-solvable" { (>= "2.0.0") | (= "dev") } "coq-mathcomp-field" "coq-mathcomp-bigenough" { (>= "1.0.0") } - "coq-mathcomp-algebra-tactics" { (>= "1.1.1") } + "coq-mathcomp-algebra-tactics" { (= "1.1.1") } ] tags: [ diff --git a/theories/lang_syntax.v b/theories/lang_syntax.v index ac3c32e4f9..5c1542ee10 100644 --- a/theories/lang_syntax.v +++ b/theories/lang_syntax.v @@ -1,8 +1,8 @@ Require Import String. From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. -From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. +From mathcomp Require Import mathcomp_extra boolp classical_sets. +From mathcomp Require Import functions cardinality fsbigop. Require Import signed reals ereal topology normedtype sequences esum measure. Require Import lebesgue_measure numfun lebesgue_integral kernel prob_lang. Require Import lang_syntax_util. @@ -89,7 +89,7 @@ Proof. done. Qed. Let mswap_sigma_additive x : semi_sigma_additive (mswap x). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ x := isMeasure.Build _ R _ +HB.instance Definition _ x := isMeasure.Build _ _ R (mswap x) (mswap0 x) (mswap_ge0 x) (@mswap_sigma_additive x). Definition mkswap : _ -> {measure set Z -> \bar R} := @@ -185,24 +185,22 @@ Let T0 z : (T' z) set0 = 0. Proof. by []. Qed. Let T_ge0 z x : 0 <= (T' z) x. Proof. by []. Qed. Let T_semi_sigma_additive z : semi_sigma_additive (T' z). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ z := @isMeasure.Build _ R X (T' z) (T0 z) (T_ge0 z) +HB.instance Definition _ z := @isMeasure.Build _ X R (T' z) (T0 z) (T_ge0 z) (@T_semi_sigma_additive z). Let sfinT z : sfinite_measure (T' z). Proof. exact: sfinite_kernel_measure. Qed. -HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ X R - (T' z) (sfinT z). +HB.instance Definition _ z := @isSFinite.Build _ X R (T' z) (sfinT z). Definition U' z : set Y -> \bar R := u z. Let U0 z : (U' z) set0 = 0. Proof. by []. Qed. Let U_ge0 z x : 0 <= (U' z) x. Proof. by []. Qed. Let U_semi_sigma_additive z : semi_sigma_additive (U' z). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ z := @isMeasure.Build _ R Y (U' z) (U0 z) (U_ge0 z) +HB.instance Definition _ z := @isMeasure.Build _ Y R (U' z) (U0 z) (U_ge0 z) (@U_semi_sigma_additive z). Let sfinU z : sfinite_measure (U' z). Proof. exact: sfinite_kernel_measure. Qed. -HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ Y R - (U' z) (sfinU z). +HB.instance Definition _ z := @isSFinite.Build _ Y R (U' z) (sfinU z). Lemma letin'C z A : measurable A -> letin' t @@ -271,7 +269,7 @@ Inductive typ := | Pair : typ -> typ -> typ | Prob : typ -> typ. -Canonical stype_eqType := Equality.Pack (@gen_eqMixin typ). +HB.instance Definition _ := gen_eqMixin typ. Fixpoint measurable_of_typ (t : typ) : {d & measurableType d} := match t with diff --git a/theories/lang_syntax_examples.v b/theories/lang_syntax_examples.v index 8a365773ee..4be13e9c55 100644 --- a/theories/lang_syntax_examples.v +++ b/theories/lang_syntax_examples.v @@ -59,7 +59,7 @@ Lemma letin'_sample_bernoulli d d' (T : measurableType d) Proof. rewrite letin'E/=. rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. -by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e. +by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT 2!mul1e. Qed. Section letin'_return. @@ -81,7 +81,7 @@ Lemma letin'_retk (f : X -> Y) (mf : measurable_fun setT f) (k : R.-sfker Y * X ~> Z) x U : measurable U -> letin' (ret mf) k x U = k (f x, x) U. Proof. -move=> mU; rewrite letin'E retE integral_dirac ?indicT ?mul1e//. +move=> mU; rewrite letin'E retE integral_dirac ?diracT ?mul1e//. exact: (measurableT_comp (measurable_kernel k _ mU)). Qed. @@ -209,38 +209,38 @@ 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") /=. rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e. +rewrite !integral_dirac//= !diracT !mul1e. rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem. -by rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE. +by rewrite !integral_dirac//= !diracT !mul1e. 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. @@ -248,9 +248,9 @@ 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,18 +260,17 @@ 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") /=. rewrite letin'E integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e. +rewrite !integral_dirac//= !diracT !mul1e. rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE. +rewrite !integral_dirac//= !diracT !mul1e. 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,19 +282,18 @@ 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. 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 !integral_dirac//= !diracT !mul1e. rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e. +rewrite !integral_dirac//= !diracT !mul1e. rewrite !letin'E !integral_measure_add//= !ge0_integral_mscale//= /onem. -rewrite !integral_dirac//= !indicE !in_setT/= !mul1e !diracE. +rewrite !integral_dirac//= !diracT !mul1e. rewrite !muleDr// -!addeA. by congr (_ + _)%E; rewrite ?addeA !muleA -?muleDl//; congr (_ * _)%E; congr (_%:E); field. @@ -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. @@ -357,24 +336,23 @@ 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. -rewrite !integral_dirac// !indicE !in_setT !mul1e. +rewrite !integral_dirac// !diracT !mul1e. rewrite iteE/= !ge0_integral_mscale//=. rewrite ger0_norm//. rewrite !integral_indic//= !iteE/= /mscale/=. -rewrite setTI diracE !in_setT !mule1. +rewrite setTI !diracT !mule1. rewrite ger0_norm//. rewrite -EFinD/= eqe ifF; last first. by apply/negbTE/negP => /orP[/eqP|//]; rewrite /onem; lra. rewrite !letin'E/= !iteE/=. rewrite !ge0_integral_mscale//=. rewrite ger0_norm//. -rewrite !integral_dirac//= !indicE !in_setT /= !mul1e ger0_norm//. +rewrite !integral_dirac//= !diracT !mul1e ger0_norm//. rewrite exp_var'E (execD_var_erefl "x")/=. rewrite /bernoulli/= measure_addE/= /mscale/= !mul1r. -rewrite muleDl//; congr (_ + _)%E; - rewrite -!EFinM; - congr (_%:E); - by rewrite indicE /onem; case: (_ \in _); field. +by rewrite muleDl//; congr (_ + _)%E; + rewrite -!EFinM; congr (_%:E); + rewrite !indicT !indicE /onem /=; case: (_ \in _); field. Qed. Definition bernoulli12_score := [Normalize @@ -400,11 +378,11 @@ 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. -rewrite !integral_dirac// !indicE !in_setT !mul1e. +rewrite !integral_dirac// !diracT !mul1e. rewrite iteE/= !ge0_integral_mscale//=. rewrite ger0_norm//. rewrite !integral_indic//= !iteE/= /mscale/=. -rewrite setTI diracE !in_setT !mule1. +rewrite setTI !diracT !mule1. rewrite ger0_norm//. rewrite -EFinD/= eqe ifF; last first. apply/negbTE/negP => /orP[/eqP|//]. @@ -412,13 +390,13 @@ rewrite -EFinD/= eqe ifF; last first. rewrite !letin'E/= !iteE/=. rewrite !ge0_integral_mscale//=. rewrite ger0_norm//. -rewrite !integral_dirac//= !indicE !in_setT /= !mul1e ger0_norm//. +rewrite !integral_dirac//= !diracT !mul1e ger0_norm//. rewrite exp_var'E (execD_var_erefl "x")/=. rewrite /bernoulli/= measure_addE/= /mscale/= !mul1r. rewrite muleDl//; congr (_ + _)%E; rewrite -!EFinM; congr (_%:E); - by rewrite indicE /onem; case: (_ \in _); field. + by rewrite !indicT !indicE /onem /=; case: (_ \in _); field. Qed. (* https://dl.acm.org/doi/pdf/10.1145/2933575.2935313 (Sect. 4) *) @@ -447,13 +425,13 @@ 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. -rewrite !integral_dirac// !indicE !in_setT !mul1e. + by move=> b _; exact: integral_ge0. + by move=> b _; exact: integral_ge0. +rewrite !integral_dirac// !diracT !mul1e. rewrite iteE/= !ge0_integral_mscale//=. rewrite ger0_norm//. -rewrite !integral_indic//= !iteE/= /mscale/=. -rewrite setTI diracE !in_setT !mule1. +rewrite !integral_cst//= !diracT !(mule1,mul1e). +rewrite !iteE/= /mscale/= !diracT !mule1. rewrite ger0_norm//. rewrite -EFinD/= eqe ifF; last first. apply/negbTE/negP => /orP[/eqP|//]. @@ -461,12 +439,12 @@ rewrite -EFinD/= eqe ifF; last first. rewrite !letin'E/= !iteE/=. rewrite !ge0_integral_mscale//=. rewrite ger0_norm//. -rewrite !integral_dirac//= !indicE !in_setT /= !mul1e ger0_norm//. +rewrite !integral_dirac//= !diracT !mul1e ger0_norm//. rewrite /bernoulli/= measure_addE/= /mscale/= !mul1r. rewrite muleDl//; congr (_ + _)%E; rewrite -!EFinM; congr (_%:E); - by rewrite indicE /onem; case: (_ \in _); field. + by rewrite !indicT !indicE /onem /=; case: (_ \in _); field. Qed. End bernoulli_examples. @@ -494,7 +472,7 @@ Proof. apply/eq_sfkernel => x U. rewrite letin'E/= /sample; unlock. rewrite integral_measure_add//= ge0_integral_mscale//= ge0_integral_mscale//=. -rewrite integral_dirac//= integral_dirac//= !indicT/= !mul1e. +rewrite !integral_dirac//= !diracT/= !mul1e. by rewrite /mscale/= iteE//= iteE//= fail'E mule0 adde0 ger0_norm. Qed. diff --git a/theories/lang_syntax_toy.v b/theories/lang_syntax_toy.v index a328ea1cd7..2c2f572673 100644 --- a/theories/lang_syntax_toy.v +++ b/theories/lang_syntax_toy.v @@ -1,7 +1,7 @@ Require Import String Classical. From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg. -From mathcomp.classical Require Import mathcomp_extra boolp. +From mathcomp Require Import mathcomp_extra boolp. Require Import signed reals topology normedtype. Require Import lang_syntax_util. @@ -36,7 +36,7 @@ Variables (R : realType). Inductive typ := Real | Unit. -Canonical typ_eqType := Equality.Pack (@gen_eqMixin typ). +HB.instance Definition _ := gen_eqMixin typ. Definition iter_pair (l : list Type) : Type := foldr (fun x y => (x * y)%type) unit l. @@ -169,7 +169,7 @@ Implicit Types str : string. Inductive typ := Real | Unit | Pair : typ -> typ -> typ. -Canonical typ_eqType := Equality.Pack (@gen_eqMixin typ). +HB.instance Definition _ := gen_eqMixin typ. Fixpoint mtyp (t : typ) : Type := match t with diff --git a/theories/lang_syntax_util.v b/theories/lang_syntax_util.v index ad84918c9b..608d25e7ef 100644 --- a/theories/lang_syntax_util.v +++ b/theories/lang_syntax_util.v @@ -8,8 +8,7 @@ Require Import signed. (* Shared by lang_syntax_*.v files *) (******************************************************************************) -Definition string_eqMixin := @EqMixin string String.eqb eqb_spec. -Canonical string_eqType := EqType string string_eqMixin. +HB.instance Definition _ := hasDecEq.Build string eqb_spec. Ltac inj_ex H := revert H; match goal with diff --git a/theories/measure.v b/theories/measure.v index 6ea3182fa6..1733f44985 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -1181,32 +1181,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. diff --git a/theories/prob_lang.v b/theories/prob_lang.v index d870d50728..54d075387e 100644 --- a/theories/prob_lang.v +++ b/theories/prob_lang.v @@ -2,10 +2,10 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import rat. -From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. +From mathcomp Require Import mathcomp_extra boolp classical_sets. +From mathcomp Require Import functions cardinality fsbigop. Require Import reals ereal signed topology normedtype sequences esum measure. -Require Import lebesgue_measure numfun lebesgue_integral exp kernel. +Require Import lebesgue_measure numfun lebesgue_integral exp kernel. (******************************************************************************) (* Semantics of a probabilistic programming language using s-finite kernels *) @@ -86,7 +86,6 @@ Qed. Section bernoulli. Variables (R : realType) (p : {nonneg R}) (p1 : (p%:num <= 1)%R). -Local Open Scope ring_scope. Definition bernoulli : set _ -> \bar R := measure_add @@ -95,8 +94,6 @@ Definition bernoulli : set _ -> \bar R := HB.instance Definition _ := Measure.on bernoulli. -Local Close Scope ring_scope. - Let bernoulli_setT : bernoulli [set: _] = 1. Proof. rewrite /bernoulli/= /measure_add/= /msum 2!big_ord_recr/= big_ord0 add0e/=. @@ -116,7 +113,7 @@ Lemma integral_bernoulli {R : realType} Proof. move=> f0. rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. -by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e. +by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT !mul1e. Qed. Section uniform_probability. @@ -131,7 +128,7 @@ HB.instance Definition _ := Measure.on uniform_probability. Let uniform_probability_setT : uniform_probability [set: _] = 1. Proof. rewrite /uniform_probability /mscale/= /mrestr/=. -rewrite setTI lebesgue_measure_itv hlength_itv/= lte_fin. +rewrite setTI lebesgue_measure_itv/= lte_fin. by rewrite -subr_gt0 ab0 -EFinD -EFinM mulVf// gt_eqF// subr_gt0. Qed. @@ -528,7 +525,7 @@ Proof. apply/eq_measure/funext => U. rewrite /ite; unlock => /=. rewrite /kcomp/= integral_dirac//=. -rewrite indicT mul1e. +rewrite diracT mul1e. rewrite -/(measure_add (ITE.kiteT k1 (x, f x)) (ITE.kiteF k2 (x, f x))). rewrite measure_addE. rewrite /ITE.kiteT /ITE.kiteF/=. @@ -588,7 +585,7 @@ Lemma letin_retk x U : measurable U -> letin (ret mf) k x U = k (x, f x) U. Proof. -move=> mU; rewrite letinE retE integral_dirac ?indicT ?mul1e//. +move=> mU; rewrite letinE retE integral_dirac ?diracT ?mul1e//. exact: (measurableT_comp (measurable_kernel k _ mU)). Qed. @@ -893,7 +890,7 @@ Let kcomp_scoreE d1 d2 (T1 : measurableType d1) (T2 : measurableType d2) (score mf \; g) r U = `|f r|%:E * g (r, tt) U. Proof. rewrite /= /kcomp /kscore /= ge0_integral_mscale//=. -by rewrite integral_dirac// indicT mul1e. +by rewrite integral_dirac// diracT mul1e. Qed. Lemma scoreE d' (T' : measurableType d') (x : T * T') (U : set T') (f : R -> R) @@ -926,7 +923,7 @@ Proof. apply/eq_sfkernel => x U. rewrite letinE/= /sample; unlock. rewrite integral_measure_add//= ge0_integral_mscale//= ge0_integral_mscale//=. -rewrite integral_dirac//= integral_dirac//= !indicT/= !mul1e. +rewrite integral_dirac//= integral_dirac//= !diracT/= !mul1e. by rewrite /mscale/= iteE//= iteE//= failE mule0 adde0 ger0_norm. Qed. @@ -1004,24 +1001,23 @@ Let T0 z : (T z) set0 = 0. Proof. by []. Qed. Let T_ge0 z x : 0 <= (T z) x. Proof. by []. Qed. Let T_semi_sigma_additive z : semi_sigma_additive (T z). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ z := @isMeasure.Build _ R X (T z) (T0 z) (T_ge0 z) +HB.instance Definition _ z := @isMeasure.Build _ X R (T z) (T0 z) (T_ge0 z) (@T_semi_sigma_additive z). Let sfinT z : sfinite_measure (T z). Proof. exact: sfinite_kernel_measure. Qed. -HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ X R - (T z) (sfinT z). + +HB.instance Definition _ z := @isSFinite.Build _ X R (T z) (sfinT z). Definition U z : set Y -> \bar R := u z. Let U0 z : (U z) set0 = 0. Proof. by []. Qed. Let U_ge0 z x : 0 <= (U z) x. Proof. by []. Qed. Let U_semi_sigma_additive z : semi_sigma_additive (U z). Proof. exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ z := @isMeasure.Build _ R Y (U z) (U0 z) (U_ge0 z) +HB.instance Definition _ z := @isMeasure.Build _ Y R (U z) (U0 z) (U_ge0 z) (@U_semi_sigma_additive z). Let sfinU z : sfinite_measure (U z). Proof. exact: sfinite_kernel_measure. Qed. -HB.instance Definition _ z := @Measure_isSFinite_subdef.Build _ Y R - (U z) (sfinU z). +HB.instance Definition _ z := @isSFinite.Build _ Y R (U z) (sfinU z). Lemma letinC z A : measurable A -> letin t @@ -1055,7 +1051,7 @@ End letinC. Section constants. Variable R : realType. -Local Open Scope ring_scope. +Local Close Scope ereal_scope. Lemma onem1S n : `1- (1 / n.+1%:R) = (n%:R / n.+1%:R)%:nng%:num :> R. Proof. @@ -1063,7 +1059,7 @@ by rewrite /onem/= -{1}(@divrr _ n.+1%:R) ?unitfE// -mulrBl -natr1 addrK. Qed. Lemma p1S n : (1 / n.+1%:R)%:nng%:num <= 1 :> R. -Proof. by rewrite ler_pdivr_mulr//= mul1r ler1n. Qed. +Proof. by rewrite ler_pdivrMr//= mul1r ler1n. Qed. Lemma p12 : (1 / 2%:R)%:nng%:num <= 1 :> R. Proof. by rewrite p1S. Qed. @@ -1073,7 +1069,7 @@ Lemma onem27 : `1- (2 / 7%:R) = (5%:R / 7%:R)%:nng%:num :> R. Proof. by apply/eqP; rewrite subr_eq/= -mulrDl -natrD divrr// unitfE. Qed. Lemma p27 : (2 / 7%:R)%:nng%:num <= 1 :> R. -Proof. by rewrite /= lter_pdivr_mulr// mul1r ler_nat. Qed. +Proof. by rewrite /= lter_pdivrMr// mul1r ler_nat. Qed. End constants. Arguments p12 {R}. @@ -1145,7 +1141,7 @@ Lemma letin_sample_bernoulli d d' (T : measurableType d) Proof. rewrite letinE/=. rewrite ge0_integral_measure_sum// 2!big_ord_recl/= big_ord0 adde0/=. -by rewrite !ge0_integral_mscale//= !integral_dirac//= indicT 2!mul1e. +by rewrite !ge0_integral_mscale//= !integral_dirac//= !diracT 2!mul1e. Qed. Section sample_and_return. @@ -1327,8 +1323,8 @@ Qed. End staton_bus_exponential. (* X + Y is a measurableType if X and Y are *) -Canonical sum_pointedType (X Y : pointedType) := - PointedType (X + Y) (@inl X Y point). +HB.instance Definition _ (X Y : pointedType) := + isPointed.Build (X + Y)%type (@inl X Y point). Section measurable_sum. Context d d' (X : measurableType d) (Y : measurableType d'). @@ -1344,7 +1340,7 @@ Let sumU (F : (set (X + Y))^nat) : (forall i, measurable_sum (F i)) -> Proof. by []. Qed. HB.instance Definition _ := @isMeasurable.Build default_measure_display (X + Y)%type - (Pointed.class _) measurable_sum sum0 sumC sumU. + measurable_sum sum0 sumC sumU. End measurable_sum. @@ -1485,7 +1481,7 @@ Proof. exact: sigma_algebra_bigcup. Qed. HB.instance Definition sum_salgebra_mixin := @isMeasurable.Build (measure_sum_display (d1, d2)) - (T1 + T2)%type (Pointed.class _) (image_classes f1 f2) + (T1 + T2)%type (image_classes f1 f2) (sum_salgebra_set0) (sum_salgebra_setC) (sum_salgebra_bigcup). End sum_salgebra_instance. @@ -1748,9 +1744,9 @@ exists (fun n => [the R.-ker _ ~> _ of case_sum' (fun ab => [the R.-fker _ ~> _ have [rfalse Hrfalse] := measure_uub (f (inr false) n). have [rtrue Hrtrue] := measure_uub (f (inr true) n). exists (maxr rtt (maxr rfalse rtrue)) => //= -[x [[]|[|]]] /=. - by rewrite 2!EFin_max lt_maxr Hrtt. - by rewrite /CASE_SUM.case_sumr /= 2!EFin_max 2!lt_maxr Hrtrue 2!orbT. - by rewrite /CASE_SUM.case_sumr /= 2!EFin_max 2!lt_maxr Hrfalse orbT. + by rewrite 2!EFin_max lt_max Hrtt. + by rewrite /CASE_SUM.case_sumr /= 2!EFin_max 2!lt_max Hrtrue 2!orbT. + by rewrite /CASE_SUM.case_sumr /= 2!EFin_max 2!lt_max Hrfalse orbT. move=> [x [[]|[|]]] U mU/=-. by rewrite (Hf (inl tt) x _ mU). by rewrite (Hf (inr true) x _ mU). diff --git a/theories/prob_lang_wip.v b/theories/prob_lang_wip.v index 9ab73014b7..fd6716937f 100644 --- a/theories/prob_lang_wip.v +++ b/theories/prob_lang_wip.v @@ -1,8 +1,8 @@ From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import rat. -From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. -From mathcomp.classical Require Import functions cardinality fsbigop. +From mathcomp Require Import mathcomp_extra boolp classical_sets functions. +From mathcomp Require Import cardinality fsbigop. Require Import signed reals ereal topology normedtype sequences esum measure. Require Import lebesgue_measure numfun lebesgue_integral exp kernel trigo. Require Import prob_lang. @@ -81,7 +81,7 @@ rewrite /mgauss01/= integral_bigcup//=; last first. rewrite (_ : (fun x => _) = (EFin \o gauss01_density)); last first. by apply/funext => x; rewrite gee0_abs// lee_fin gauss_density_ge0. apply: le_lt_trans. - apply: (@subset_integral _ _ _ _ _ setT) => //=. + apply: (@ge0_subset_integral _ _ _ _ _ setT) => //=. apply/EFin_measurable_fun. exact: measurable_fun_gauss_density. by move=> ? _; rewrite lee_fin gauss_density_ge0. @@ -142,7 +142,7 @@ transitivity (\int[@mgauss01 R]_(y in U) (f1 y)%:E). apply: eq_integral => //= r. rewrite letinE/= ge0_integral_mscale//= ger0_norm//; last first. by rewrite invr_ge0// gauss_density_ge0. - by rewrite integral_dirac// indicT mul1e diracE indicE. + by rewrite integral_dirac// diracT mul1e diracE indicE. rewrite integral_mgauss01//. transitivity (\int[lebesgue_measure]_(x in U) (\1_U x)%:E). apply: eq_integral => /= y yU. @@ -196,7 +196,7 @@ rewrite /mpoisson1/= integral_bigcup//=; last first. rewrite (_ : (fun x => _) = (EFin \o poisson1)); last first. by apply/funext => x; rewrite gee0_abs// lee_fin poisson1_ge0//. apply: le_lt_trans. - apply: (@subset_integral _ _ _ _ _ setT) => //=. + apply: (@ge0_subset_integral _ _ _ _ _ setT) => //=. by apply/EFin_measurable_fun; exact: measurable_poisson. by move=> ? _; rewrite lee_fin poisson1_ge0//. by rewrite /= integral_poisson_density// ltry.