gcm and altprob

affeldt-aist · Feb 7, 2025 · 4f18d51 · 4f18d51
1 parent a872f0b
commit 4f18d51
Show file tree

Hide file tree

Showing 6 changed files with 65 additions and 70 deletions.
diff --git a/theories/core/hierarchy.v b/theories/core/hierarchy.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 Ltac typeof X := type of X.
 
-Require Import ssrmatching Reals JMeq.
+Require Import ssrmatching JMeq.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require boolp.
 From mathcomp Require Import mathcomp_extra reals.

diff --git a/theories/lib/proba_lib.v b/theories/lib/proba_lib.v
@@ -3,7 +3,7 @@
 From HB Require Import structures.
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require boolp.
-From mathcomp Require Import reals mathcomp_extra Rstruct lra ring.
+From mathcomp Require Import reals mathcomp_extra lra ring.
 From infotheo Require Import realType_ext.
 From infotheo Require Import proba convex necset.
 From infotheo Require Import fdist.
@@ -328,7 +328,6 @@ Qed.
 Section arbcoin_spec_convexity.
 Local Open Scope latt_scope.
 Local Open Scope convex_scope.
-Local Open Scope R_scope.
 
 (* TODO? : move magnified_weight to infotheo.convex *)
 Lemma magnified_weight_proof (p q r : {prob R}) :

diff --git a/theories/lib/typed_store_lib.v b/theories/lib/typed_store_lib.v
@@ -1,8 +1,5 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2023 monae authors, license: LGPL-2.1-or-later               *)
-Ltac typeof X := type of X.
-
-Require Import ssrmatching Reals JMeq.
 From mathcomp Require Import all_ssreflect.
 From mathcomp Require boolp.
 Require Import preamble hierarchy.

diff --git a/theories/models/altprob_model.v b/theories/models/altprob_model.v
@@ -1,12 +1,8 @@
 (* monae: Monadic equational reasoning in Coq                                 *)
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
-Require Import Reals.
 From mathcomp Require Import all_ssreflect ssralg ssrnum finmap.
-From mathcomp Require Import boolp classical_sets.
-From mathcomp Require Import reals Rstruct.
-From infotheo Require Import classical_sets_ext Reals_ext ssrR fdist.
-From infotheo Require Import ssrR Reals_ext proba.
-From infotheo Require Import Reals_ext realType_ext.
+From mathcomp Require Import boolp classical_sets reals.
+From infotheo Require Import classical_sets_ext realType_ext fdist proba.
 From infotheo Require Import fsdist convex necset.
 Require category.
 From HB Require Import structures.
@@ -24,25 +20,28 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 Unset Printing Implicit Defensive.
 
+Import GRing.Theory.
+
 Local Open Scope proba_scope.
 Local Open Scope category_scope.
 
 Section P_delta_altProbMonad.
-Local Open Scope R_scope.
+Variable R : realType.
+Local Open Scope ring_scope.
 Local Open Scope reals_ext_scope.
 Local Open Scope classical_set_scope.
 Local Open Scope convex_scope.
 Local Open Scope latt_scope.
 Local Open Scope monae_scope.
 
-Definition alt A (x y : gcm A) : gcm A := x [+] y.
-Definition choice p A (x y : gcm A) : gcm A := x <| p |> y.
+Definition alt A (x y : gcm R A) : gcm R A := x [+] y.
+Definition choice p A (x y : gcm R A) : gcm R A := x <| p |> y.
 
 Lemma altA A : ssrfun.associative (@alt A).
 Proof. by move=> x y z; rewrite /alt lubA. Qed.
 
-Lemma image_fsdistmap A B (x : gcm A) (k : choice_of_Type A -> gcm B) :
-  fsdistmap k @` x = (gcm # k) x.
+Lemma image_fsdistmap A B (x : gcm R A) (k : choice_of_Type A -> gcm R B) :
+  fsdistmap k @` x = (gcm R # k) x.
 Proof.
 rewrite /hierarchy.actm/= /actm 5!FCompE /category.actm/=.
 by rewrite /free_semiCompSemiLattConvType_mor/=; unlock.
@@ -58,15 +57,15 @@ Local Notation UC := forget_choiceType.
 Local Notation U0 := forget_convType.
 Local Notation U1 := forget_semiCompSemiLattConvType.
 
-Lemma FunaltDr (A B : Type) (x y : gcm A) (k : A -> gcm B) :
-  (gcm # k) (x [+] y) = (gcm # k) x [+] (gcm # k) y.
+Lemma FunaltDr (A B : Type) (x y : gcm R A) (k : A -> gcm R B) :
+  (gcm R # k) (x [+] y) = (gcm R # k) x [+] (gcm R # k) y.
 Proof.
 rewrite /hierarchy.actm /= /Monad_of_category_monad.actm /=.
 by rewrite scsl_hom_is_lubmorph.
 Qed.
 
-Lemma FunpchoiceDr (A B : Type) (x y : gcm A) (k : A -> gcm B) p :
-  (gcm # k) (x <|p|> y) = (gcm # k) x <|p|> (gcm # k) y.
+Lemma FunpchoiceDr (A B : Type) (x y : gcm R A) (k : A -> gcm R B) p :
+  (gcm R # k) (x <|p|> y) = (gcm R # k) x <|p|> (gcm R # k) y.
 Proof.
 rewrite /hierarchy.actm /= /Monad_of_category_monad.actm /=.
 by rewrite scsl_hom_is_affine.
@@ -76,22 +75,22 @@ End funalt_funchoice.
 Section bindaltDl.
 Import category.
 Import comps_notation.
-Local Notation F1 := free_semiCompSemiLattConvType.
-Local Notation F0 := free_convType.
+Local Notation F1 := (free_semiCompSemiLattConvType R).
+Local Notation F0 := (free_convType R).
 Local Notation FC := free_choiceType.
 Local Notation UC := forget_choiceType.
-Local Notation U0 := forget_convType.
-Local Notation U1 := forget_semiCompSemiLattConvType.
+Local Notation U0 := (forget_convType R).
+Local Notation U1 := (forget_semiCompSemiLattConvType R).
 
-Lemma affine_F1e0U1PD_alt T (u v : gcm (gcm T)) :
-  (F1 # eps0 (U1 (P_delta_left T)))%category (u [+] v) =
-  (F1 # eps0 (U1 (P_delta_left T)))%category u [+]
-  (F1 # eps0 (U1 (P_delta_left T)))%category v.
+Lemma affine_F1e0U1PD_alt T (u v : gcm R (gcm R T)) :
+  (F1 # eps0 R (U1 (P_delta_left R T)))%category (u [+] v) =
+  (F1 # eps0 R (U1 (P_delta_left R T)))%category u [+]
+  (F1 # eps0 R (U1 (P_delta_left R T)))%category v.
 Proof. exact: scsl_hom_is_lubmorph. Qed.
 
-Lemma affine_e1PD_alt T (x y : el (F1 (FId (U1 (P_delta_left T))))) :
-  (eps1 (P_delta_left T)) (x [+] y) =
-  (eps1 (P_delta_left T)) x [+] (eps1 (P_delta_left T)) y.
+Lemma affine_e1PD_alt T (x y : el (F1 (FId (U1 (P_delta_left R T))))) :
+  (eps1 R (P_delta_left R T)) (x [+] y) =
+  (eps1 R (P_delta_left R T)) x [+] (eps1 R (P_delta_left R T)) y.
 Proof. exact: scsl_hom_is_lubmorph. Qed.
 
 (*
@@ -102,7 +101,7 @@ Local Notation FCo := choice_of_Type.
 Local Notation F1m := free_semiCompSemiLattConvType_mor.
 Local Notation F0m := free_convType_mor.
 
-Lemma bindaltDl : BindLaws.left_distributive (@hierarchy.bind gcm) alt.
+Lemma bindaltDl : BindLaws.left_distributive (@hierarchy.bind (gcm R)) alt.
 Proof.
 move=> A B x y k.
 rewrite hierarchy.bindE /= /join_ -category.bindE.
@@ -111,58 +110,58 @@ Qed.
 End bindaltDl.
 
 HB.instance Definition _ :=
-  @isMonadAlt.Build (Monad_of_category_monad.acto Mgcm) alt altA bindaltDl.
+  @isMonadAlt.Build (Monad_of_category_monad.acto (Mgcm R)) alt altA bindaltDl.
 
 Lemma altxx A : idempotent_op (@alt A).
 Proof. by move=> x; rewrite /= /alt lubxx. Qed.
 Lemma altC A : commutative (@alt A).
 Proof. by move=> a b; rewrite /= /alt /= lubC. Qed.
 
 HB.instance Definition _ :=
-  @isMonadAltCI.Build (Monad_of_category_monad.acto Mgcm) altxx altC.
+  @isMonadAltCI.Build (Monad_of_category_monad.acto (Mgcm R)) altxx altC.
 
-Definition gcmACI := [the altCIMonad of gcm].
+Definition gcmACI := [the altCIMonad of gcm R].
 
-Lemma choice1 A (x y : gcm A) : x <| 1%:pr |> y = x.
+Lemma choice1 A (x y : gcm R A) : x <| 1%:pr |> y = x.
 Proof. by rewrite conv1. Qed.
-Lemma choiceC A p (x y : gcm A) : x <|p|> y = y <|(Prob.p p).~%:pr|> x.
+Lemma choiceC A p (x y : gcm R A) : x <|p|> y = y <|(Prob.p p).~%:pr|> x.
 Proof. by rewrite convC. Qed.
 Lemma choicemm A p : idempotent_op (@choice p A).
 Proof. by move=> m; rewrite /choice convmm. Qed.
 
-Let choiceA A (p q r s : {prob R}) (x y z : gcm A) :
+Let choiceA A (p q r s : {prob R}) (x y z : gcm R A) :
   x <| p |> (y <| q |> z) = (x <| [r_of p, q] |> y) <| [s_of p, q] |> z.
 Proof. exact: convA. Qed.
 
 Section bindchoiceDl.
 Import category.
 Import comps_notation.
-Local Notation F1 := free_semiCompSemiLattConvType.
-Local Notation F0 := free_convType.
+Local Notation F1 := (free_semiCompSemiLattConvType R).
+Local Notation F0 := (free_convType R).
 Local Notation FC := free_choiceType.
 Local Notation UC := forget_choiceType.
-Local Notation U0 := forget_convType.
-Local Notation U1 := forget_semiCompSemiLattConvType.
+Local Notation U0 := (forget_convType R).
+Local Notation U1 := (forget_semiCompSemiLattConvType R).
 
-Lemma affine_F1e0U1PD_conv T (u v : gcm (gcm T)) p :
-  ((F1 # eps0 (U1 (P_delta_left T))) (u <|p|> v) =
-   (F1 # eps0 (U1 (P_delta_left T))) u <|p|>
-   (F1 # eps0 (U1 (P_delta_left T))) v)%category.
+Lemma affine_F1e0U1PD_conv T (u v : gcm R (gcm R T)) p :
+  ((F1 # eps0 R (U1 (P_delta_left R T))) (u <|p|> v) =
+   (F1 # eps0 R (U1 (P_delta_left R T))) u <|p|>
+   (F1 # eps0 R (U1 (P_delta_left R T))) v)%category.
 Proof. exact: scsl_hom_is_affine. Qed.
 
-Lemma affine_e1PD_conv T (x y : el (F1 (FId (U1 (P_delta_left T))))) p :
-  (eps1 (P_delta_left T)) (x <|p|> y) =
-  (eps1 (P_delta_left T)) x <|p|> (eps1 (P_delta_left T)) y.
+Lemma affine_e1PD_conv T (x y : el (F1 (FId (U1 (P_delta_left R T))))) p :
+  (eps1 R (P_delta_left R T)) (x <|p|> y) =
+  (eps1 R (P_delta_left R T)) x <|p|> (eps1 R (P_delta_left R T)) y.
 Proof. exact: scsl_hom_is_affine. Qed.
 
 (*Local Notation F1o := necset_semiCompSemiLattConvType.*)
 Local Notation F0o := FSDist.t.
 Local Notation FCo := choice_of_Type.
-Local Notation F1m := free_semiCompSemiLattConvType_mor.
-Local Notation F0m := free_convType_mor.
+Local Notation F1m := (@free_semiCompSemiLattConvType_mor R).
+Local Notation F0m := (@free_convType_mor R).
 
 Lemma bindchoiceDl p :
-  BindLaws.left_distributive (@hierarchy.bind gcm) (@choice p).
+  BindLaws.left_distributive (@hierarchy.bind (gcm R)) (@choice p).
 Proof.
 move=> A B x y k.
 rewrite hierarchy.bindE /= /join_ -category.bindE.
@@ -172,24 +171,25 @@ Qed.
 End bindchoiceDl.
 
 HB.instance Definition _ :=
-  isMonadConvex.Build R (Monad_of_category_monad.acto Mgcm)
+  isMonadConvex.Build R (Monad_of_category_monad.acto (Mgcm R))
     choice1 choiceC choicemm choiceA.
 
 HB.instance Definition _ :=
-  isMonadProb.Build R (Monad_of_category_monad.acto Mgcm) bindchoiceDl.
+  isMonadProb.Build R (Monad_of_category_monad.acto (Mgcm R)) bindchoiceDl.
 
 Lemma choicealtDr A (p : {prob R}) :
-  right_distributive (fun x y : Mgcm A => x <| p |> y) (@alt A).
+  right_distributive (fun x y : Mgcm R A => x <| p |> y) (@alt A).
 Proof. by move=> x y z; rewrite /choice lubDr. Qed.
 
 HB.instance Definition _ :=
-  @isMonadAltProb.Build R (Monad_of_category_monad.acto Mgcm) choicealtDr.
+  @isMonadAltProb.Build R (Monad_of_category_monad.acto (Mgcm R)) choicealtDr.
 
-Definition gcmAP := [the altProbMonad R of gcm].
+Definition gcmAP := [the altProbMonad R of gcm R].
 
 End P_delta_altProbMonad.
 
 Section probabilisctic_choice_not_trivial.
+Variable R : realType.
 Local Open Scope proba_monad_scope.
 
 (* An example that probabilistic choice in this model is not trivial:
@@ -198,14 +198,14 @@ Example gcmAP_choice_nontrivial (p q : {prob R}) :
   p <> q ->
   (* Ret = hierarchy.ret *)
   Ret true <|p|> Ret false <>
-  Ret true <|q|> Ret false :> (Monad_of_category_monad.acto Mgcm) bool.
+  Ret true <|q|> Ret false :> (Monad_of_category_monad.acto (Mgcm R)) bool.
 Proof.
 apply contra_not.
-rewrite !gcm_retE /hierarchy.choice => /(congr1 (@NECSet.sort _)).
+rewrite !gcm_retE /hierarchy.choice => /(congr1 (@NECSet.sort _ _)).
 rewrite /= !necset_convType.convE !conv_cset1 /=.
-move/(@set1_inj _ (conv _ _ _))/(congr1 (@FSDist.f _))/fsfunP/(_ true).
+move/(@set1_inj _ (conv _ _ _))/(congr1 (@FSDist.f _ _))/fsfunP/(_ true).
 rewrite !fsdist_convE !fsdist1xx !fsdist10//; last exact/eqP. (*TODO: we should not need that*)
-by rewrite !avgRE !mulR1 ?mulR0 ?addR0 => /val_inj.
+by rewrite !avgRE !mulr1 ?mulr0 ?addr0 => /val_inj.
 Qed.
 
 End probabilisctic_choice_not_trivial.
diff --git a/theories/models/gcm_model.v b/theories/models/gcm_model.v
@@ -721,8 +721,6 @@ Variables (T : Type) (X : gcm (gcm T)).
 Import category.
 Local Open Scope convex_scope.
 
-STOP
-
 Lemma gcm_joinE : Join X = necset_join X.
 Proof.
 apply/necset_ext.
@@ -733,7 +731,7 @@ set E := epsC _; have->: E = [hom idfun] by apply/hom_ext; rewrite epsCE.
 rewrite functor_id_hom.
 rewrite !functor_o functor_id !compfid.
 set F1J := F1 # _.
-have-> : F1J = @necset_join.F1join0 _ :> (_ -> _).
+have-> : F1J = @necset_join.F1join0 _ _ :> (_ -> _).
 - apply funext=> x; apply necset_ext=> /=.
   rewrite /F1J /= /necset_join.F1join0' /=.
   cbn.
@@ -749,19 +747,20 @@ End P_delta_category_monad.
 Require proba_monad_model.
 
 Section probMonad_out_of_F0U0.
+Variable R : realType.
 Import category.
 (* probability monad built directly *)
 Definition M := proba_monad_model.MonadProbModel.t.
 (* probability monad built using adjunctions *)
 Definition N := [the hierarchy.Monad.Exports.monad of
-  Monad_of_category_monad.acto (Monad_of_adjoint_functors Aprob)].
+  Monad_of_category_monad.acto (Monad_of_adjoint_functors (Aprob R))].
 
-Lemma actmE T : N T = M T. Proof. by []. Qed.
+Lemma actmE T : N T = M R T. Proof. by []. Qed.
 
 Import comps_notation hierarchy.
 Local Open Scope monae_scope.
 
-Lemma JoinE T : (Join : (N \o N) T -> N T) = (Join : (M \o M) T -> M T).
+Lemma JoinE T : (Join : (N \o N) T -> N T) = (Join : (M R \o M R) T -> M R T).
 Proof.
 apply funext => t /=.
 rewrite /join_.
@@ -774,7 +773,7 @@ congr fsdistbind.
 by apply funext => x; rewrite fsdist1bind.
 Qed.
 
-Lemma RetE T : (Ret : idfun T -> N T) = (Ret : FId T -> M T).
+Lemma RetE T : (Ret : idfun T -> N T) = (Ret : FId T -> M R T).
 Proof.
 apply funext => t /=.
 rewrite /ret_.

diff --git a/theories/models/proba_monad_model.v b/theories/models/proba_monad_model.v
@@ -2,7 +2,7 @@
 (* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later               *)
 From mathcomp Require Import all_ssreflect ssralg ssrnum.
 From mathcomp Require boolp.
-From mathcomp Require Import mathcomp_extra reals Rstruct.
+From mathcomp Require Import mathcomp_extra reals.
 From infotheo Require Import realType_ext ssr_ext fsdist.
 From infotheo Require Import convex.
 From HB Require Import structures.