fix after rebase

Author: affeldt-aist

theories/lang_syntax.v

@@ -151,7 +151,7 @@ move/left_right_continuousP.
 apply/not_andP; left.
 move/(@cvgrPdist_le _ R^o).
 apply/existsNP.
-exists (2%:R^-1)%R.
+exists 2%:R^-1%R.
 rewrite not_implyE; split; first by rewrite invr_gt0.
 move=> [e /= e0].
 move/(_ (-(e / 2))%R).
@@ -690,7 +690,7 @@ split.
   exact: exprn_continuous.
 Qed.
 
-Lemma derive_onemXn {R : realType} (n : nat) x :
+Lemma derive_onemXn {R : realType} n x :
   ((fun y : R => `1-y ^+ n.+1 : R^o)^`() x = - n.+1%:R * `1-x ^+ n)%R.
 Proof.
 rewrite (@derive1_comp _ (@onem R) (fun x => GRing.exp x n.+1))//; last first.
@@ -700,7 +700,8 @@ by rewrite -derive1E derive1_cst derive_id sub0r mulrN1 [in RHS]mulNr.
 Qed.
 
 Lemma integral_onemXn {R : realType} n :
-  fine (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (`1-x ^+ n)%:E) = n.+1%:R^-1%R :> R.
+  fine (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (`1-x ^+ n)%:E)
+  = (n.+1%:R^-1)%R :> R.
 Proof.
 rewrite (@continuous_FTC2 _ _ (fun x : R => ((1 - x) ^+ n.+1 / - n.+1%:R))%R)//=.
 - rewrite subrr subr0 expr0n/= mul0r expr1n mul1r sub0r.
@@ -723,7 +724,7 @@ exact: continuous_XMonemX.
 Qed.
 
 Lemma Rintegral_onemXn {R : realType} n :
-  (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (`1-x ^+ n))%R = n.+1%:R^-1%R :> R.
+  (\int[lebesgue_measure]_(x in `[0%R, 1%R]) (`1-x ^+ n) = n.+1%:R^-1 :> R)%R.
 Proof.
 rewrite /Rintegral.
 rewrite (@continuous_FTC2 _ _ (fun x : R => ((1 - x) ^+ n.+1 / - n.+1%:R))%R)//=.

theories/lang_syntax_table_game.v

@@ -214,13 +214,13 @@ Definition prog0 : @exp R _ [::] _ :=
   return {1}:N <= #{"y"}].
 
 Definition tail1 : @exp R _ [:: ("_", Unit); ("x", Nat) ; ("p", Real)] _ :=
-  [Sample {exp_bernoulli [{1}:R - {[{1}:R - #{"p"}]} ^+ {3}]}].
+  [Sample {exp_bernoulli [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%R}]}].
 
 Definition tail2 : @exp R _ [:: ("_", Unit); ("p", Real)] _ :=
-  [Sample {exp_bernoulli [{1}:R - {[{1}:R - #{"p"}]} ^+ {3}]}].
+  [Sample {exp_bernoulli [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%R}]}].
 
 Definition tail3 : @exp R _ [:: ("p", Real); ("_", Unit)] _ :=
-  [Sample {exp_bernoulli [{1}:R - {[{1}:R - #{"p"}]} ^+ {3}]}].
+  [Sample {exp_bernoulli [{1}:R - {[{1}:R - #{"p"}]} ^+ {3%R}]}].
 
 Definition prog1 : @exp R _ [::] _ :=
  [Normalize
@@ -233,14 +233,14 @@ Definition prog2 : @exp R _ [::] _ :=
  [Normalize
   let "p" := Sample {exp_uniform 0 1 (@ltr01 R)} in
   let "_" :=
-    Score {[{56}:R * #{"p"} ^+ {5} * {[{1}:R - #{"p"}]} ^+ {3}]} in
+    Score {[{56}:R * #{"p"} ^+ {5%R} * {[{1}:R - #{"p"}]} ^+ {3%R}]} in
   {tail2}].
 
 Definition prog2' : @exp R _ [::] _ :=
  [Normalize
   let "p" := Sample {exp_beta 1 1} in
   let "_" := Score
-    {[{56}:R * #{"p"} ^+ {5} * {[{1}:R - #{"p"}]} ^+ {3}]} in
+    {[{56}:R * #{"p"} ^+ {5%R} * {[{1}:R - #{"p"}]} ^+ {3%R}]} in
   {tail2}].
 
 Definition prog3 : @exp R _ [::] _ :=
@@ -377,7 +377,7 @@ rewrite execD_pow/=.
 rewrite (@execD_bin _ _ binop_minus)/=/=.
 rewrite 2!execD_real/=.
 rewrite (execD_var_erefl "p")/=.
-rewrite -(mulrA 56).
+rewrite -(mulrA 56%R).
 exact: prog12_subproof.
 Qed.
 
@@ -504,7 +504,7 @@ rewrite /beta_pdf /XMonemX01 2!patchE; case: ifPn => [y01|_]; last first.
 rewrite ger0_norm; last first.
   by rewrite mulr_ge0// XMonemX_ge0//; rewrite inE in y01.
 rewrite [X in _ = _ * X]EFinM [in RHS]muleCA.
-rewrite /= XMonemX00 mul1r [in LHS](mulrC 56) [in LHS]EFinM -[in LHS]muleA; congr *%E.
+rewrite /= XMonemX00 mul1r [in LHS](mulrC 56%R) [in LHS]EFinM -[in LHS]muleA; congr *%E.
 by rewrite !betafunE/=; repeat rewrite !factE/=; rewrite -EFinM; congr EFin; lra.
 
 Qed.

theories/prob_lang.v

@@ -1647,7 +1647,7 @@ Definition sample_and_branch : R.-sfker T ~> _ :=
     (ite macc1of2 (ret (@k3 _ _ R)) (ret k10)).
 
 Lemma sample_and_branchE t U : sample_and_branch t U =
-  (2 / 7)%:E * \d_(3 : R) U + (5 / 7)%:E * \d_(10 : R) U.
+  (2 / 7)%:E * \d_(3%R : R) U + (5 / 7)%:E * \d_(10%R : R) U.
 Proof.
 rewrite /sample_and_branch letin_sample_bernoulli/=; last lra.
 by rewrite !iteE/= onem27.

theories/prob_lang_wip.v

@@ -92,7 +92,7 @@ Import Notations.
 Hypothesis integral_poisson_density : forall k,
   (\int[mu]_x (@poisson_pdf R k x)%:E = 1%E)%E.
 
-Let f1 x := ((poisson1 (x : R)) ^-1)%R.
+Let f1 x := ((poisson1 (x : R))^-1)%R.
 
 Let mf1 : measurable_fun setT f1.
 rewrite /f1 /poisson1 /poisson_pdf.