rm duplicate, more uniform naming

theories/kernel.v

@@ -753,46 +753,14 @@ HB.instance Definition _ t :=
   Kernel_isFinite.Build _ _ _ _ R (kadd k1 k2) kadd_finite_uub.
 End fkadd.
 
-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 =>
-    [the probability _ _ of mnormalize (k x) point] : pprobability Y R).
-Proof.
-apply: (@measurability _ _ _ _ _ _
-  (@pset _ _ _ : set (set (pprobability Y R)))) => //.
-move=> _ -[_ [r r01] [Ys mYs <-]] <-.
-rewrite /mnormalize /mset /preimage/=.
-apply: emeasurable_fun_infty_o => //.
-rewrite /mnormalize/=.
-rewrite (_ : (fun x => _) = (fun x => if (k x setT == 0) || (k x setT == +oo)
-    then \d_point Ys else k x Ys * ((fine (k x setT))^-1)%:E)); last first.
-  by apply/funext => x/=; case: ifPn.
-apply: measurable_fun_if => //.
-- apply: (measurable_fun_bool true) => //.
-  rewrite (_ : _ @^-1` _ = [set t | k t setT == 0] `|`
-                           [set t | k t setT == +oo]); last first.
-    by apply/seteqP; split=> x /= /orP//.
-  by apply: measurableU; exact: kernel_measurable_eq_cst.
-- apply/emeasurable_funM; first exact/measurable_funTS/measurable_kernel.
-  apply/EFin_measurable_fun; rewrite setTI.
-  apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]).
-  + exact: open_measurable.
-  + by move=> /= _ [x /norP[s0 soo]] <-; rewrite -eqe fineK ?ge0_fin_numE ?ltey.
-  + apply: open_continuous_measurable_fun => //; apply/in_setP => x /= x0.
-    exact: inv_continuous.
-  + by apply: measurableT_comp => //; exact/measurable_funS/measurable_kernel.
-Qed.
-
 Section knormalize.
 Context d d' (X : measurableType d) (Y : measurableType d') (R : realType).
 Variable f : R.-ker X ~> Y.
 
 Definition knormalize (P : probability Y R) : X -> {measure set Y -> \bar R} :=
   fun x => [the measure _ _ of mnormalize (f x) P].
 
-Variable P : probability Y R.
-
-Let measurable_fun_knormalize U :
+Let measurable_knormalize (P : probability Y R) U :
   measurable U -> measurable_fun [set: X] (knormalize P ^~ U).
 Proof.
 move=> mU; rewrite /knormalize/= /mnormalize /=.
@@ -809,7 +777,7 @@ apply: measurable_fun_if => //.
 - apply: (@measurable_funS _ _ _ _ setT) => //.
   exact: kernel_measurable_fun_eq_cst.
 - apply: emeasurable_funM.
-    by have := measurable_kernel f U mU; exact: measurable_funS.
+    exact: measurable_funS (measurable_kernel f U mU).
   apply/EFin_measurable_fun.
   apply: (@measurable_comp _ _ _ _ _ _ [set r : R | r != 0%R]) => //.
   + exact: open_measurable.
@@ -822,14 +790,14 @@ apply: measurable_fun_if => //.
     by have := measurable_kernel f _ measurableT; exact: measurable_funS.
 Qed.
 
-HB.instance Definition _ := isKernel.Build _ _ _ _ R (knormalize P)
-  measurable_fun_knormalize.
+HB.instance Definition _ (P : probability Y R) :=
+  isKernel.Build _ _ _ _ R (knormalize P) (measurable_knormalize P).
 
-Let knormalize1 x : knormalize P x [set: Y] = 1.
+Let knormalize1 (P : probability Y R) x : knormalize P x [set: Y] = 1.
 Proof. by rewrite /knormalize/= probability_setT. Qed.
 
-HB.instance Definition _ :=
-  @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) knormalize1.
+HB.instance Definition _ (P : probability Y R):=
+  @Kernel_isProbability.Build _ _ _ _ _ (knormalize P) (knormalize1 P).
 
 End knormalize.
 

theories/lang_syntax.v

@@ -449,12 +449,6 @@ Notation "'Normalize' e" := (exp_normalize e)
 Notation "'if' e1 'then' e2 'else' e3" := (exp_if e1 e2 e3)
   (in custom expr at level 1) : lang_scope.
 
-Local Open Scope lang_scope.
-Example three_letin {R : realType} x y z : @exp R P [::] _ :=
-  [let x := return {1}:R in
-   let y := return #x in
-   let z := return #y in return #z].
-
 Section free_vars.
 Context {R : realType}.
 
@@ -609,7 +603,7 @@ Inductive evalD : forall g t, exp D g t ->
 
 | eval_normalize g t (e : exp P g t) k :
   e -P> k ->
-  [Normalize e] -D> normalize k point ; measurable_fun_mnormalize k
+  [Normalize e] -D> normalize_pt k ; measurable_normalize_pt k
 
 | evalD_if g t e f mf (e1 : exp D g t) f1 mf1 e2 f2 mf2 :
   e -D> f ; mf -> e1 -D> f1 ; mf1 -> e2 -D> f2 ; mf2 ->
@@ -630,8 +624,8 @@ with evalP : forall g t, exp P g t -> pval R g t -> Prop :=
   [let str := e1 in e2] -P> letin' k1 k2
 
 | eval_sample g t (e : exp _ _ (Prob t))
-    (p : mctx g -> pprobability (mtyp t) R) mp :
-  e -D> p ; mp -> [Sample e] -P> sample p mp
+    (f : mctx g -> probability (mtyp t) R) mf :
+  e -D> f ; mf -> [Sample e] -P> sample f mf
 
 | eval_score g (e : exp _ g _) f mf :
   e -D> f ; mf -> [Score e] -P> kscore mf
@@ -750,13 +744,13 @@ all: (rewrite {g t e u v mu mv hu}).
   inj_ex H6; subst e5.
   inj_ex H5; subst e4.
   by rewrite (IH1 _ H4) (IH2 _ H8).
-- move=> g t e p mp ev IH k.
+- move=> g t e f mf ev IH k.
   inversion 1; subst g0.
   inj_ex H5; subst t0.
   inj_ex H5; subst e1.
   inj_ex H7; subst k.
-  have ? := IH _ _ H3; subst p1.
-  by have -> : mp = mp1 by [].
+  have ? := IH _ _ H3; subst f1.
+  by have -> : mf = mf1 by [].
 - move=> g e f mf ev IH k.
   inversion 1; subst g0.
   inj_ex H0; subst e0.
@@ -875,12 +869,12 @@ all: rewrite {g t e u v eu}.
   inj_ex H5; subst e4.
   inj_ex H6; subst e5.
   by rewrite (IH1 _ H4) (IH2 _ H8).
-- move=> g t e p mp ep IH v.
+- move=> g t e f mf ep IH v.
   inversion 1; subst g0 t0.
   inj_ex H7; subst v.
   inj_ex H5; subst e1.
-  have ? := IH _ _ H3; subst p1.
-  by have -> : mp = mp1 by [].
+  have ? := IH _ _ H3; subst f1.
+  by have -> : mf = mf1 by [].
 - move=> g e f mf ev IH k.
   inversion 1; subst g0.
   inj_ex H0; subst e0.
@@ -931,7 +925,7 @@ all: rewrite {z g t}.
 - move=> g h e [f [mf H]].
   by exists (poisson h \o f); eexists; exact: eval_poisson.
 - move=> g t e [k ek].
-  by exists (normalize k point); eexists; exact: eval_normalize.
+  by exists (normalize_pt k); eexists; exact: eval_normalize.
 - move=> g t1 t2 x e1 [k1 ev1] e2 [k2 ev2].
   by exists (letin' k1 k2); exact: eval_letin.
 - move=> g t e [f [/= mf ef]].
@@ -1072,10 +1066,10 @@ Lemma execD_bernoulli g r (r1 : (r%:num <= 1)%R) :
     existT _ (cst [the probability _ _ of bernoulli r1]) (measurable_cst _).
 Proof. exact/execD_evalD/eval_bernoulli. Qed.
 
-Lemma execD_normalize g t (e : exp P g t) :
+Lemma execD_normalize_pt g t (e : exp P g t) :
   @execD g _ [Normalize e] =
-  existT _ (normalize (execP e) point : _ -> pprobability _ _)
-           (measurable_fun_mnormalize (execP e)).
+  existT _ (normalize_pt (execP e) : _ -> pprobability _ _)
+           (measurable_normalize_pt (execP e)).
 Proof. exact/execD_evalD/eval_normalize/evalP_execP. Qed.
 
 Lemma execD_poisson g n (e : exp D g Real) :

theories/lang_syntax_examples.v

@@ -137,35 +137,46 @@ Qed.
 Local Close Scope lang_scope.
 
 (* simple tests to check bidirectional hints *)
-Module tests_bidi.
+Module bidi_tests.
 Local Open Scope lang_scope.
 Import Notations.
 Context (R : realType).
 
-Definition v1 x : @exp R P [::] _ := [
+Definition bidi_test1 x : @exp R P [::] _ := [
   let x := return {1}:R in
   return #x].
 
-Definition v2 (a b : string)
+Definition bidi_test2 (a b : string)
   (a := "a") (b := "b")
-  (* (H : infer (b != a)) *)
+  (* (ba : infer (b != a)) *)
   : @exp R P [::] _ := [
   let a := return {1}:R in
   let b := return {true}:B in
   (* let c := return {3}:R in
   let d := return {4}:R in *)
   return (#a, #b)].
 
-Definition v3 (a b c d : string) (H1 : infer (b != a)) (H2 : infer (c != a))
-  (H3 : infer (c != b)) (H4 : infer (a != b)) (H5 : infer (a != c))
-  (H6 : infer (b != c)) : @exp R P [::] _ := [
+Definition bidi_test3 (a b c d : string)
+    (ba : infer (b != a)) (ca : infer (c != a))
+    (cb : infer (c != b)) (ab : infer (a != b))
+    (ac : infer (a != c)) (bc : infer (b != c)) : @exp R P [::] _ := [
   let a := return {1}:R in
   let b := return {2}:R in
   let c := return {3}:R in
   (* let d := return {4}:R in *)
   return (#b, #a)].
 
-End tests_bidi.
+Definition bidi_test4 (a b c d : string)
+    (ba : infer (b != a)) (ca : infer (c != a))
+    (cb : infer (c != b)) (ab : infer (a != b))
+    (ac : infer (a != c)) (bc : infer (b != c)) : @exp R P [::] _ := [
+  let a := return {1}:R in
+  let b := return {2}:R in
+  let c := return {3}:R in
+  (* let d := return {4}:R in *)
+  return {exp_poisson O [#c(*{exp_var c erefl}*)]}].
+
+End bidi_tests.
 
 Section trivial_example.
 Local Open Scope lang_scope.
@@ -175,7 +186,8 @@ Context {R : realType}.
 Lemma exec_normalize_return g x r :
   projT1 (@execD _ g _ [Normalize return r:R]) x = \d_r :> probability _ R.
 Proof.
-by rewrite execD_normalize execP_return execD_real/= normalize_kdirac.
+rewrite execD_normalize_pt execP_return execD_real/=.
+exact: normalize_kdirac.
 Qed.
 
 End trivial_example.
@@ -235,7 +247,7 @@ 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 normalizeE/= exec_sample_pair0.
+rewrite execD_normalize_pt normalizeE/= exec_sample_pair0.
 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//=.
@@ -259,7 +271,7 @@ Lemma exec_bernoulli13_score :
   execD bernoulli13_score = execD (exp_bernoulli (1 / 5%:R)%:nng (p1S 4)).
 Proof.
 apply: eq_execD.
-rewrite execD_bernoulli/= /bernoulli13_score execD_normalize 2!execP_letin.
+rewrite execD_bernoulli/= /bernoulli13_score execD_normalize_pt 2!execP_letin.
 rewrite execP_sample/= execD_bernoulli/= execP_if /= exp_var'E.
 rewrite (execD_var_erefl "x")/= !execP_return/= 2!execP_score 2!execD_real/=.
 apply: funext=> g; apply: eq_probability => U.
@@ -302,7 +314,7 @@ Lemma exec_bernoulli12_score :
   execD bernoulli12_score = execD (exp_bernoulli (1 / 3%:R)%:nng (p1S 2)).
 Proof.
 apply: eq_execD.
-rewrite execD_bernoulli/= /bernoulli12_score execD_normalize 2!execP_letin.
+rewrite execD_bernoulli/= /bernoulli12_score execD_normalize_pt 2!execP_letin.
 rewrite execP_sample/= execD_bernoulli/= execP_if /= exp_var'E.
 rewrite (execD_var_erefl "x")/= !execP_return/= 2!execP_score 2!execD_real/=.
 apply: funext=> g; apply: eq_probability => U.
@@ -350,7 +362,7 @@ Lemma exec_bernoulli14_score :
   execD bernoulli14_score = execD (exp_bernoulli (5%:R / 11%:R)%:nng p511).
 Proof.
 apply: eq_execD.
-rewrite execD_bernoulli/= execD_normalize 2!execP_letin.
+rewrite execD_bernoulli/= execD_normalize_pt 2!execP_letin.
 rewrite execP_sample/= execD_bernoulli/= execP_if /= !exp_var'E.
 rewrite !execP_return/= 2!execP_score 2!execD_real/=.
 rewrite !(execD_var_erefl "x")/=.
@@ -506,12 +518,43 @@ Local Open Scope lang_scope.
 Import Notations.
 Context {R : realType}.
 
+Section tests.
+
+Local Notation "$ str" := (@exp_var _ _ str%string _ erefl)
+  (in custom expr at level 1, format "$ str").
+
+Definition staton_bus_syntax0_generic (x r u : string)
+    (rx : infer (r != x)) (Rx : infer (u != x))
+    (ur : infer (u != r)) (xr : infer (x != r))
+    (xu : infer (x != u)) (ru : infer (r != u)) : @exp R P [::] _ :=
+  [let x := Sample {exp_bernoulli (2 / 7%:R)%:nng p27} in
+   let r := if #x then return {3}:R else return {10}:R in
+   let u := Score {exp_poisson 4 [#r]} in
+   return #x].
+
+Fail Definition staton_bus_syntax0_generic' (x r u : string)
+    (rx : infer (r != x)) (Rx : infer (u != x))
+    (ur : infer (u != r)) (xr : infer (x != r))
+    (xu : infer (x != u)) (ru : infer (r != u)) : @exp R P [::] _ :=
+  [let x := Sample {exp_bernoulli (2 / 7%:R)%:nng p27} in
+   let r := if $x then return {3}:R else return {10}:R in
+   let u := Score {exp_poisson 4 [$r]} in
+   return $x].
+
+Fail Definition staton_bus_syntax0' : @exp R _ [::] _ :=
+  [let "x" := Sample {exp_bernoulli (2 / 7%:R)%:nng p27} in
+   let "r" := if ${"x"} then return {3}:R else return {10}:R in
+   let "_" := Score {exp_poisson 4 [${"r"}]} in
+   return ${"x"}].
+
 Definition staton_bus_syntax0 : @exp R _ [::] _ :=
   [let "x" := Sample {exp_bernoulli (2 / 7%:R)%:nng p27} in
    let "r" := if #{"x"} then return {3}:R else return {10}:R in
    let "_" := Score {exp_poisson 4 [#{"r"}]} in
    return #{"x"}].
 
+End tests.
+
 Definition staton_bus_syntax := [Normalize {staton_bus_syntax0}].
 
 Let sample_bern : R.-sfker munit ~> mbool := sample_cst (bernoulli p27).
@@ -558,8 +601,8 @@ by rewrite exp_var'E (execD_var_erefl "x") /=; congr ret.
 Qed.
 
 Lemma exec_staton_bus : execD staton_bus_syntax =
-  existT _ (normalize kstaton_bus' point) (measurable_fun_mnormalize _).
-Proof. by rewrite execD_normalize exec_staton_bus0'. Qed.
+  existT _ (normalize_pt kstaton_bus') (measurable_normalize_pt _).
+Proof. by rewrite execD_normalize_pt exec_staton_bus0'. Qed.
 
 Let poisson4 := @poisson R 4%N.
 
@@ -662,8 +705,8 @@ by rewrite exp_var'E (execD_var_erefl "x") /=; congr ret.
 Qed.
 
 Lemma exec_statonA_bus : execD staton_busA_syntax =
-  existT _ (normalize kstaton_busA' point) (measurable_fun_mnormalize _).
-Proof. by rewrite execD_normalize exec_staton_busA0'. Qed.
+  existT _ (normalize_pt kstaton_busA') (measurable_normalize_pt _).
+Proof. by rewrite execD_normalize_pt exec_staton_busA0'. Qed.
 
 (* equivalence between staton_bus and staton_busA *)
 Lemma staton_bus_staton_busA :
@@ -709,8 +752,6 @@ Section letinC.
 Local Open Scope lang_scope.
 Variable (R : realType).
 
-Require Import Classical_Prop.
-
 Lemma letinC g t1 t2 (e1 : @exp R P g t1) (e2 : exp P g t2)
   (x y : string)
   (xy : infer (x != y)) (yx : infer (y != x))

theories/measure.v

@@ -100,15 +100,16 @@ From HB Require Import structures.
 (*                            The HB class is FiniteMeasure.                  *)
 (*      SigmaFinite_isFinite == mixin for finite measures                     *)
 (*          Measure_isFinite == factory for finite measures                   *)
-(*       subprobability T R == subprobability measure over the measurableType *)
-(*                            T with values in \bar R with R : realType       *)
+(*        subprobability T R == subprobability measure over the               *)
+(*                            measurableType T with values in \bar R with     *)
+(*                            R : realType                                    *)
 (*                            The HB class is SubProbability.                 *)
-(*         probability T R == probability measure over the measurableType T   *)
+(*           probability T R == probability measure over the measurableType T *)
 (*                            with values in \bar with R : realType           *)
 (*               probability == type of probability measures                  *)
 (*                            The HB class is Probability.                    *)
 (*     Measure_isProbability == factor for probability measures               *)
-(*              mnormalize mu == normalization of a measure to a probability  *)
+(*             mnormalize mu == normalization of a measure to a probability   *)
 (* {outer_measure set T -> \bar R} == type of an outer measure over sets      *)
 (*                            of elements of type T : Type where R is         *)
 (*                            expected to be a numFieldType                   *)