hard constraint example

theories/kernel.v

@@ -405,6 +405,16 @@ Notation "R .-ker X ~> Y" := (kernel X Y R).
 
 Arguments measurable_kernel {_ _ _ _ _} _.
 
+Lemma eq_kernel d d' (T : measurableType d) (T' : measurableType d') (R : realType)
+    (k1 k2 : R.-ker T ~> T') :
+  (forall x U, k1 x U = k2 x U) -> k1 = k2.
+Proof.
+move: k1 k2 => [m1 [[?]]] [m2 [[?]]] /= k12.
+have ? : m1 = m2.
+  by apply/funext => t; apply/eq_measure; apply/funext => U; rewrite k12.
+by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance.
+Qed.
+
 Section kseries.
 Variables (d d' : measure_display) (R : realType).
 Variables (X : measurableType d) (Y : measurableType d').
@@ -468,6 +478,16 @@ Notation "R .-sfker X ~> Y" := (sfinite_kernel X Y R).
 
 Arguments sfinite_subdef {_ _ _ _ _} _.
 
+Lemma eq_sfkernel d d' (T : measurableType d) (T' : measurableType d') (R : realType)
+    (k1 k2 : R.-sfker T ~> T') :
+  (forall x U, k1 x U = k2 x U) -> k1 = k2.
+Proof.
+move: k1 k2 => [m1 [[?] [?]]] [m2 [[?] [?]]] /= k12.
+have ? : m1 = m2.
+  by apply/funext => t; apply/eq_measure; apply/funext => U; rewrite k12.
+by subst m1; f_equal; f_equal; f_equal; apply/Prop_irrelevance.
+Qed.
+
 HB.mixin Record SFiniteKernel_isFinite
     d d' (X : measurableType d) (Y : measurableType d')
     (R : realType) (k : X -> {measure set Y -> \bar R}) :=
@@ -483,7 +503,8 @@ Notation "R .-fker X ~> Y" := (finite_kernel X Y R).
 Arguments measure_uub {_ _ _ _ _} _.
 
 HB.factory Record Kernel_isFinite d d' (X : measurableType d)
-    (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R}) of isKernel _ _ _ _ _ k := {
+    (Y : measurableType d') (R : realType) (k : X -> {measure set Y -> \bar R})
+    of isKernel _ _ _ _ _ k := {
   measure_uub : measure_fam_uub k }.
 
 Section kzero.
@@ -500,26 +521,9 @@ Proof. by move=> ?/=; exact: measurable_fun_cst. Qed.
 HB.instance Definition _ :=
   @isKernel.Build _ _ X Y R kzero measurable_fun_kzero.
 
-(*Let kernel_from_mzero_sfinite0 : exists2 s : (R.-ker T' ~> T)^nat, forall n, measure_fam_uub (s n) &
-    forall x U, measurable U -> kernel_from_mzero x U = kseries s x U.
-Proof.
-exists (fun=> [the _.-ker _ ~> _ of kernel_from_mzero]).
-  move=> _.
-  by exists 1%R => y; rewrite /= /mzero.
-by move=> t U mU/=; rewrite /mseries nneseries0.
-Qed.
-
-HB.instance Definition _ :=
-  @isSFinite0.Build _ _ _ T R kernel_from_mzero
-  kernel_from_mzero_sfinite0.*)
-
 Lemma kzero_uub : measure_fam_uub kzero.
 Proof. by exists 1%R => /= t; rewrite /mzero/=. Qed.
 
-(*HB.instance Definition _ :=
-  @SFiniteKernel_isFinite.Build _ _ _ T R kernel_from_mzero
-  kernel_from_mzero_uub.*)
-
 End kzero.
 
 HB.builders Context d d' (X : measurableType d) (Y : measurableType d')

theories/prob_lang.v

@@ -584,6 +584,20 @@ Definition score (f : X -> R) (mf : measurable_fun setT f) :=
 
 End insn1.
 
+Section hard_constraint.
+Variables (d d' : _) (X : measurableType d) (Y : measurableType d').
+Variable R : realType.
+
+Definition fail :=
+  letin (score (@measurable_fun_cst _ _ X _ setT (0%R : R)))
+        (ret (@measurable_fun_cst _ _ _ Y setT point)).
+
+Lemma failE x U : fail x U = 0.
+Proof. by rewrite /fail letinE ge0_integral_mscale//= normr0 mul0e. Qed.
+
+End hard_constraint.
+Arguments fail {d d' X Y R}.
+
 Module Notations.
 
 Notation var1of2 := (@measurable_fun_fst _ _ _ _).
@@ -600,6 +614,20 @@ Notation mbool := Datatypes_bool__canonical__measure_Measurable.
 
 End Notations.
 
+Section cst_fun.
+Variables (R : realType) (d : _) (T : measurableType d).
+
+Definition kr (r : R) := @measurable_fun_cst _ _ T _ setT r.
+Definition k3 : measurable_fun _ _ := kr 3%:R.
+Definition k10 : measurable_fun _ _ := kr 10%:R.
+Definition ktt := @measurable_fun_cst _ _ T _ setT tt.
+
+End cst_fun.
+Arguments kr {R d T}.
+Arguments k3 {R d T}.
+Arguments k10 {R d T}.
+Arguments ktt {d T}.
+
 Section insn1_lemmas.
 Import Notations.
 Variables (R : realType) (d : _) (T : measurableType d).
@@ -623,14 +651,30 @@ Proof. by rewrite /score/= /mscale/= ger0_norm// f0. Qed.
 
 Lemma score_score (f : R -> R) (g : R * unit -> R)
     (mf : measurable_fun setT f)
-    (mg : measurable_fun setT g) x U :
-  letin (score mf) (score mg) x U =
-  score (measurable_funM mf (measurable_fun_prod2 tt mg)) x U.
+    (mg : measurable_fun setT g) :
+  letin (score mf) (score mg) =
+  score (measurable_funM mf (measurable_fun_prod2 tt mg)).
 Proof.
+apply/eq_sfkernel => x U.
 rewrite {1}/letin; unlock.
 by rewrite kcomp_scoreE/= /mscale/= diracE normrM muleA EFinM.
 Qed.
 
+Import Notations.
+
+(* hard constraints to express score below 1 *)
+Lemma score_fail (r : {nonneg R}) (r1 : (r%:num <= 1)%R) :
+  score (kr r%:num) =
+  letin (sample (bernoulli r1) : R.-pker T ~> _)
+        (ite var2of2 (ret ktt) fail).
+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.
+by rewrite iteE//= iteE//= /mscale/= failE retE//= mule0 adde0 ger0_norm.
+Qed.
+
 End insn1_lemmas.
 
 Section letin_ite.
@@ -769,17 +813,6 @@ Qed.
 
 End exponential.
 
-Section cst_fun.
-Variables (R : realType) (d : _) (T : measurableType d).
-
-Definition kn (n : nat) := @measurable_fun_cst _ _ T _ setT (n%:R : R).
-Definition k3 : measurable_fun _ _ := kn 3.
-Definition k10 : measurable_fun _ _ := kn 10.
-
-End cst_fun.
-Arguments k3 {R d T}.
-Arguments k10 {R d T}.
-
 Lemma letin_sample_bernoulli (R : realType) (d d' : _) (T : measurableType d)
     (T' : measurableType d') (r : {nonneg R}) (r1 : (r%:num <= 1)%R)
     (u : R.-sfker [the measurableType _ of (T * bool)%type] ~> T') x y :