a temporary measure for overflow

theories/lang_syntax_examples.v

@@ -1,5 +1,5 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
-From Coq Require Import String.
+From Stdlib Require Import String.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp.classical Require Import unstable mathcomp_extra boolp.
@@ -68,6 +68,8 @@ Local Open Scope lang_scope.
 
 Local Close Scope lang_scope.
 
+Local Open Scope string_scope.
+
 (* simple tests to check bidirectional hints *)
 Module bidi_tests.
 Section bidi_tests.
@@ -695,9 +697,17 @@ transitivity (beta_prob_bernoulli_prob 6 4 1 0 U : \bar R).
 rewrite beta_prob_bernoulli_probE// !bernoulli_probE//=; last 2 first.
   lra.
   by rewrite div_beta_fun_ge0 div_beta_fun_le1.
-by congr (_ * _ + _ * _)%:E;
-  rewrite /div_beta_fun/= /onem !beta_funE/= !factE/= !factE; field.
+ (* temporary measure to avoid stack overflow *)
+suff : div_beta_fun 6 4 1 0 = 3 / 5 :> R by move->.
+rewrite /div_beta_fun/= /onem !beta_funE/=.
+rewrite 2!addn0 invfM mulrCA invrK addn1 8!addnS 2!addn0.
+by rewrite (factS 9) !factS fact0; field.
+Qed.
+(*
+congr (_ * _ + _ * _)%:E.
+rewrite !factE/= !factE; field.
 Qed.
+*)
 
 End beta_bernoulli_bernoulli.
 

theories/lang_syntax_noisy.v

@@ -1,4 +1,4 @@
-From Coq Require Import String.
+From Stdlib 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.
@@ -39,7 +39,7 @@ Import numFieldTopology.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 Local Open Scope ereal_scope.
-
+Local Open Scope string_scope.
 (* TODO: PR *)
 Section ge0_bounded_measurable_probability_integrable.
 Context d {T : measurableType d} {R : realType} {p : probability T R}

theories/lang_syntax_table_game.v

@@ -1,5 +1,5 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
-Require Import String.
+From Stdlib Require Import String.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
 From mathcomp Require Import ring lra.
@@ -40,6 +40,7 @@ Import numFieldTopology.Exports.
 
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
+Local Open Scope string_scope.
 
 Section execP_letin_uniform.
 Local Open Scope ereal_scope.
@@ -569,7 +570,15 @@ under eq_integral.
   rewrite /XMonemX01 patchE x0 XMonemX0.
   over.
 rewrite /= => ->; congr bernoulli_prob.
-by rewrite /div_beta_fun addn0 !beta_funE/= !factE/= ?factE; field.
+rewrite /div_beta_fun addn0 !beta_funE/=.
+(* temporary measure to avoid stack overflow *)
+rewrite mulrAC -mulrA mulrAC 2!invfM 3!mulrA mulfV ?gt_eqF// 2!div1r.
+rewrite 17!addnS 2!addn0.
+rewrite (factS 11) (factS 10) (factS 9).
+by rewrite !factE; field.
+(*
+rewrite !factE/= ?factE; field.
+*)
 Qed.
 
 Lemma dirac_bool {R : realType} (U : set bool) :

theories/lang_syntax_toy.v

@@ -1,5 +1,5 @@
 (* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C.              *)
-From Coq Require Import String Classical.
+From Stdlib Require Import String Classical.
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg.
 From mathcomp Require Import mathcomp_extra boolp.
@@ -33,6 +33,7 @@ Import numFieldTopology.Exports.
 Local Open Scope classical_set_scope.
 Local Open Scope ring_scope.
 Local Open Scope ereal_scope.
+Local Open Scope string_scope.
 
 Section type.
 Variables (R : realType).

theories/probability.v

@@ -2584,7 +2584,7 @@ case: a => [|a].
   by rewrite beta_fun00 eqxx ltnn/= fact0 mul1r divr1.
 case: b => [|b].
   by rewrite beta_fun_sym beta_fun0// fact0 addn0/= mulr1 divff.
-by rewrite beta_fun_fact/= natrM// -addnE addnS.
+by rewrite beta_fun_fact/= natrM// addnS.
 Qed.
 
 Lemma beta_fun_gt0 a b : 0 < beta_fun a b :> R.