From 4f18d51596926cb7ea6fb4ef08f83f6a1ffd32ad Mon Sep 17 00:00:00 2001 From: Takafumi Saikawa Date: Sat, 8 Feb 2025 05:55:02 +0900 Subject: [PATCH] gcm and altprob --- theories/core/hierarchy.v | 2 +- theories/lib/proba_lib.v | 3 +- theories/lib/typed_store_lib.v | 3 - theories/models/altprob_model.v | 112 ++++++++++++++-------------- theories/models/gcm_model.v | 13 ++-- theories/models/proba_monad_model.v | 2 +- 6 files changed, 65 insertions(+), 70 deletions(-) diff --git a/theories/core/hierarchy.v b/theories/core/hierarchy.v index 1f4e98b..9138846 100644 --- 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 index 557ed4d..1403023 100644 --- 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 index 0587cb8..3ffa14f 100644 --- 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 index c6fac0f..3e5de45 100644 --- 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,7 +110,7 @@ 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. @@ -119,50 +118,50 @@ 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 index 4856fac..640dc17 100644 --- 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 index e910030..491af5d 100644 --- 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.