From d5f3a6507bfac388e93b3625752a1a87b1b6f2f1 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 21 Apr 2022 17:53:33 +0900 Subject: [PATCH] use the short facility of HB - remove type-in-type versions of lifting files --- Makefile | 11 - category.v | 2 +- coq-monae.opam | 4 +- fmt_lifting.v | 723 --------------------------------- gcm_model.v | 7 +- hierarchy.v | 405 +++++++++--------- impredicative_set/ihierarchy.v | 355 ++++++++-------- meta.yml | 4 +- parametricity_codensity.v | 223 ---------- 9 files changed, 372 insertions(+), 1362 deletions(-) delete mode 100644 fmt_lifting.v delete mode 100644 parametricity_codensity.v diff --git a/Makefile b/Makefile index c568eaf6..39518935 100644 --- a/Makefile +++ b/Makefile @@ -21,14 +21,3 @@ _CoqProject Makefile: ; install_full: all $(MAKE) install $(MAKE) -C impredicative_set install - -# This last entry is only to support work-in-progress. - -COQ5 = coqc -w -notation-overridden -R . monae - -sect5: all - $(COQ5) fmt_lifting.v - $(COQ5) parametricity_codensity.v - -clean5: - rm -f *.vo *.glob *.vok *.vos diff --git a/category.v b/category.v index 38c15690..07e98674 100644 --- a/category.v +++ b/category.v @@ -1124,7 +1124,7 @@ Require Import hierarchy. Module Monad_of_category_monad. Section monad_of_category_monad. -Variable M : Monad.Exports.monad CT. +Variable M : category.Monad.Exports.monad CT. Definition acto : Type -> Type := M. diff --git a/coq-monae.opam b/coq-monae.opam index c0466865..e7bece02 100644 --- a/coq-monae.opam +++ b/coq-monae.opam @@ -25,9 +25,9 @@ depends: [ "coq-mathcomp-solvable" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-field" { (>= "1.13.0" & < "1.15~") | (= "dev") } "coq-mathcomp-analysis" { (>= "0.3.11" & < "0.4~") } - "coq-infotheo" { >= "0.3.5" & < "0.4~"} + "coq-infotheo" { >= "0.3.7" & < "0.4~"} "coq-paramcoq" { >= "1.1.3" & < "1.2~" } - "coq-hierarchy-builder" { >= "1.1.0" } + "coq-hierarchy-builder" { >= "1.2.0" } "coq-equations" { >= "1.3" & < "1.4~" } ] diff --git a/fmt_lifting.v b/fmt_lifting.v deleted file mode 100644 index 989b60da..00000000 --- a/fmt_lifting.v +++ /dev/null @@ -1,723 +0,0 @@ -(* monae: Monadic equational reasoning in Coq *) -(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect. -From mathcomp Require boolp. -From HB Require Import structures. -Require Import monae_lib hierarchy monad_lib monad_transformer. - -(******************************************************************************) -(* Uniform Lifting of Sigma-operations Along Functorial Monad Transformers *) -(* *) -(* This file corresponds to the formalization of [Mauro Jaskelioff, *) -(* Modular Monad Transformers, ESOP 2009] (from Sect. 5, definition 23). *) -(* *) -(* codensityT == codensity monad transformer *) -(* slifting == definition of a sigma-operation using a *) -(* sigma-operation and a functorial monad *) -(* transformer *) -(* uniform_sigma_lifting == Theorem: given a functorial monad transformer t, *) -(* slifting is a lifting along Lift t *) -(* slifting_stateT == lifting of a sigma-operation along stateT *) -(* slifting_exceptT == lifting of a sigma-operation along exceptT *) -(* slifting_envT == lifting of a sigma-operation along envT *) -(* slifting_outputT == lifting of a sigma-operation along outputT *) -(* slifting_alifting_* == Lemmas: slifting and alifting of algebraic *) -(* operations coincide *) -(* local_*E == Lemmas: liftings of local *) -(* handle_*E == Lemmas: liftings of handle *) -(* flush_*E == Lemmas: liftings of flush *) -(* *) -(* WARNING: *) -(* Do `make sect5` to compile it, `make clean5` to clean it. Unlike the rest *) -(* of monae, it requires some form of impredicativity. That is why this file *) -(* uses Unset/Set Universe Checking. See the directory impredicative_set for *) -(* a version where this check isn't disabled. *) -(******************************************************************************) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Local Open Scope monae_scope. - -Definition MK (m : UU0 -> UU0) (A : UU0) := forall (B : UU0), (A -> m B) -> m B. - -Section codensity. -Variable (M : monad). - -Definition retK : FId ~~> MK M := - fun (A : UU0) (a : A) (B : UU0) (k : A -> M B) => k a. - -Definition bindK (A B : UU0) (m : MK M A) f : MK M B := - fun (C : UU0) (k : B -> M C) => m C (fun a : A => (f a) C k). - -Definition MK_map (A B : UU0) (f : A -> B) (m : MK M A) : MK M B := - fun (C : UU0) (k : B -> M C) => m C (fun a : A => k (f a)). - -Let MK_map_i : FunctorLaws.id MK_map. -Proof. -move=> A; rewrite /MK_map; apply boolp.funext => m /=. -by apply funext_dep => B; exact: boolp.funext. -Qed. - -Let MK_map_o : FunctorLaws.comp MK_map. Proof. by []. Qed. - -HB.instance Definition _ := isFunctor.Build (MK M) MK_map_i MK_map_o. - -Let naturality_retK : naturality FId [the functor of MK M] retK. -Proof. -move=> A B h; rewrite /actm /= /MK_map /retK /=. -by apply boolp.funext => a /=; exact: funext_dep. -Qed. - -HB.instance Definition _ := isNatural.Build - _ [the functor of MK M] retK naturality_retK. - -Let left_neutral : BindLaws.left_neutral bindK retK. -Proof. -by move=> A B a f; rewrite /bindK /=; apply funext_dep => C; exact: boolp.funext. -Qed. - -Let right_neutral : BindLaws.right_neutral bindK retK. -Proof. -by move=> A m; rewrite /bindK /retK; apply funext_dep => C; exact: boolp.funext. -Qed. - -Let associative : BindLaws.associative bindK. -Proof. by move=> A B C m f g; rewrite /bindK; exact: funext_dep. Qed. - -Lemma fmapE (A B : UU0) (f : A -> B) (m : MK M A) : - ([the functor of MK M] # f) m = bindK m (@retK _ \o f). -Proof. by []. Qed. - -HB.instance Definition _ := @Monad_of_ret_bind.Build - (MK M) [the _ ~> _ of retK] bindK fmapE left_neutral right_neutral associative. - -Definition liftK : M ~~> MK M := - fun (A : UU0) (m : M A) (B : UU0) (k : A -> M B) => m >>= k. - -Let retliftK : MonadMLaws.ret liftK. -Proof. -move=> A; rewrite /liftK/= /retK/=; apply boolp.funext => a. -by apply funext_dep => B /=; apply: boolp.funext => b; rewrite bindretf. -Qed. - -Let bindliftK : MonadMLaws.bind liftK. -Proof. -move=> A B m f; rewrite /liftK; apply funext_dep => C /=. -by apply boolp.funext => g; rewrite bindA. -Qed. - -HB.instance Definition _ := isMonadM_of_ret_bind.Build - M [the monad of MK M] liftK retliftK bindliftK. - -End codensity. - -Definition codensityT := fun M : monad => [the monad of MK M]. - -HB.instance Definition _ := - isMonadT.Build codensityT (fun M => [the monadM _ _ of @liftK M]). - -Unset Universe Checking. -Section kappa. -Variables (M : monad) (E : functor) (op : E.-operation M). - -Definition kappa' : E ~~> codensityT M := - fun (A : UU0) (s : E A) (B : UU0) (k : A -> M B) => - op B ((E # k) s). - -Lemma naturality_kappa' : naturality _ _ kappa'. -Proof. -move=> A B h; rewrite /kappa'; apply boolp.funext => ea; rewrite [in RHS]/=. -transitivity (fun B0 (k : B -> M B0) => op B0 ((E # (k \o h)) ea)) => //. -(*by apply funext_dep => C; apply boolp.funext => D; rewrite functor_o.*) -Qed. - -HB.instance Definition _ := isNatural.Build - _ (codensityT M) kappa' naturality_kappa'. - -Definition kappa := [the _ ~> _ of kappa']. - -Lemma kappaE X : kappa X = - fun (s : E X) (B : UU0) (k : X -> M B) => op B ((E # k) s). -Proof. by []. Qed. - -End kappa. - -Definition naturality_MK (M : functor) (A : UU0) (m : MK M A) := - naturality [the functor of exponential_F A \o M] M m. - -Section from. -Variables (M : monad). - -Definition from_component : codensityT M ~~> M := - fun (A : UU0) (c : codensityT M A) => c A Ret. - -Hypothesis naturality_MK : forall (A : UU0) (m : MK M A), - naturality_MK m. - -Lemma natural_from_component : naturality (codensityT M) M from_component. -Proof. -move=> A B h; apply boolp.funext => m /=. -rewrite [RHS](_ : _ = m B (Ret \o h)) //. (* by definition of from *) -(*rewrite -natural. -rewrite [LHS](_ : _ = (M # h \o m A) Ret) //. (* by definition of from *) -by rewrite naturality_MK.*) -Qed. - -HB.instance Definition _ := - isNatural.Build _ M from_component natural_from_component. - -Definition from := [the _ ~> _ of from_component]. - -Lemma from_component_liftK A : - @from_component A \o Lift [the monadT of codensityT] M A = id. -Proof. -by apply boolp.funext => m /=; rewrite /from_component/= /liftK /= bindmret. -Qed. - -End from. -Set Universe Checking. - -Section psi_kappa. -Variables (E : functor) (M : monad) (op : E.-operation M). - -Definition psik : E.-aoperation (codensityT M) := psi (kappa op). - -Lemma psikE (A : UU0) : op A = (@from_component M A) \o (@psik A) \o - ((E ## Lift [the monadT of codensityT] M) A). -Proof. -apply boolp.funext => m /=. -rewrite /from_component /psik /= /psi' /kappa' /fun_app_nt /=. -rewrite /bindK /=. -rewrite /join_of_bind. -rewrite -[in RHS]compE. -rewrite -[in RHS]compE. -rewrite -compA. -rewrite -functor_o. -rewrite from_component_liftK. -rewrite functor_id. -by rewrite compfid. -Qed. - -End psi_kappa. - -Section uniform_sigma_lifting. -Variables (E : functor) (M : monad) (op : E.-operation M) (t : fmt). -(*Hypothesis naturality_MK : forall (A : UU0) (m : MK M A), naturality_MK m.*) - -Let op1 : t (codensityT M) ~> t M := hmap t (from M). -Let op2 := alifting (psik op) (Lift t _). -Let op3 : [the functor of E \o t M] ~> [the functor of E \o t (codensityT M)] := - E ## hmap t (Lift [the monadT of codensityT] M). - -Definition slifting : E.-operation (t M) := op1 \v op2 \v op3. - -Theorem uniform_sigma_lifting : lifting_monadT op slifting. -Proof. -rewrite /lifting_monadT /slifting => X. -apply/esym. -transitivity ((op1 \v op2) X \o op3 X \o E # Lift t M X). - by rewrite (vassoc op1) vcompE/= !vcompE. -rewrite -compA. -transitivity ((op1 \v op2) X \o - ((E # Lift t (codensityT M) X) \o - (E # Lift [the monadT of codensityT] M X))). - congr (_ \o _); rewrite /op3. - by rewrite -functor_o -natural_hmap functor_app_naturalE -(@functor_o E). -transitivity (op1 X \o - (op2 X \o E # Lift t (codensityT M) X) \o E # Lift [the monadT of codensityT] M X). - by rewrite vcompE -compA. -rewrite -uniform_algebraic_lifting. -transitivity (Lift t M X \o from M (*naturality_MK*) X \o (psik op) X \o - E # Lift [the monadT of codensityT] M X). - congr (_ \o _). - by rewrite compA natural_hmap. -rewrite -2!compA. -congr (_ \o _). -by rewrite compA -psikE. -Qed. -End uniform_sigma_lifting. - -(* example 29 *) -Section slifting_instances. - -Variables (E : functor) (M : monad) (op : E.-operation M). -Hypothesis naturality_MK : forall (A : UU0) (m : MK M A), naturality_MK m. - -Section slifting_stateT. -Variable S : UU0. - -Let tau (X : UU0) s (f : S -> M (X * S)%type) := f s. - -Let op' : E \o stateT S M ~~> stateT S M := - fun (X : UU0) t s => op (X * S)%type ((E # tau s) t). - -Lemma slifting_stateT (X : UU0) : - (slifting op [the fmt of stateT S] (*naturality_MK*)) X = @op' _. -Proof. -apply boolp.funext => emx. -rewrite /op'. -apply boolp.funext => s. -rewrite /slifting. -rewrite 2!vcompE. -set h := hmap _. -rewrite [in RHS](psikE op). -rewrite 2!functor_app_naturalE. -rewrite /=. -congr (from_component _). -apply funext_dep => A; apply boolp.funext => f. -rewrite {1}/psi' /=. -rewrite /bindS /=. -rewrite /join_of_bind. -rewrite vcompE/=. -rewrite /liftS /=. -rewrite -(compE _ _ emx) -functor_o. -rewrite -[in RHS](compE _ _ emx) -functor_o. -rewrite bindA. -set ret_id := (X in _ >>= X). -have -> : ret_id = fun (x : MS S (codensityT M) X) (C : UU0) => (fun t => x s C t). - by apply boolp.funext. -rewrite {1}bindE /= /join_of_bind /=. -rewrite fmapE. -rewrite /bindK /=. -rewrite /psi' /= /bindK /kappa' /=. -rewrite /join_of_bind /=. -rewrite /retK /= /MK /=. -rewrite -(compE _ _ emx). -rewrite -functor_o. -rewrite -[in RHS](compE _ _ emx). -by rewrite -functor_o. -Qed. - -End slifting_stateT. - -Section slifting_exceptT. -Variable Z : UU0. - -Let op' : E \o exceptT Z M ~~> exceptT Z M := fun (Y : UU0) => @op _. - -Lemma slifting_exceptT (X : UU0) : - (slifting op [the fmt of exceptT Z] (*naturality_MK*)) X = @op' X. -Proof. -apply boolp.funext => emx. -rewrite /op'. -rewrite (psikE op (Z + X)%type). -rewrite /slifting. -rewrite 2!vcompE. -set h := hmap _. -rewrite /=. -f_equal. -rewrite /psi' /= /join_of_bind. -rewrite /bindX /= bindE /= {1}/join_of_bind /=. -rewrite fmapE. -rewrite /bindK /=. -apply funext_dep => A; apply boolp.funext => k. -rewrite vcompE/=. -rewrite /liftX /= bindE /= /join_of_bind /= /bindK /= fmapE /= /bindK /=. -rewrite /psi' /= /join_of_bind /= /bindK /= /kappa'. -congr (op _ _). -rewrite -(compE (E # _)). -by rewrite -functor_o. -Qed. - -End slifting_exceptT. - -Section slifting_envT. -Variable Env : UU0. - -Let tau (X : UU0) e (f : Env -> M X) := f e. - -Let op' : E \o envT Env M ~~> envT Env M := - fun (X : UU0) t => fun e => op X ((E # tau e) t). - -Lemma slifting_envT (X : UU0) : - (slifting op [the fmt of envT Env] (*naturality_MK*)) X = @op' _. -Proof. -apply boolp.funext => emx. -rewrite /op'. -apply boolp.funext => s. -rewrite /slifting. -rewrite 2!vcompE. -set h := hmap _. -rewrite (psikE op). -rewrite 2!functor_app_naturalE. -rewrite /=. -congr (from_component _). -apply funext_dep => A; apply boolp.funext => f. -rewrite {1}/psi' /= /join_of_bind /=. -rewrite /bindEnv /=. -rewrite vcompE/=. -rewrite bindE /= /join_of_bind /= /bindK. -rewrite fmapE /bindK. -rewrite /liftEnv /=. -rewrite -(compE _ _ emx) -functor_o. -rewrite -[in RHS](compE _ _ emx) -functor_o. -rewrite /psi' /= /bindK /= /kappa' /=. -congr (op A). -rewrite -(compE _ _ emx) -[in RHS](compE _ _ emx). -by rewrite -2!functor_o. -Qed. - -End slifting_envT. - -Section slifting_outputT. -Variable R : UU0. - -Let op' : E \o outputT R M ~~> outputT R M := - fun (X : UU0) => @op (X * seq R)%type. - -Lemma slifting_outputT (X : UU0) : - (slifting op [the fmt of outputT R] (*naturality_MK*)) X = @op' _. -Proof. -apply boolp.funext => emx. -rewrite /op'. -rewrite /slifting. -rewrite 2!vcompE. -set h := hmap _. -rewrite (psikE op). -rewrite 2!functor_app_naturalE. -rewrite /=. -f_equal. -rewrite /psi' /= /join_of_bind /= /bindK /bindO /= bindE /= /join_of_bind /bindK /=. -apply funext_dep => A; apply boolp.funext => f. -rewrite fmapE /bindK. -rewrite vcompE/=. -rewrite /liftO /=. -rewrite -(compE _ _ emx) -functor_o. -rewrite bindE /= /join_of_bind /= /bindK /=. -rewrite fmapE. -rewrite /bindK. -rewrite /psi' /= /bindK /= /kappa' /=. -congr (op A). -rewrite -(compE _ _ emx) -[in RHS](compE _ _ emx). -rewrite -2!functor_o. -congr ((E # _) _). -apply boolp.funext => rmx /=. -rewrite /retK /= bindE fmapE /= /join_of_bind /= /bindK. -congr (Lift [the monadT of codensityT] M _ _ _ _). -by apply boolp.funext => -[]. -Qed. - -End slifting_outputT. - -End slifting_instances. - -Unset Universe Checking. - -(* proposition 28 *) -Section slifting_alifting_coincide. - -Variables (E : functor) (M : monad) (aop : E.-aoperation M). -Hypothesis naturality_MK : forall (A : UU0) (m : MK M A), - naturality_MK m. - -Lemma slifting_alifting_stateFMT (S : UU0) (t := [the fmt of stateT S]) : - slifting aop t (*naturality_MK*) = alifting aop (Lift t M). -Proof. -apply nattrans_ext => X. -rewrite (slifting_stateT aop (*naturality_MK*) S). -apply boolp.funext => m; apply boolp.funext => s. -rewrite /alifting. -rewrite /=. -rewrite psiE /=. -rewrite /join_of_bind /= /bindS. -rewrite vcompE/=. -rewrite /liftS/=. -rewrite 2!algebraic. -congr (aop _ _). -rewrite -[RHS](compE _ (E # _)). -rewrite -functor_o. -rewrite -[RHS](compE _ (E # _)). -rewrite -functor_o. -congr ((E # _) m). -apply boolp.funext => x /=. -by rewrite 2!bindretf. -Qed. - -Lemma slifting_alifting_exceptFMT (Z : UU0) (t := [the fmt of exceptT Z]) : - slifting aop t (*naturality_MK*) = alifting aop (Lift t M). -Proof. -apply nattrans_ext => X. -rewrite (slifting_exceptT aop (*naturality_MK*) Z). -apply boolp.funext => m. -rewrite /alifting. -rewrite /=. -rewrite psiE /= /join_of_bind /bindX. -rewrite vcompE/=. -rewrite /liftX. -rewrite 2!algebraic. -congr (aop _ _). -rewrite -[RHS](compE _ (E # _)). -rewrite -functor_o. -rewrite -[RHS](compE _ (E # _)). -rewrite -functor_o. -rewrite (_ : _ \o Ret = id) ?functor_id //. -(*apply boolp.funext => n /=. -by rewrite 2!bindretf.*) -Qed. - -Lemma slifting_alifting_envFMT (Env : UU0) (t := [the fmt of envT Env]) : - slifting aop t (*naturality_MK*) = alifting aop (Lift t M). -Proof. -apply nattrans_ext => X. -rewrite (slifting_envT aop (*naturality_MK*) Env). -apply boolp.funext => m; apply boolp.funext => e. -rewrite /alifting. -rewrite /=. -rewrite psiE /= /join_of_bind /= /bindEnv. -rewrite vcompE/=. -rewrite /liftEnv. -rewrite algebraic. -congr (aop _ _). -rewrite -[RHS](compE _ (E # _)). -rewrite -functor_o. -congr ((E # _) m). -apply boolp.funext => x /=. -by rewrite bindretf. -Qed. - -Lemma slifting_alifting_outputFMT (R : UU0) (t := [the fmt of outputT R]) : - slifting aop t (*naturality_MK*) = alifting aop (Lift t M). -Proof. -apply nattrans_ext => X. -rewrite (slifting_outputT aop (*naturality_MK*) R). -apply boolp.funext => m. -rewrite /alifting. -rewrite /=. -rewrite psiE /= /join_of_bind /= /bindO. -rewrite vcompE/=. -rewrite /liftO. -rewrite 2!algebraic. -congr (aop _ _). -rewrite -[RHS](compE _ (E # _)). -rewrite -functor_o. -rewrite -[RHS](compE _ (E # _)). -rewrite -functor_o. -by rewrite (_ : _ \o Ret = id) ?functor_id //. -(*apply boolp.funext => n /=. -rewrite 2!bindretf. -Open (X in _ >>= X). - by case : x => ? ?; rewrite cat0s. -by rewrite bindmret.*) -Qed. - -End slifting_alifting_coincide. - -Set Universe Checking. - -Require Import monad_model. - -(* example 30 *) -Section slifting_local. -Variable Env : UU0. -Let E := [the functor of Local.acto Env]. -Let M := [the monad of EnvironmentMonad.acto Env]. -Let local : E.-operation M := local_op Env. -Hypothesis naturality_MK : forall (A : UU0) (m : MK M A), naturality_MK m. - -Section slifting_local_FMT. -Variable T : fmt. - -Definition localKT (f : Env -> Env) : T (codensityT M) ~~> T (codensityT M) := - fun (X : UU0) t => Join - (Lift T (codensityT M) (T (codensityT M) X) (fun Y k => local Y (f, k t))). - -Definition localT (f : Env -> Env) : T M ~~> T M := - fun X t => let t' := hmap T (Lift [the monadT of codensityT] M) X t in - hmap T (from (*naturality_MK*) M) X (localKT f t'). - -End slifting_local_FMT. - -Section slifting_local_stateT. -Variable S : UU0. - -Definition local_stateT (f : Env -> Env) : stateT S M ~~> stateT S M := - fun X t s e => t s (f e). - -Let local_stateT' : (E \o stateT S M) ~~> (stateT S M) := - fun X => uncurry (@local_stateT ^~ X). - -Lemma local_stateTE (X : UU0) : - (slifting local [the fmt of stateT S] (*naturality_MK*)) X = @local_stateT' X. -Proof. by rewrite slifting_stateT; apply boolp.funext => -[]. Qed. -End slifting_local_stateT. - -Section slifting_local_exceptT. -Variable Z : UU0. -Definition local_exceptT (f : Env -> Env) : exceptT Z M ~~> exceptT Z M := - fun X t e => t (f e). - -Let local_exceptT' : (E \o exceptT Z M) ~~> (exceptT Z M) := - fun X => uncurry (@local_exceptT ^~ X). - -Lemma local_exceptTE (X : UU0) : - (slifting local [the fmt of exceptT Z] (*naturality_MK*)) X = @local_exceptT' X. -Proof. by rewrite slifting_exceptT; apply boolp.funext => -[]. Qed. - -End slifting_local_exceptT. - -Section slifting_local_envT. -Variable Z : UU0. -Definition local_envT (f : Env -> Env) : envT Z M ~~> envT Z M := - fun X t e e' => t e (f e'). - -Let local_envT' : E \o envT Z M ~~> envT Z M := - fun X => uncurry (@local_envT ^~ X). - -Lemma local_envTE (X : UU0) : - (slifting local [the fmt of envT Z] (*naturality_MK*)) X = @local_envT' X. -Proof. -rewrite slifting_envT. -by apply boolp.funext => -[]. -Qed. -End slifting_local_envT. - -Section slifting_local_outputT. -Variable R : UU0. -Definition local_outputT (f : Env -> Env) : outputT R M ~~> outputT R M := - fun (X : UU0) t e => t (f e). - -Let local_outputT' : E \o outputT R M ~~> outputT R M := - fun (X : UU0) => uncurry (@local_outputT ^~ X). - -Lemma local_outputTE (X : UU0) : - (slifting local [the fmt of outputT R] (*naturality_MK*)) X = @local_outputT' X. -Proof. by rewrite slifting_outputT; apply boolp.funext => -[]. Qed. -End slifting_local_outputT. - -End slifting_local. - -(* example 31 *) -Section slifting_handle. (* except monad with Z = unit *) -Let E := [the functor of Handle.acto unit]. -Let M := [the monad of ExceptMonad.acto unit]. -Let handle : E.-operation M := @handle_op unit. -Hypothesis naturality_MK : forall (A : UU0) (m : MK M A), - naturality_MK m. - -Section slifting_handle_stateT. -Variable S : UU0. -Definition handle_stateT (X : UU0) (t : stateT S M X) (h : unit -> stateT S M X) - : stateT S M X := fun s => match t s with - | inl z(*unit*) => h z s - | inr x => inr x - end. - -Let handle_stateT' : (E \o stateT S M) ~~> (stateT S M) := - fun (X : UU0) => uncurry (@handle_stateT X). - -Lemma handle_stateTE (X : UU0) : - (slifting handle [the fmt of stateT S] (*naturality_MK*)) X = @handle_stateT' X. -Proof. by rewrite slifting_stateT; apply boolp.funext => -[m f]. Qed. -End slifting_handle_stateT. - -Section slifting_handle_exceptT. -Variable Z : UU0. -Definition handle_exceptT (X : UU0) (t : exceptT Z M X) - (h : unit -> exceptT Z M X) : exceptT Z M X := match t with - | inl z(*unit*) => h z - | inr x => inr x - end. - -Let handle_exceptT' : E \o exceptT Z M ~~> exceptT Z M := - fun (X : UU0) => uncurry (@handle_exceptT X). - -Lemma handle_exceptTE (X : UU0) : - (slifting handle [the fmt of exceptT Z] (*naturality_MK*)) X = @handle_exceptT' X. -Proof. by rewrite slifting_exceptT; exact: boolp.funext. Qed. -End slifting_handle_exceptT. - -Section slifting_handle_envT. -Variable Z : UU0. -Definition handle_envT (X : UU0) (t : envT Z M X) (h : unit -> envT Z M X) - : envT Z M X := fun e => match t e with - | inl z(*unit*) => h z e - | inr x => inr x - end. - -Let handle_envT' : E \o envT Z M ~~> envT Z M := - fun (X : UU0) => uncurry (@handle_envT X). - -Lemma handle_envTE (X : UU0) : - (slifting handle [the fmt of envT Z] (*naturality_MK*)) X = @handle_envT' X. -Proof. -by rewrite slifting_envT; apply boolp.funext => -[m f]; exact: boolp.funext. -Qed. -End slifting_handle_envT. - -Section slifting_handle_outputT. -Variable R : UU0. -Definition handle_outputT (X : UU0) (t : outputT R M X) - (h : unit -> outputT R M X) : outputT R M X := match t with - | inl z(*unit*) => h z - | inr x => inr x - end. - -Let handle_outputT' : E \o outputT R M ~~> outputT R M := - fun (X : UU0) => uncurry (@handle_outputT X). - -Lemma handle_outputTE (X : UU0) : - (slifting handle [the fmt of outputT R] (*naturality_MK*)) X = @handle_outputT' X. -Proof. by rewrite slifting_outputT; apply boolp.funext => -[]. Qed. -End slifting_handle_outputT. - -End slifting_handle. - -(* example 32 *) -Section slifting_flush. -Variable R : UU0. -Let E := [the functor of Flush.acto]. -Let M := [the monad of OutputMonad.acto R]. -Let flush : E.-operation M := flush_op R. -Hypothesis naturality_MK : forall (A : UU0) (m : MK M A), - naturality_MK m. - -Section slifting_flush_stateT. -Variable S : UU0. -Definition flush_stateT : stateT S M ~~> stateT S M := - fun (X : UU0) t s => let: (x, _) := t s in (x, [::]). - -Lemma flush_stateTE (X : UU0) : - (slifting flush [the fmt of stateT S] (*naturality_MK*)) X = @flush_stateT X. -Proof. by rewrite slifting_stateT. Qed. -End slifting_flush_stateT. - -Section slifting_flush_exceptT. -Variable Z : UU0. -Definition flush_exceptT (X : UU0) (t : exceptT Z M X) (h : Z -> exceptT Z M X) - : exceptT Z M X := - let: (c, _) := t in (c, [::]). - -Let flush_exceptT' : E \o exceptT Z M ~~> exceptT Z M := - fun (X : UU0) c => let : (x, _) := c in (x, [::]). - -Lemma flush_exceptTE (X : UU0) : - (slifting flush [the fmt of exceptT Z] (*naturality_MK*)) X = @flush_exceptT' X. -Proof. by rewrite slifting_exceptT. Qed. -End slifting_flush_exceptT. - -Section slifting_flush_envT. -Variable Z : UU0. -Definition flush_envT : envT Z M ~~> envT Z M := - fun (X : UU0) t e => let: (x, _) := t e in (x, [::]). - -Lemma flush_envTE (X : UU0) : - (slifting flush [the fmt of envT Z] (*naturality_MK*)) X = @flush_envT X. -Proof. by rewrite slifting_envT. Qed. -End slifting_flush_envT. - -Section slifting_flush_outputT. -Variable Z : UU0. -Definition flush_outputT (X : UU0) (t : outputT R M X) (h : Z -> outputT R M X) - : outputT R M X := let: (p, w) := t in (p, [::]). - -Let flush_outputT' : E \o outputT R M ~~> outputT R M := - fun (X : UU0) e => let: (pw, w') := e in (pw, [::]). - -Lemma flush_outputTE (X : UU0) : - (slifting flush [the fmt of outputT R] (*naturality_MK*)) X = @flush_outputT' X. -Proof. by rewrite slifting_outputT; exact: boolp.funext. Qed. -End slifting_flush_outputT. - -End slifting_flush. diff --git a/gcm_model.v b/gcm_model.v index 70a96076..bc0ec9bf 100644 --- a/gcm_model.v +++ b/gcm_model.v @@ -631,7 +631,8 @@ Definition A1 := AdjointFunctors.mk triL1 triR1. Definition Aprob := adj_comp AC A0. Definition Agcm := adj_comp Aprob A1. Definition Mgcm := Monad_of_adjoint Agcm. -Definition gcm := [the hierarchy.monad of Monad_of_category_monad.acto Mgcm]. +Definition gcm := + [the hierarchy.Monad.Exports.monad of Monad_of_category_monad.acto Mgcm]. Section gcm_opsE. Import hierarchy. @@ -686,8 +687,8 @@ Import category. (* probability monad built directly *) Definition M := proba_monad_model.MonadProbModel.t. (* probability monad built using adjunctions *) -Definition N := - [the hierarchy.monad of Monad_of_category_monad.acto (Monad_of_adjoint Aprob)]. +Definition N := [the hierarchy.Monad.Exports.monad of + Monad_of_category_monad.acto (Monad_of_adjoint Aprob)]. Lemma actmE T : N T = M T. Proof. by []. Qed. diff --git a/hierarchy.v b/hierarchy.v index f8322c32..9ec927f5 100644 --- a/hierarchy.v +++ b/hierarchy.v @@ -123,7 +123,7 @@ Section def. Variable (F : UU0 -> UU0) (f : forall A B : UU0, (A -> B) -> F A -> F B). Definition id := forall A : UU0, f id = id :> (F A -> F A). Definition comp := forall (A B C : UU0) (g : B -> C) (h : A -> B), - f (g \o h) = f g \o f h :> (F A -> F C). + f (g \o h) = f g \o f h. End def. End FunctorLaws. @@ -132,16 +132,16 @@ HB.mixin Record isFunctor (F : UU0 -> UU0) := { functor_id : FunctorLaws.id actm ; functor_o : FunctorLaws.comp actm }. +#[short(type=functor)] HB.structure Definition Functor := {F of isFunctor F}. -Notation functor := Functor.type. Notation "F # g" := (@actm F _ _ g) : monae_scope. Notation "'fmap' f" := (_ # f) : mprog. Section functorid. -Definition id_f (A B : UU0) (f : A -> B) : idfun A -> idfun B := f. -Let id_id : FunctorLaws.id id_f. Proof. by []. Qed. -Let id_comp : FunctorLaws.comp id_f. Proof. by []. Qed. +Let id_actm (A B : UU0) (f : A -> B) : idfun A -> idfun B := f. +Let id_id : FunctorLaws.id id_actm. Proof. by []. Qed. +Let id_comp : FunctorLaws.comp id_actm. Proof. by []. Qed. HB.instance Definition _ := isFunctor.Build idfun id_id id_comp. End functorid. @@ -203,7 +203,8 @@ Arguments fcomp : simpl never. Lemma functor_ext (F G : functor) : forall (H : Functor.sort F = Functor.sort G), @actm G = - eq_rect _ (fun m : UU0 -> UU0 => forall A B : UU0, (A -> B) -> m A -> m B) (@actm F) _ H -> + eq_rect _ (fun m : UU0 -> UU0 => forall A B : UU0, (A -> B) -> m A -> m B) + (@actm F) _ H -> G = F. Proof. move: F G => [F [[HF1 HF2 HF3]]] [G [[HG1 HG2 HG3]]] /= H. @@ -226,9 +227,9 @@ Arguments naturality : clear implicits. HB.mixin Record isNatural (F G : functor) (f : F ~~> G) := { natural : naturality F G f }. +#[short(type=nattrans)] HB.structure Definition Nattrans (F G : functor) := {f of isNatural F G f}. Arguments natural {F G} s. -Notation nattrans := Nattrans.type. Notation "f ~> g" := (nattrans f g) : monae_scope. Section natrans_lemmas. @@ -303,11 +304,10 @@ HB.mixin Record isMonad (F : UU0 -> UU0) of Functor F := { bind A B m f = join B (([the functor of F] # f) m) ; joinretM : JoinLaws.left_unit ret join ; joinMret : JoinLaws.right_unit ret join ; - joinA : JoinLaws.associativity join -}. + joinA : JoinLaws.associativity join }. +#[short(type=monad)] HB.structure Definition Monad := {F of isMonad F &}. -Notation monad := Monad.type. Arguments bind {s A B} : simpl never. Notation "m >>= f" := (bind m f) : monae_scope. @@ -380,7 +380,8 @@ rewrite fmapE bindA; congr bind. by apply boolp.funext => ?; rewrite bindretf. Qed. -Lemma naturality_join : naturality [the functor of F \o F] F (join_of_bind bind). +Lemma naturality_join : + naturality [the functor of F \o F] F (join_of_bind bind). Proof. move=> A B h; apply boolp.funext => mma /=. rewrite fmapE /join_of_bind bindA bind_Map; congr bind. @@ -488,7 +489,8 @@ Qed. End monad_lemmas. Notation "'do' x <- m ; e" := (bind m (fun x => e)) (only parsing) : do_notation. -Notation "'do' x : T <- m ; e" := (bind m (fun x : T => e)) (only parsing) : do_notation. +Notation "'do' x : T <- m ; e" := + (bind m (fun x : T => e)) (only parsing) : do_notation. Delimit Scope do_notation with Do. Notation "m >> f" := (bind m (fun _ => f)) : monae_scope. @@ -554,7 +556,8 @@ Proof. case: ifPn => Hb //; by rewrite fmapE bindretf. Qed. Lemma fmap_bind (A B C : UU0) (f : A -> B) m (g : C -> M A) : fmap f (m >>= g) = m >>= (f (o) g). Proof. -rewrite fcomp_def fmapE bindA; bind_ext => c; by rewrite compE -/(fmap _ _) fmapE. +rewrite fcomp_def fmapE bindA; bind_ext => c. +by rewrite compE -/(fmap _ _) fmapE. Qed. Lemma skip_fmap (A B : UU0) (f : A -> B) (mb : M B) ma : @@ -625,16 +628,14 @@ Notation "m >=> n" := (kleisli n m) : monae_scope. HB.mixin Record isMonadFail (M : UU0 -> UU0) of Monad M := { fail : forall A : UU0, M A; - (* exceptions are left-zeros of sequential composition *) - bindfailf : BindLaws.left_zero (@bind [the monad of M]) fail (* fail A >>= f = fail B *) -}. + (* exceptions are left-zeros of sequential composition *) + bindfailf : BindLaws.left_zero (@bind [the monad of M]) fail + (* fail A >>= f = fail B *) }. +#[short(type=failMonad)] HB.structure Definition MonadFail := {M of isMonadFail M & }. -Notation failMonad := MonadFail.type. Arguments bindfailf [_]. - -(*Definition Fail (M : failMonad) := @fail M.*) Arguments fail {_} {_}. Section guard_assert. @@ -658,7 +659,8 @@ Qed. Definition assert {A : UU0} (p : pred A) (a : A) : M A := locked (guard (p a) >> Ret a). -Lemma assertE {A : UU0} (p : pred A) (a : A) : assert p a = guard (p a) >> Ret a. +Lemma assertE {A : UU0} (p : pred A) (a : A) : + assert p a = guard (p a) >> Ret a. Proof. by rewrite /assert; unlock. Qed. Lemma assertT {A : UU0} (a : A) : assert xpredT a = Ret a. @@ -705,46 +707,52 @@ HB.mixin Record isMonadAlt (M : UU0 -> UU0) of Monad M := { (* composition distributes leftwards over choice *) alt_bindDl : BindLaws.left_distributive (@bind [the monad of M]) alt (* in general, composition does not distribute rightwards over choice *) -(* NB: no bindDr to accommodate both angelic and demonic interpretations of nondeterminism *) -}. +(* NB: no bindDr to accommodate both angelic and demonic interpretations of + nondeterminism *) }. +#[short(type=altMonad)] HB.structure Definition MonadAlt := {M of isMonadAlt M & }. Notation "a [~] b" := (@alt _ _ a b). (* infix notation *) -Notation altMonad := MonadAlt.type. - HB.mixin Record isMonadAltCI (M : UU0 -> UU0) of MonadAlt M := { altmm : forall A : UU0, idempotent (@alt [the altMonad of M] A) ; - altC : forall A : UU0, commutative (@alt [the altMonad of M] A) -}. + altC : forall A : UU0, commutative (@alt [the altMonad of M] A) }. +#[short(type=altCIMonad)] HB.structure Definition MonadAltCI := {M of isMonadAltCI M & }. -Notation altCIMonad := MonadAltCI.type. Arguments altC {_} {_}. Arguments altmm {_} {_}. Section altci_lemmas. Variable (M : altCIMonad). + Lemma altCA A : @left_commutative (M A) (M A) (fun x y => x [~] y). Proof. by move=> x y z; rewrite altA altC altA altC (altC x). Qed. + Lemma altAC A : @right_commutative (M A) (M A) (fun x y => x [~] y). Proof. move=> x y z; by rewrite altC altA (altC x). Qed. + Lemma altACA A : @interchange (M A) (fun x y => x [~] y) (fun x y => x [~] y). Proof. move=> x y z t; rewrite !altA; congr (_ [~] _); by rewrite altAC. Qed. + End altci_lemmas. HB.mixin Record isMonadNondet (M : UU0 -> UU0) of MonadFail M & MonadAlt M := { - altfailm : @BindLaws.left_id [the functor of M] (@fail [the failMonad of M]) (@alt [the altMonad of M]); - altmfail : @BindLaws.right_id [the functor of M] (@fail [the failMonad of M]) (@alt [the altMonad of M]) -}. - -HB.structure Definition MonadNondet := {M of isMonadNondet M & MonadFail M & MonadAlt M}. -Notation nondetMonad := MonadNondet.type. - + altfailm : + @BindLaws.left_id [the functor of M] (@fail [the failMonad of M]) + (@alt [the altMonad of M]); + altmfail : + @BindLaws.right_id [the functor of M] (@fail [the failMonad of M]) + (@alt [the altMonad of M]) }. + +#[short(type=nondetMonad)] +HB.structure Definition MonadNondet := + {M of isMonadNondet M & MonadFail M & MonadAlt M}. + +#[short(type=nondetCIMonad)] HB.structure Definition MonadCINondet := {M of MonadAltCI M & MonadNondet M}. -Notation nondetCIMonad := MonadCINondet.type. Section nondet_big. Variables (M : nondetMonad) (A : UU0). @@ -759,22 +767,21 @@ Qed. End nondet_big. -HB.mixin Record isMonadFailR0 (M : UU0 -> UU0) of MonadFail M := { - bindmfail : BindLaws.right_zero (@bind [the monad of M]) (@fail _) -}. +HB.mixin Record isMonadFailR0 (M : UU0 -> UU0) of MonadFail M := + { bindmfail : BindLaws.right_zero (@bind [the monad of M]) (@fail _) }. +#[short(type=failR0Monad)] HB.structure Definition MonadFailR0 := {M of isMonadFailR0 M & }. -Notation failR0Monad := MonadFailR0.type. -HB.mixin Record isMonadPrePlus (M : UU0 -> UU0) of MonadNondet M & MonadFailR0 M := { - alt_bindDr : BindLaws.right_distributive (@bind [the monad of M]) (@alt _) -}. +HB.mixin Record isMonadPrePlus (M : UU0 -> UU0) + of MonadNondet M & MonadFailR0 M := + { alt_bindDr : BindLaws.right_distributive (@bind [the monad of M]) (@alt _) }. +#[short(type=prePlusMonad)] HB.structure Definition MonadPrePlus := {M of isMonadPrePlus M & }. -Notation prePlusMonad := MonadPrePlus.type. +#[short(type=plusMonad)] HB.structure Definition MonadPlus := {M of MonadCINondet M & MonadPrePlus M}. -Notation plusMonad := MonadPlus.type. HB.mixin Record isMonadExcept (M : UU0 -> UU0) of MonadFail M := { catch : forall A, M A -> M A -> M A ; @@ -784,75 +791,77 @@ HB.mixin Record isMonadExcept (M : UU0 -> UU0) of MonadFail M := { catchA : forall A, associative (@catch A) ; (* unexceptional bodies need no handler *) catchret : forall A x, @left_zero (M A) (M A) (Ret x) (@catch A) - (* NB: left-zero of sequential composition inherited from failMonad *) -}. + (* NB: left-zero of sequential composition inherited from failMonad *) }. +#[short(type=exceptMonad)] HB.structure Definition MonadExcept := {M of isMonadExcept M & }. -Notation exceptMonad := MonadExcept.type. -(*Definition Catch (M : exceptMonad) := @catch M.*) Arguments catch {_} {_}. HB.mixin Record isMonadContinuation (M : UU0 -> UU0) of Monad M := { (* NB: interface is wip *) - callcc : forall A B : UU0, ((A -> M B) -> M A) -> M A; - callcc0 : forall (A B : UU0) (g : (A -> M B) -> M A) (k : B -> M B), - @callcc _ _ (fun f => g (fun x => f x >>= k)) = @callcc _ _ g; (* see Sect. 7.2 of [Schrijvers, 19] *) - callcc1 : forall (A B : UU0) (m : M B), @callcc _ _ (fun _ : B -> M A => m) = m ; (* see Sect. 3.3 of [Wadler, 94] *) - callcc2 : forall (A B C : UU0) (m : M A) x (k : A -> B -> M C), - @callcc _ _ (fun f : _ -> M _ => m >>= (fun a => f x >>= (fun b => k a b))) = - @callcc _ _ (fun f : _ -> M _ => m >> f x) ; - callcc3 : forall (A B : UU0) (m : M A) b, - @callcc _ _ (fun f : B -> M B => m >> f b) = - @callcc _ _ (fun _ : B -> M B => m >> Ret b) -}. - + callcc : forall A B : UU0, ((A -> M B) -> M A) -> M A; + callcc0 : forall (A B : UU0) (g : (A -> M B) -> M A) (k : B -> M B), + @callcc _ _ (fun f => g (fun x => f x >>= k)) = @callcc _ _ g + (* see Sect. 7.2 of [Schrijvers, 19] *); + callcc1 : forall (A B : UU0) (m : M B), + @callcc _ _ (fun _ : B -> M A => m) = m + (* see Sect. 3.3 of [Wadler, 94] *); + callcc2 : forall (A B C : UU0) (m : M A) x (k : A -> B -> M C), + @callcc _ _ (fun f : _ -> M _ => m >>= (fun a => f x >>= (fun b => k a b))) + = @callcc _ _ (fun f : _ -> M _ => m >> f x) ; + callcc3 : forall (A B : UU0) (m : M A) b, + @callcc _ _ (fun f : B -> M B => m >> f b) = + @callcc _ _ (fun _ : B -> M B => m >> Ret b) }. + +#[short(type=contMonad)] HB.structure Definition MonadContinuation := {M of isMonadContinuation M & }. -Notation contMonad := MonadContinuation.type. -(*Definition Callcc (M : contMonad) := @callcc M.*) Arguments callcc {_} {_} {_}. -HB.mixin Record isMonadShiftReset (U : UU0) (M : UU0 -> UU0) of MonadContinuation M := { +HB.mixin Record isMonadShiftReset (U : UU0) (M : UU0 -> UU0) + of MonadContinuation M := { shift : forall A : UU0, ((A -> M U) -> M U) -> M A ; reset : M U -> M U ; shiftreset0 : forall (A : UU0) (m : M A), @shift _ (fun k => m >>= k) = m ; (* see Sect. 3.3 of [Wadler, 94] *) - shiftreset1 : forall (A B : UU0) (h : (A -> M B) -> M A), - callcc h = @shift _ (fun k' => h (fun x => @shift _ (fun k'' => k' x)) >>= k') ; + shiftreset1 : forall (A B : UU0) (h : (A -> M B) -> M A), callcc h = + @shift _ (fun k' => h (fun x => @shift _ (fun k'' => k' x)) >>= k') ; (* see Sect. 3.3 of [Wadler, 94] *) shiftreset2 : forall (A : UU0) (c : A) (c': U) (k : A -> U -> _), - (reset (do x <- Ret c; do y <- @shift _ (fun _ => Ret c'); k x y) = Ret c >> Ret c')%Do ; + (reset (do x <- Ret c; do y <- @shift _ (fun _ => Ret c'); k x y) = + Ret c >> Ret c')%Do ; shiftreset3 : forall (c c' : U) (k : U -> U -> _), - (reset (do x <- Ret c; do y <- @shift _ (fun f => do v <- f c'; f v); Ret (k x y)) = - reset (do x <- Ret c; do y <- @shift _ (fun f => f c'); Ret (k x (k x y))))%Do ; + (reset (do x <- Ret c; do y <- @shift _ (fun f => do v <- f c'; f v); + Ret (k x y)) = + reset (do x <- Ret c; do y <- @shift _ (fun f => f c'); + Ret (k x (k x y))))%Do ; shiftreset4 : forall (c : U) k, - (reset (do y <- @shift _ (@^~ c); Ret (k y)) = Ret (k c))%Do -}. + (reset (do y <- @shift _ (@^~ c); Ret (k y)) = Ret (k c))%Do }. +#[short(type=shiftresetMonad)] HB.structure Definition MonadShiftReset U := {M of isMonadShiftReset U M & }. -Notation shiftresetMonad := MonadShiftReset.type. -(*Definition Shift U (M : shiftresetMonad U) := @shift U M.*) Arguments shift {_} {_} {_}. -(*Definition Reset U (M : shiftresetMonad U) := @reset U M. -Arguments Reset {_} {_}.*) (* NB: wip, no model *) (* Sect. 7.2 of [Tom Schrijvers & al., Monad Transformers and Modular Algebraic Effects: What Binds Them Together, Haskell 2019] *) HB.mixin Record isMonadJump (ref : UU0 -> UU0) (M : UU0 -> UU0) of Monad M := { - jump : forall A B : UU0, ref A -> A -> M B; - sub : forall A B : UU0, (ref A -> M B) -> (A -> M B) -> M B; - jump0 : forall (A B : UU0) k x, @sub _ _ (fun r => @jump A B r x) k = k x ; - jump1 : forall (A B : UU0) p k, @sub A B (fun _ => p) k = p; - jump2 : forall (A B : UU0) p r', @sub _ _ p (@jump A B r') = p r'; - jump3 : forall (A B : UU0) (p : ref A -> ref B -> M B) (k1 : A -> M B) k2, - @sub _ _ (fun r1 : ref A => @sub _ _ (fun r2 => p r1 r2) (k2 r1)) k1 = - @sub _ _ (fun r2 : ref B => @sub _ _ (fun r1 => p r1 r2) k1) (fun x => @sub _ _ (k2^~ x) k1); (*NB: differs from [Schrijvers et al. 19]*) - jump4 : forall (A B : UU0) r x k, (@jump A B r x) >>= k = @jump A B r x; - jump5 : forall (A B : UU0) p q k, @sub A B p q >>= k = @sub A B (p >=> k) (q >=> k) -}. + jump : forall A B : UU0, ref A -> A -> M B; + sub : forall A B : UU0, (ref A -> M B) -> (A -> M B) -> M B; + jump0 : forall (A B : UU0) k x, @sub _ _ (fun r => @jump A B r x) k = k x ; + jump1 : forall (A B : UU0) p k, @sub A B (fun _ => p) k = p; + jump2 : forall (A B : UU0) p r', @sub _ _ p (@jump A B r') = p r'; + jump3 : forall (A B : UU0) (p : ref A -> ref B -> M B) (k1 : A -> M B) k2, + @sub _ _ (fun r1 : ref A => @sub _ _ (fun r2 => p r1 r2) (k2 r1)) k1 = + @sub _ _ (fun r2 : ref B => @sub _ _ (fun r1 => p r1 r2) k1) + (fun x => @sub _ _ (k2^~ x) k1) + (*NB: differs from [Schrijvers et al. 19]*); + jump4 : forall (A B : UU0) r x k, (@jump A B r x) >>= k = @jump A B r x; + jump5 : forall (A B : UU0) p q k, + @sub A B p q >>= k = @sub A B (p >=> k) (q >=> k) }. + +#[short(type=jumpMonad)] HB.structure Definition MonadJump ref := {M of isMonadJump ref M & }. -Notation jumpMonad := MonadJump.type. Definition Jump ref (M : jumpMonad ref) := @jump ref M. Arguments Jump {_} {_} {_} {_}. Definition Sub ref (M : jumpMonad ref) := @sub ref M. @@ -867,48 +876,53 @@ HB.mixin Record isMonadState (S : UU0) (M : UU0 -> UU0) of Monad M := { getget : forall (A : UU0) (k : S -> S -> M A), get >>= (fun s => get >>= k s) = get >>= fun s => k s s }. +#[short(type=stateMonad)] HB.structure Definition MonadState (S : UU0) := { M of isMonadState S M & }. -Notation stateMonad := MonadState.type. (*NB: explicit join newly added*) +#[short(type=failStateMonad)] HB.structure Definition MonadFailState (S : UU0) := { M of isMonadFail M & isMonadState S M & isMonad M & isFunctor M }. -Notation failStateMonad := MonadFailState.type. (*NB: explicit join newly added*) +#[short(type=failR0StateMonad)] HB.structure Definition MonadFailR0State (S : UU0) := - { M of isMonadFailR0 M & isMonadState S M & isMonadFail M & isMonad M & isFunctor M }. -Notation failR0StateMonad := MonadFailR0State.type. + { M of isMonadFailR0 M & isMonadState S M & isMonadFail M & isMonad M & + isFunctor M }. +#[short(type=nondetStateMonad)] HB.structure Definition MonadNondetState (S : UU0) := { M of MonadPrePlus M & MonadState S M }. -Notation nondetStateMonad := MonadNondetState.type. HB.mixin Record isMonadStateRun (S : UU0) (N : monad) (M : UU0 -> UU0) of MonadState S M := { runStateT : forall A : UU0, M A -> S -> N (A * S)%type ; - runStateTret : forall (A : UU0) (a : A) (s : S), @runStateT _ (Ret a) s = Ret (a, s) ; + runStateTret : forall (A : UU0) (a : A) (s : S), + @runStateT _ (Ret a) s = Ret (a, s) ; runStateTbind : forall (A B : UU0) (m : M A) (f : A -> M B) (s : S), - @runStateT _ (m >>= f) s = @runStateT _ m s >>= fun x => @runStateT _ (f x.1) x.2 ; + @runStateT _ (m >>= f) s = + @runStateT _ m s >>= fun x => @runStateT _ (f x.1) x.2 ; runStateTget : forall s : S, @runStateT _ get s = Ret (s, s) ; runStateTput : forall s' s : S, @runStateT _ (put s') s = Ret (tt, s') }. +#[short(type=stateRunMonad)] HB.structure Definition MonadStateRun (S : UU0) (N : monad) := {M of isMonadStateRun S N M & }. -Notation stateRunMonad := MonadStateRun.type. + Arguments runStateT {_} {_} {_} {_}. -HB.mixin Record isMonadExceptStateRun (S : UU0) (N : exceptMonad) - (M : UU0 -> UU0) of MonadStateRun S N M & MonadExcept M - := Mixin { +HB.mixin Record isMonadExceptStateRun + (S : UU0) (N : exceptMonad) (M : UU0 -> UU0) + of MonadStateRun S N M & MonadExcept M := Mixin { runStateTfail : forall (A : UU0) (s : S), runStateT (@fail [the exceptMonad of M] A) s = @fail N _ ; runStateTcatch : forall (A : UU0) (s : S) (m1 m2 : M A), - runStateT (@catch [the exceptMonad of M] _ m1 m2) s = @catch N _ (runStateT m1 s) (runStateT m2 s) }. + runStateT (@catch [the exceptMonad of M] _ m1 m2) s = + @catch N _ (runStateT m1 s) (runStateT m2 s) }. +#[short(type=exceptStateRunMonad)] HB.structure Definition MonadExceptStateRun (S : UU0) (N : exceptMonad) := {M of isMonadExceptStateRun S N M & }. -Notation exceptStateRunMonad := MonadExceptStateRun.type. HB.mixin Record isMonadReify (S : UU0) (M : UU0 -> UU0) of Monad M := { reify : forall A : UU0, M A -> S -> option (A * S)%type ; @@ -917,81 +931,54 @@ HB.mixin Record isMonadReify (S : UU0) (M : UU0 -> UU0) of Monad M := { @reify _ (m >>= f) s = match @reify _ m s with | Some a's' => @reify _ (f a's'.1) a's'.2 | None => None - end -}. + end }. +#[short(type=reifyMonad)] HB.structure Definition MonadReify (S : UU0) := {M of isMonadReify S M & }. -Notation reifyMonad := MonadReify.type. Arguments reify {_} {_} {_}. -HB.mixin Record isMonadStateReify (S : UU0) (M : UU0 -> UU0) of MonadReify S M & MonadState S M := { +HB.mixin Record isMonadStateReify (S : UU0) (M : UU0 -> UU0) + of MonadReify S M & MonadState S M := { reifyget : forall s, reify (@get _ [the stateMonad S of M]) s = Some (s, s) ; - reifyput : forall s s', reify (@put _ [the stateMonad S of M] s') s = Some (tt, s') -}. + reifyput : forall s s', + reify (@put _ [the stateMonad S of M] s') s = Some (tt, s') }. -HB.structure Definition MonadStateReify (S : UU0) := {M of isMonadStateReify S M &}. -Notation stateReifyMonad := MonadStateReify.type. +#[short(type=stateReifyMonad)] +HB.structure Definition MonadStateReify (S : UU0) := + {M of isMonadStateReify S M &}. -HB.mixin Record isMonadFailReify (S : UU0) (M : UU0 -> UU0) of MonadReify S M & MonadFail M := { - reifyfail : forall S' (s : S), reify (@fail [the failMonad of M] S') s = None -}. +HB.mixin Record isMonadFailReify (S : UU0) (M : UU0 -> UU0) + of MonadReify S M & MonadFail M := + { reifyfail : forall S' (s : S), + reify (@fail [the failMonad of M] S') s = None }. + +#[short(type=failReifyMonad)] +HB.structure Definition MonadFailReify (S : UU0) := + {M of isMonadFailReify S M & }. -HB.structure Definition MonadFailReify (S : UU0) := {M of isMonadFailReify S M & }. -Notation failReifyMonad := MonadFailReify.type. - -HB.structure Definition MonadFailFailR0Reify (S : UU0) := {M of MonadFailReify S M & MonadFailR0 M}. -Notation failFailR0ReifyMonad := MonadFailFailR0Reify.type. - -HB.structure Definition MonadFailStateReify (S : UU0) := {M of MonadStateReify S M & MonadFailFailR0Reify S M}. -Notation failStateReifyMonad := MonadFailStateReify.type. - -(* -Module MonadFailStateReify. -Record class_of (S : UU0) (M : UU0 -> UU0) := Class { - base : MonadStateReify.class_of S M ; - mixin_fail : MonadFail.mixin_of (Monad.Pack (MonadReify.base (MonadStateReify.base base))) ; - mixin_failReify : @MonadFailReify.mixin_of S (MonadReify.Pack (MonadStateReify.base base)) (@Fail (MonadFail.Pack (MonadFail.Class mixin_fail))) ; - mixin_failR0 : @MonadFailR0.mixin_of (MonadFail.Pack (MonadFail.Class mixin_fail)) ; - }. -Structure type (S : UU0) := Pack { acto : UU0 -> UU0 ; class : class_of S acto }. -Definition failStateMonadType (S : UU0) (M : type S) := MonadStateReify.Pack (base (class M)). -Definition fail_of_failStateReify (S : UU0) (M : type S) := - MonadFail.Pack (MonadFail.Class (mixin_fail (class M))). -Definition failReify_of_failStateReify (S : UU0) (M : type S) := - MonadFailReify.Pack (MonadFailReify.Class (mixin_failReify (class M))). -Definition failR0_of_failStateReify (S : UU0) (M : type S) := - MonadFailR0.Pack (MonadFailR0.Class (mixin_failR0 (class M))). -Definition failFailR0_of_failStateReify (S : UU0) (M : type S) := - MonadFailFailR0Reify.Pack (@MonadFailFailR0Reify.Class _ _ (MonadFailReify.class (failReify_of_failStateReify M)) (mixin_failR0 (class M))). -Module Exports. -Notation failStateReifyMonad := type. -Coercion failStateMonadType : failStateReifyMonad >-> stateReifyMonad. -Canonical failStateMonadType. -Coercion fail_of_failStateReify : failStateReifyMonad >-> failMonad. -Canonical fail_of_failStateReify. -Coercion failReify_of_failStateReify : failStateReifyMonad >-> failReifyMonad. -Canonical failReify_of_failStateReify. -Coercion failR0_of_failStateReify : failStateReifyMonad >-> failR0Monad. -Canonical failR0_of_failStateReify. -Coercion failFailR0_of_failStateReify : failStateReifyMonad >-> failFailR0ReifyMonad. -Canonical failFailR0_of_failStateReify. -End Exports. -End MonadFailStateReify. - -Export MonadFailStateReify.Exports.*) +#[short(type=failFailR0ReifyMonad)] +HB.structure Definition MonadFailFailR0Reify (S : UU0) := + {M of MonadFailReify S M & MonadFailR0 M}. + +#[short(type=failStateReifyMonad)] +HB.structure Definition MonadFailStateReify (S : UU0) := + {M of MonadStateReify S M & MonadFailFailR0Reify S M}. (* NB: this is experimental, may disappear, see rather foreach in -monad_transformer because it is more general *) -HB.mixin Record isMonadStateLoop (S : UU0) (M : UU0 -> UU0) of MonadState S M := { + monad_transformer because it is more general *) +HB.mixin Record isMonadStateLoop (S : UU0) (M : UU0 -> UU0) + of MonadState S M := { foreach : nat -> nat -> (nat -> M unit) -> M unit ; loop0 : forall m body, foreach m m body = Ret tt ; - loop1 : forall m n body, foreach (m.+1 + n) m body = - (body (m + n)) >> foreach (m + n) m body :> M unit }. + loop1 : forall m n body, + foreach (m.+1 + n) m body = (body (m + n)) >> foreach (m + n) m body }. -HB.structure Definition MonadStateLoop (S : UU0) := {M of isMonadStateLoop S M & }. -Notation loopStateMonad := MonadStateLoop.type. +#[short(type=loopStateMonad)] +HB.structure Definition MonadStateLoop (S : UU0) := + {M of isMonadStateLoop S M & }. -HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0) of Monad M := { +HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0) + of Monad M := { aget : I -> M S ; aput : I -> S -> M unit ; aputput : forall i s s', aput i s >> aput i s' = aput i s' ; @@ -1007,29 +994,26 @@ HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0) of Monad M aput i u >> aput j v = aput j v >> aput i u ; aputgetC : forall i j u (A : UU0) (k : S -> M A), i != j -> aput i u >> aget j >>= k = - aget j >>= (fun v => aput i u >> k v) -}. + aget j >>= (fun v => aput i u >> k v) }. +#[short(type=arrayMonad)] HB.structure Definition MonadArray (S : UU0) (I : eqType) := { M of isMonadArray S I M & isMonad M & isFunctor M }. -Notation arrayMonad := MonadArray.type. +#[short(type=plusArrayMonad)] HB.structure Definition MonadPlusArray (S : UU0) (I : eqType) := { M of MonadPlus M & isMonadArray S I M}. -Notation plusArrayMonad := MonadPlusArray.type. -HB.mixin Record isMonadTrace (T : UU0) (M : UU0 -> UU0) of Monad M := { - mark : T -> M unit -}. +HB.mixin Record isMonadTrace (T : UU0) (M : UU0 -> UU0) of Monad M := + { mark : T -> M unit }. +#[short(type=traceMonad)] HB.structure Definition MonadTrace (T : UU0) := {M of isMonadTrace T M & }. -Notation traceMonad := MonadTrace.type. -HB.mixin Record isMonadTraceReify (T : UU0) (M : UU0 -> UU0) of - MonadReify (seq T) M & MonadTrace T M := { +HB.mixin Record isMonadTraceReify (T : UU0) (M : UU0 -> UU0) + of MonadReify (seq T) M & MonadTrace T M := { reifytmark : forall t l, - reify (@mark _ [the traceMonad T of M] t) l = Some (tt, rcons l t) -}. + reify (@mark _ [the traceMonad T of M] t) l = Some (tt, rcons l t) }. HB.mixin Record isMonadStateTrace (S T : UU0) (M : UU0 -> UU0) of Monad M := { st_get : M S ; @@ -1039,29 +1023,31 @@ HB.mixin Record isMonadStateTrace (S T : UU0) (M : UU0 -> UU0) of Monad M := { st_putget : forall s, st_put s >> st_get = st_put s >> Ret s ; st_getputskip : st_get >>= st_put = skip ; st_getget : forall (A : UU0) (k : S -> S -> M A), - st_get >>= (fun s => st_get >>= k s) = st_get >>= fun s => k s s ; + st_get >>= (fun s => st_get >>= k s) = st_get >>= fun s => k s s ; st_putmark : forall s e, st_put s >> st_mark e = st_mark e >> st_put s ; - st_getmark : forall e (k : _ -> M S), st_get >>= (fun v => st_mark e >> k v) = - st_mark e >> st_get >>= k -}. + st_getmark : forall e (k : _ -> M S), + st_get >>= (fun v => st_mark e >> k v) = st_mark e >> st_get >>= k }. +#[short(type=stateTraceMonad)] HB.structure Definition MonadStateTrace (S T : UU0) := { M of isMonadStateTrace S T M & isMonad M & isFunctor M }. -Notation stateTraceMonad := MonadStateTrace.type. HB.mixin Record isMonadStateTraceReify (S T : UU0) (M : UU0 -> UU0) of MonadReify (S * seq T)%type M & MonadStateTrace S T M := { reifystget : forall s l, - reify (@st_get _ _ [the stateTraceMonad S T of M]) (s, l) = Some (s, (s, l)) ; + reify (@st_get _ _ [the stateTraceMonad S T of M]) (s, l) = + Some (s, (s, l)) ; reifystput : forall s l s', - reify (@st_put _ _ [the stateTraceMonad S T of M] s') (s, l) = Some (tt, (s', l)) ; + reify (@st_put _ _ [the stateTraceMonad S T of M] s') (s, l) = + Some (tt, (s', l)) ; reifystmark : forall t s l, - reify (@st_mark _ _ [the stateTraceMonad S T of M] t) (s, l) = Some (tt, (s, rcons l t)) -}. + reify (@st_mark _ _ [the stateTraceMonad S T of M] t) (s, l) = + Some (tt, (s, rcons l t)) }. + +#[short(type=stateTraceReifyMonad)] HB.structure Definition MonadStateTraceReify (S T : UU0) := { M of isMonadStateTraceReify S T M & isFunctor M & isMonad M & isMonadReify S M & isMonadStateTrace S T M }. -Notation stateTraceReifyMonad := MonadStateTraceReify.type. Local Open Scope reals_ext_scope. HB.mixin Record isMonadProb (M : UU0 -> UU0) of Monad M := { @@ -1070,22 +1056,23 @@ HB.mixin Record isMonadProb (M : UU0 -> UU0) of Monad M := { choice0 : forall (T : UU0) (a b : M T), choice 0%:pr _ a b = b ; choice1 : forall (T : UU0) (a b : M T), choice 1%:pr _ a b = a ; (* skewed commutativity *) - choiceC : forall (T : UU0) p (a b : M T), choice p _ a b = choice (p.~ %:pr) _ b a ; + choiceC : forall (T : UU0) p (a b : M T), + choice p _ a b = choice (p.~ %:pr) _ b a ; choicemm : forall (T : UU0) p, idempotent (@choice p T) ; (* quasi associativity *) choiceA : forall (T : UU0) (p q r s : prob) (a b c : M T), (p = r * s :> R /\ s.~ = p.~ * q.~)%R -> - (*NB: needed to preserve the notation in the resulting choiceA lemma, report? *) + (*NB: needed to preserve the notation in the resulting choiceA lemma*) let bc := choice q _ b c in let ab := choice r _ a b in choice p _ a bc = choice s _ ab c; (* composition distributes leftwards over [probabilistic] choice *) - prob_bindDl : forall p, BindLaws.left_distributive (@bind [the monad of M]) (choice p) -}. + prob_bindDl : + forall p, BindLaws.left_distributive (@bind [the monad of M]) (choice p) }. +#[short(type=probMonad)] HB.structure Definition MonadProb := {M of isMonadProb M & }. Notation "a <| p |> b" := (choice p _ a b) : proba_monad_scope. -Notation probMonad := MonadProb.type. Arguments choiceA {_} {_} _ _ _ _ {_} {_} {_}. Arguments choiceC {_} {_} _ _ _. Arguments choicemm {_} {_} _. @@ -1094,20 +1081,20 @@ HB.mixin Record isMonadProbDr (M : UU0 -> UU0) of MonadProb M := { (* composition distributes rightwards over [probabilistic] choice *) (* WARNING: this should not be asserted as an axiom in conjunction with distributivity of <||> over [] *) - prob_bindDr : forall p, BindLaws.right_distributive (@bind [the monad of M]) (choice p) (* NB: not used *) -}. + prob_bindDr : (* NB: not used *) + forall p, BindLaws.right_distributive (@bind [the monad of M]) (choice p) }. +#[short(type=probDrMonad)] HB.structure Definition MonadProbDr := {M of isMonadProbDr M & }. -Notation probDrMonad := MonadProbDr.type. -HB.mixin Record isMonadAltProb (M : UU0 -> UU0) of MonadAltCI M & MonadProb M := { - choiceDr : forall T p, - right_distributive (@choice [the probMonad of M] p T) (fun a b => a [~] b) -}. +HB.mixin Record isMonadAltProb (M : UU0 -> UU0) of MonadAltCI M & MonadProb M := + { choiceDr : forall T p, right_distributive + (@choice [the probMonad of M] p T) (fun a b => a [~] b) }. + +#[short(type=altProbMonad)] HB.structure Definition MonadAltProb := { M of isMonadAltProb M & isFunctor M & isMonad M & isMonadAlt M & isMonadAltCI M & isMonadProb M }. -Notation altProbMonad := MonadAltProb.type. Section altprob_lemmas. Local Open Scope proba_monad_scope. @@ -1117,22 +1104,21 @@ Lemma choiceDl A p : Proof. by move=> x y z; rewrite !(choiceC p) choiceDr. Qed. End altprob_lemmas. -HB.mixin Record isMonadExceptProb (M : UU0 -> UU0) of MonadExcept M & MonadProb M := { +HB.mixin Record isMonadExceptProb (M : UU0 -> UU0) + of MonadExcept M & MonadProb M := { catchDl : forall (A : UU0) w, - left_distributive (@catch [the exceptMonad of M] A) (fun x y => choice w A x y) -}. + left_distributive (@catch [the exceptMonad of M] A) (choice w A) }. +#[short(type=exceptProbMonad)] HB.structure Definition MonadExceptProb := - { M of isMonadExceptProb M & isFunctor M & isMonad M & isMonadFail M & - isMonadExcept M & isMonadProb M }. -Notation exceptProbMonad := MonadExceptProb.type. + { M of isMonadExceptProb M & isFunctor M & isMonad M & isMonadFail M & + isMonadExcept M & isMonadProb M }. -HB.mixin Record isMonadFresh (S : eqType) (M : UU0 -> UU0) of Monad M := { - fresh : M S -}. +HB.mixin Record isMonadFresh (S : eqType) (M : UU0 -> UU0) of Monad M := + { fresh : M S }. +#[short(type=freshMonad)] HB.structure Definition MonadFresh (S : eqType) := {M of isMonadFresh S M & }. -Notation freshMonad:= MonadFresh.type. Module segment_closed. Record t A := mk { @@ -1142,12 +1128,11 @@ End segment_closed. Definition segment_closed_p A := @segment_closed.p A. Coercion segment_closed_p : segment_closed.t >-> pred. -Definition symbols S (M : freshMonad S) := fun n => sequence (nseq n (@fresh _ M)). -Arguments symbols {_} {_}. +Definition symbols {S} {M : freshMonad S} := + fun n => sequence (nseq n (@fresh _ M)). HB.mixin Record isMonadFailFresh (S : eqType) (M : UU0 -> UU0) of MonadFresh S M & MonadFail M := Mixin { -(* symbols := fun n => sequence (nseq n fresh);*) (* generated symbols are indeed fresh (specification of fresh) *) distinct : segment_closed.t S ; bassert_symbols : bassert distinct \o (@symbols _ [the freshMonad S of M]) = @@ -1156,9 +1141,7 @@ HB.mixin Record isMonadFailFresh (S : eqType) (M : UU0 -> UU0) failfresh_bindmfail : BindLaws.right_zero (@bind [the monad of M]) (@fail _) }. +#[short(type=failFreshMonad)] HB.structure Definition MonadFailFresh (S : eqType) := { M of isMonadFailFresh S M & isFunctor M & isMonad M & isMonadFresh S M & isMonadFail M }. -Notation failFreshMonad := MonadFailFresh.type. - -(* HB.graph "hier.dot". *) \ No newline at end of file diff --git a/impredicative_set/ihierarchy.v b/impredicative_set/ihierarchy.v index 073edb87..20e65830 100644 --- a/impredicative_set/ihierarchy.v +++ b/impredicative_set/ihierarchy.v @@ -121,8 +121,8 @@ HB.mixin Record isFunctor (F : UU0 -> UU0) := { functor_id : FunctorLaws.id actm ; functor_o : FunctorLaws.comp actm }. +#[short(type=functor)] HB.structure Definition Functor := {F of isFunctor F}. -Notation functor := Functor.type. Notation "F # g" := (@actm F _ _ g) : monae_scope. Notation "'fmap' f" := (_ # f) : mprog. @@ -192,7 +192,8 @@ Arguments fcomp : simpl never. Lemma functor_ext (F G : functor) : forall (H : Functor.sort F = Functor.sort G), @actm G = - eq_rect _ (fun m : UU0 -> UU0 => forall A B : UU0, (A -> B) -> m A -> m B) (@actm F) _ H -> + eq_rect _ (fun m : UU0 -> UU0 => forall A B : UU0, (A -> B) -> m A -> m B) + (@actm F) _ H -> G = F. Proof. move: F G => [F [[HF1 HF2 HF3]]] [G [[HG1 HG2 HG3]]] /= H. @@ -215,9 +216,9 @@ Arguments naturality : clear implicits. HB.mixin Record isNatural (F G : functor) (f : F ~~> G) := { natural : naturality F G f }. +#[short(type=nattrans)] HB.structure Definition Nattrans (F G : functor) := {f of isNatural F G f}. Arguments natural {F G} s. -Notation nattrans := Nattrans.type. Notation "f ~> g" := (nattrans f g) : monae_scope. Section natrans_lemmas. @@ -292,11 +293,10 @@ HB.mixin Record isMonad (F : UU0 -> UU0) of Functor F := { bind A B m f = join B (([the functor of F] # f) m) ; joinretM : JoinLaws.left_unit ret join ; joinMret : JoinLaws.right_unit ret join ; - joinA : JoinLaws.associativity join -}. + joinA : JoinLaws.associativity join }. +#[short(type=monad)] HB.structure Definition Monad := {F of isMonad F &}. -Notation monad := Monad.type. Arguments bind {s A B} : simpl never. Notation "m >>= f" := (bind m f) : monae_scope. @@ -369,7 +369,8 @@ rewrite fmapE bindA; congr bind. by apply funext => ?; rewrite bindretf. Qed. -Lemma naturality_join : naturality [the functor of F \o F] F (join_of_bind bind). +Lemma naturality_join : + naturality [the functor of F \o F] F (join_of_bind bind). Proof. move=> A B h; apply funext => mma /=. rewrite fmapE /join_of_bind bindA bind_Map; congr bind. @@ -477,7 +478,8 @@ Qed. End monad_lemmas. Notation "'do' x <- m ; e" := (bind m (fun x => e)) (only parsing) : do_notation. -Notation "'do' x : T <- m ; e" := (bind m (fun x : T => e)) (only parsing) : do_notation. +Notation "'do' x : T <- m ; e" := + (bind m (fun x : T => e)) (only parsing) : do_notation. Delimit Scope do_notation with Do. Notation "m >> f" := (bind m (fun _ => f)) : monae_scope. @@ -543,7 +545,8 @@ Proof. case: ifPn => Hb //; by rewrite fmapE bindretf. Qed. Lemma fmap_bind (A B C : UU0) (f : A -> B) m (g : C -> M A) : fmap f (m >>= g) = m >>= (f (o) g). Proof. -rewrite fcomp_def fmapE bindA; bind_ext => c; by rewrite compE -/(fmap _ _) fmapE. +rewrite fcomp_def fmapE bindA; bind_ext => c. +by rewrite compE -/(fmap _ _) fmapE. Qed. Lemma skip_fmap (A B : UU0) (f : A -> B) (mb : M B) ma : @@ -614,16 +617,14 @@ Notation "m >=> n" := (kleisli n m) : monae_scope. HB.mixin Record isMonadFail (M : UU0 -> UU0) of Monad M := { fail : forall A : UU0, M A; - (* exceptions are left-zeros of sequential composition *) - bindfailf : BindLaws.left_zero (@bind [the monad of M]) fail (* fail A >>= f = fail B *) -}. + (* exceptions are left-zeros of sequential composition *) + bindfailf : BindLaws.left_zero (@bind [the monad of M]) fail + (* fail A >>= f = fail B *) }. +#[short(type=failMonad)] HB.structure Definition MonadFail := {M of isMonadFail M & }. -Notation failMonad := MonadFail.type. Arguments bindfailf [_]. - -(*Definition Fail (M : failMonad) := @fail M.*) Arguments fail {_} {_}. Section guard_assert. @@ -647,7 +648,8 @@ Qed. Definition assert {A : UU0} (p : pred A) (a : A) : M A := locked (guard (p a) >> Ret a). -Lemma assertE {A : UU0} (p : pred A) (a : A) : assert p a = guard (p a) >> Ret a. +Lemma assertE {A : UU0} (p : pred A) (a : A) : + assert p a = guard (p a) >> Ret a. Proof. by rewrite /assert; unlock. Qed. Lemma assertT {A : UU0} (a : A) : assert xpredT a = Ret a. @@ -694,46 +696,52 @@ HB.mixin Record isMonadAlt (M : UU0 -> UU0) of Monad M := { (* composition distributes leftwards over choice *) alt_bindDl : BindLaws.left_distributive (@bind [the monad of M]) alt (* in general, composition does not distribute rightwards over choice *) -(* NB: no bindDr to accommodate both angelic and demonic interpretations of nondeterminism *) -}. +(* NB: no bindDr to accommodate both angelic and demonic interpretations of + nondeterminism *) }. +#[short(type=altMonad)] HB.structure Definition MonadAlt := {M of isMonadAlt M & }. Notation "a [~] b" := (@alt _ _ a b). (* infix notation *) -Notation altMonad := MonadAlt.type. - HB.mixin Record isMonadAltCI (M : UU0 -> UU0) of MonadAlt M := { altmm : forall A : UU0, idempotent (@alt [the altMonad of M] A) ; - altC : forall A : UU0, commutative (@alt [the altMonad of M] A) -}. + altC : forall A : UU0, commutative (@alt [the altMonad of M] A) }. +#[short(type=altCIMonad)] HB.structure Definition MonadAltCI := {M of isMonadAltCI M & }. -Notation altCIMonad := MonadAltCI.type. Arguments altC {_} {_}. Arguments altmm {_} {_}. Section altci_lemmas. Variable (M : altCIMonad). + Lemma altCA A : @left_commutative (M A) (M A) (fun x y => x [~] y). Proof. by move=> x y z; rewrite altA altC altA altC (altC x). Qed. + Lemma altAC A : @right_commutative (M A) (M A) (fun x y => x [~] y). Proof. move=> x y z; by rewrite altC altA (altC x). Qed. + Lemma altACA A : @interchange (M A) (fun x y => x [~] y) (fun x y => x [~] y). Proof. move=> x y z t; rewrite !altA; congr (_ [~] _); by rewrite altAC. Qed. + End altci_lemmas. HB.mixin Record isMonadNondet (M : UU0 -> UU0) of MonadFail M & MonadAlt M := { - altfailm : @BindLaws.left_id [the functor of M] (@fail [the failMonad of M]) (@alt [the altMonad of M]); - altmfail : @BindLaws.right_id [the functor of M] (@fail [the failMonad of M]) (@alt [the altMonad of M]) -}. - -HB.structure Definition MonadNondet := {M of isMonadNondet M & MonadFail M & MonadAlt M}. -Notation nondetMonad := MonadNondet.type. - + altfailm : + @BindLaws.left_id [the functor of M] (@fail [the failMonad of M]) + (@alt [the altMonad of M]); + altmfail : + @BindLaws.right_id [the functor of M] (@fail [the failMonad of M]) + (@alt [the altMonad of M]) }. + +#[short(type=nondetMonad)] +HB.structure Definition MonadNondet := + {M of isMonadNondet M & MonadFail M & MonadAlt M}. + +#[short(type=nondetCIMonad)] HB.structure Definition MonadCINondet := {M of MonadAltCI M & MonadNondet M}. -Notation nondetCIMonad := MonadCINondet.type. Section nondet_big. Variables (M : nondetMonad) (A : UU0). @@ -748,22 +756,21 @@ Qed. End nondet_big. -HB.mixin Record isMonadFailR0 (M : UU0 -> UU0) of MonadFail M := { - bindmfail : BindLaws.right_zero (@bind [the monad of M]) (@fail _) -}. +HB.mixin Record isMonadFailR0 (M : UU0 -> UU0) of MonadFail M := + { bindmfail : BindLaws.right_zero (@bind [the monad of M]) (@fail _) }. +#[short(type=failR0Monad)] HB.structure Definition MonadFailR0 := {M of isMonadFailR0 M & }. -Notation failR0Monad := MonadFailR0.type. -HB.mixin Record isMonadPrePlus (M : UU0 -> UU0) of MonadNondet M & MonadFailR0 M := { - alt_bindDr : BindLaws.right_distributive (@bind [the monad of M]) (@alt _) -}. +HB.mixin Record isMonadPrePlus (M : UU0 -> UU0) + of MonadNondet M & MonadFailR0 M := + { alt_bindDr : BindLaws.right_distributive (@bind [the monad of M]) (@alt _) }. +#[short(type=prePlusMonad)] HB.structure Definition MonadPrePlus := {M of isMonadPrePlus M & }. -Notation prePlusMonad := MonadPrePlus.type. +#[short(type=plusMonad)] HB.structure Definition MonadPlus := {M of MonadCINondet M & MonadPrePlus M}. -Notation plusMonad := MonadPlus.type. HB.mixin Record isMonadExcept (M : UU0 -> UU0) of MonadFail M := { catch : forall A, M A -> M A -> M A ; @@ -773,75 +780,77 @@ HB.mixin Record isMonadExcept (M : UU0 -> UU0) of MonadFail M := { catchA : forall A, associative (@catch A) ; (* unexceptional bodies need no handler *) catchret : forall A x, @left_zero (M A) (M A) (Ret x) (@catch A) - (* NB: left-zero of sequential composition inherited from failMonad *) -}. + (* NB: left-zero of sequential composition inherited from failMonad *) }. +#[short(type=exceptMonad)] HB.structure Definition MonadExcept := {M of isMonadExcept M & }. -Notation exceptMonad := MonadExcept.type. -(*Definition Catch (M : exceptMonad) := @catch M.*) Arguments catch {_} {_}. HB.mixin Record isMonadContinuation (M : UU0 -> UU0) of Monad M := { (* NB: interface is wip *) - callcc : forall A B : UU0, ((A -> M B) -> M A) -> M A; - callcc0 : forall (A B : UU0) (g : (A -> M B) -> M A) (k : B -> M B), - @callcc _ _ (fun f => g (fun x => f x >>= k)) = @callcc _ _ g; (* see Sect. 7.2 of [Schrijvers, 19] *) - callcc1 : forall (A B : UU0) (m : M B), @callcc _ _ (fun _ : B -> M A => m) = m ; (* see Sect. 3.3 of [Wadler, 94] *) - callcc2 : forall (A B C : UU0) (m : M A) x (k : A -> B -> M C), - @callcc _ _ (fun f : _ -> M _ => m >>= (fun a => f x >>= (fun b => k a b))) = - @callcc _ _ (fun f : _ -> M _ => m >> f x) ; - callcc3 : forall (A B : UU0) (m : M A) b, - @callcc _ _ (fun f : B -> M B => m >> f b) = - @callcc _ _ (fun _ : B -> M B => m >> Ret b) -}. - + callcc : forall A B : UU0, ((A -> M B) -> M A) -> M A; + callcc0 : forall (A B : UU0) (g : (A -> M B) -> M A) (k : B -> M B), + @callcc _ _ (fun f => g (fun x => f x >>= k)) = @callcc _ _ g + (* see Sect. 7.2 of [Schrijvers, 19] *); + callcc1 : forall (A B : UU0) (m : M B), + @callcc _ _ (fun _ : B -> M A => m) = m + (* see Sect. 3.3 of [Wadler, 94] *); + callcc2 : forall (A B C : UU0) (m : M A) x (k : A -> B -> M C), + @callcc _ _ (fun f : _ -> M _ => m >>= (fun a => f x >>= (fun b => k a b))) + = @callcc _ _ (fun f : _ -> M _ => m >> f x) ; + callcc3 : forall (A B : UU0) (m : M A) b, + @callcc _ _ (fun f : B -> M B => m >> f b) = + @callcc _ _ (fun _ : B -> M B => m >> Ret b) }. + +#[short(type=contMonad)] HB.structure Definition MonadContinuation := {M of isMonadContinuation M & }. -Notation contMonad := MonadContinuation.type. -(*Definition Callcc (M : contMonad) := @callcc M.*) Arguments callcc {_} {_} {_}. -HB.mixin Record isMonadShiftReset (U : UU0) (M : UU0 -> UU0) of MonadContinuation M := { +HB.mixin Record isMonadShiftReset (U : UU0) (M : UU0 -> UU0) + of MonadContinuation M := { shift : forall A : UU0, ((A -> M U) -> M U) -> M A ; reset : M U -> M U ; shiftreset0 : forall (A : UU0) (m : M A), @shift _ (fun k => m >>= k) = m ; (* see Sect. 3.3 of [Wadler, 94] *) - shiftreset1 : forall (A B : UU0) (h : (A -> M B) -> M A), - callcc h = @shift _ (fun k' => h (fun x => @shift _ (fun k'' => k' x)) >>= k') ; + shiftreset1 : forall (A B : UU0) (h : (A -> M B) -> M A), callcc h = + @shift _ (fun k' => h (fun x => @shift _ (fun k'' => k' x)) >>= k') ; (* see Sect. 3.3 of [Wadler, 94] *) shiftreset2 : forall (A : UU0) (c : A) (c': U) (k : A -> U -> _), - (reset (do x <- Ret c; do y <- @shift _ (fun _ => Ret c'); k x y) = Ret c >> Ret c')%Do ; + (reset (do x <- Ret c; do y <- @shift _ (fun _ => Ret c'); k x y) = + Ret c >> Ret c')%Do ; shiftreset3 : forall (c c' : U) (k : U -> U -> _), - (reset (do x <- Ret c; do y <- @shift _ (fun f => do v <- f c'; f v); Ret (k x y)) = - reset (do x <- Ret c; do y <- @shift _ (fun f => f c'); Ret (k x (k x y))))%Do ; + (reset (do x <- Ret c; do y <- @shift _ (fun f => do v <- f c'; f v); + Ret (k x y)) = + reset (do x <- Ret c; do y <- @shift _ (fun f => f c'); + Ret (k x (k x y))))%Do ; shiftreset4 : forall (c : U) k, - (reset (do y <- @shift _ (@^~ c); Ret (k y)) = Ret (k c))%Do -}. + (reset (do y <- @shift _ (@^~ c); Ret (k y)) = Ret (k c))%Do }. +#[short(type=shiftresetMonad)] HB.structure Definition MonadShiftReset U := {M of isMonadShiftReset U M & }. -Notation shiftresetMonad := MonadShiftReset.type. -(*Definition Shift U (M : shiftresetMonad U) := @shift U M.*) Arguments shift {_} {_} {_}. -(*Definition Reset U (M : shiftresetMonad U) := @reset U M. -Arguments Reset {_} {_}.*) (* NB: wip, no model *) (* Sect. 7.2 of [Tom Schrijvers & al., Monad Transformers and Modular Algebraic Effects: What Binds Them Together, Haskell 2019] *) HB.mixin Record isMonadJump (ref : UU0 -> UU0) (M : UU0 -> UU0) of Monad M := { - jump : forall A B : UU0, ref A -> A -> M B; - sub : forall A B : UU0, (ref A -> M B) -> (A -> M B) -> M B; - jump0 : forall (A B : UU0) k x, @sub _ _ (fun r => @jump A B r x) k = k x ; - jump1 : forall (A B : UU0) p k, @sub A B (fun _ => p) k = p; - jump2 : forall (A B : UU0) p r', @sub _ _ p (@jump A B r') = p r'; - jump3 : forall (A B : UU0) (p : ref A -> ref B -> M B) (k1 : A -> M B) k2, - @sub _ _ (fun r1 : ref A => @sub _ _ (fun r2 => p r1 r2) (k2 r1)) k1 = - @sub _ _ (fun r2 : ref B => @sub _ _ (fun r1 => p r1 r2) k1) (fun x => @sub _ _ (k2^~ x) k1); (*NB: differs from [Schrijvers et al. 19]*) - jump4 : forall (A B : UU0) r x k, (@jump A B r x) >>= k = @jump A B r x; - jump5 : forall (A B : UU0) p q k, @sub A B p q >>= k = @sub A B (p >=> k) (q >=> k) -}. + jump : forall A B : UU0, ref A -> A -> M B; + sub : forall A B : UU0, (ref A -> M B) -> (A -> M B) -> M B; + jump0 : forall (A B : UU0) k x, @sub _ _ (fun r => @jump A B r x) k = k x ; + jump1 : forall (A B : UU0) p k, @sub A B (fun _ => p) k = p; + jump2 : forall (A B : UU0) p r', @sub _ _ p (@jump A B r') = p r'; + jump3 : forall (A B : UU0) (p : ref A -> ref B -> M B) (k1 : A -> M B) k2, + @sub _ _ (fun r1 : ref A => @sub _ _ (fun r2 => p r1 r2) (k2 r1)) k1 = + @sub _ _ (fun r2 : ref B => @sub _ _ (fun r1 => p r1 r2) k1) + (fun x => @sub _ _ (k2^~ x) k1) + (*NB: differs from [Schrijvers et al. 19]*); + jump4 : forall (A B : UU0) r x k, (@jump A B r x) >>= k = @jump A B r x; + jump5 : forall (A B : UU0) p q k, + @sub A B p q >>= k = @sub A B (p >=> k) (q >=> k) }. + +#[short(type=jumpMonad)] HB.structure Definition MonadJump ref := {M of isMonadJump ref M & }. -Notation jumpMonad := MonadJump.type. Definition Jump ref (M : jumpMonad ref) := @jump ref M. Arguments Jump {_} {_} {_} {_}. Definition Sub ref (M : jumpMonad ref) := @sub ref M. @@ -856,48 +865,52 @@ HB.mixin Record isMonadState (S : UU0) (M : UU0 -> UU0) of Monad M := { getget : forall (A : UU0) (k : S -> S -> M A), get >>= (fun s => get >>= k s) = get >>= fun s => k s s }. +#[short(type=stateMonad)] HB.structure Definition MonadState (S : UU0) := { M of isMonadState S M & }. -Notation stateMonad := MonadState.type. (*NB: explicit join newly added*) +#[short(type=failStateMonad)] HB.structure Definition MonadFailState (S : UU0) := { M of isMonadFail M & isMonadState S M & isMonad M & isFunctor M }. -Notation failStateMonad := MonadFailState.type. (*NB: explicit join newly added*) +#[short(type=failR0StateMonad)] HB.structure Definition MonadFailR0State (S : UU0) := - { M of isMonadFailR0 M & isMonadState S M & isMonadFail M & isMonad M & isFunctor M }. -Notation failR0StateMonad := MonadFailR0State.type. + { M of isMonadFailR0 M & isMonadState S M & isMonadFail M & isMonad M & + isFunctor M }. +#[short(type=nondetStateMonad)] HB.structure Definition MonadNondetState (S : UU0) := { M of MonadPrePlus M & MonadState S M }. -Notation nondetStateMonad := MonadNondetState.type. HB.mixin Record isMonadStateRun (S : UU0) (N : monad) (M : UU0 -> UU0) of MonadState S M := { runStateT : forall A : UU0, M A -> S -> N (A * S)%type ; - runStateTret : forall (A : UU0) (a : A) (s : S), @runStateT _ (Ret a) s = Ret (a, s) ; + runStateTret : forall (A : UU0) (a : A) (s : S), + @runStateT _ (Ret a) s = Ret (a, s) ; runStateTbind : forall (A B : UU0) (m : M A) (f : A -> M B) (s : S), - @runStateT _ (m >>= f) s = @runStateT _ m s >>= fun x => @runStateT _ (f x.1) x.2 ; + @runStateT _ (m >>= f) s = + @runStateT _ m s >>= fun x => @runStateT _ (f x.1) x.2 ; runStateTget : forall s : S, @runStateT _ get s = Ret (s, s) ; runStateTput : forall s' s : S, @runStateT _ (put s') s = Ret (tt, s') }. +#[short(type=stateRunMonad)] HB.structure Definition MonadStateRun (S : UU0) (N : monad) := {M of isMonadStateRun S N M & }. -Notation stateRunMonad := MonadStateRun.type. Arguments runStateT {_} {_} {_} {_}. -HB.mixin Record isMonadExceptStateRun (S : UU0) (N : exceptMonad) - (M : UU0 -> UU0) of MonadStateRun S N M & MonadExcept M - := Mixin { +HB.mixin Record isMonadExceptStateRun + (S : UU0) (N : exceptMonad) (M : UU0 -> UU0) + of MonadStateRun S N M & MonadExcept M := Mixin { runStateTfail : forall (A : UU0) (s : S), runStateT (@fail [the exceptMonad of M] A) s = @fail N _ ; runStateTcatch : forall (A : UU0) (s : S) (m1 m2 : M A), - runStateT (@catch [the exceptMonad of M] _ m1 m2) s = @catch N _ (runStateT m1 s) (runStateT m2 s) }. + runStateT (@catch [the exceptMonad of M] _ m1 m2) s = + @catch N _ (runStateT m1 s) (runStateT m2 s) }. +#[short(type=exceptStateRunMonad)] HB.structure Definition MonadExceptStateRun (S : UU0) (N : exceptMonad) := {M of isMonadExceptStateRun S N M & }. -Notation exceptStateRunMonad := MonadExceptStateRun.type. HB.mixin Record isMonadReify (S : UU0) (M : UU0 -> UU0) of Monad M := { reify : forall A : UU0, M A -> S -> option (A * S)%type ; @@ -906,81 +919,54 @@ HB.mixin Record isMonadReify (S : UU0) (M : UU0 -> UU0) of Monad M := { @reify _ (m >>= f) s = match @reify _ m s with | Some a's' => @reify _ (f a's'.1) a's'.2 | None => None - end -}. + end }. +#[short(type=reifyMonad)] HB.structure Definition MonadReify (S : UU0) := {M of isMonadReify S M & }. -Notation reifyMonad := MonadReify.type. Arguments reify {_} {_} {_}. -HB.mixin Record isMonadStateReify (S : UU0) (M : UU0 -> UU0) of MonadReify S M & MonadState S M := { +HB.mixin Record isMonadStateReify (S : UU0) (M : UU0 -> UU0) + of MonadReify S M & MonadState S M := { reifyget : forall s, reify (@get _ [the stateMonad S of M]) s = Some (s, s) ; - reifyput : forall s s', reify (@put _ [the stateMonad S of M] s') s = Some (tt, s') -}. + reifyput : forall s s', + reify (@put _ [the stateMonad S of M] s') s = Some (tt, s') }. -HB.structure Definition MonadStateReify (S : UU0) := {M of isMonadStateReify S M &}. -Notation stateReifyMonad := MonadStateReify.type. +#[short(type=stateReifyMonad)] +HB.structure Definition MonadStateReify (S : UU0) := + {M of isMonadStateReify S M &}. -HB.mixin Record isMonadFailReify (S : UU0) (M : UU0 -> UU0) of MonadReify S M & MonadFail M := { - reifyfail : forall S' (s : S), reify (@fail [the failMonad of M] S') s = None -}. +HB.mixin Record isMonadFailReify (S : UU0) (M : UU0 -> UU0) + of MonadReify S M & MonadFail M := + { reifyfail : forall S' (s : S), + reify (@fail [the failMonad of M] S') s = None }. + +#[short(type=failReifyMonad)] +HB.structure Definition MonadFailReify (S : UU0) := + {M of isMonadFailReify S M & }. -HB.structure Definition MonadFailReify (S : UU0) := {M of isMonadFailReify S M & }. -Notation failReifyMonad := MonadFailReify.type. - -HB.structure Definition MonadFailFailR0Reify (S : UU0) := {M of MonadFailReify S M & MonadFailR0 M}. -Notation failFailR0ReifyMonad := MonadFailFailR0Reify.type. - -HB.structure Definition MonadFailStateReify (S : UU0) := {M of MonadStateReify S M & MonadFailFailR0Reify S M}. -Notation failStateReifyMonad := MonadFailStateReify.type. - -(* -Module MonadFailStateReify. -Record class_of (S : UU0) (M : UU0 -> UU0) := Class { - base : MonadStateReify.class_of S M ; - mixin_fail : MonadFail.mixin_of (Monad.Pack (MonadReify.base (MonadStateReify.base base))) ; - mixin_failReify : @MonadFailReify.mixin_of S (MonadReify.Pack (MonadStateReify.base base)) (@Fail (MonadFail.Pack (MonadFail.Class mixin_fail))) ; - mixin_failR0 : @MonadFailR0.mixin_of (MonadFail.Pack (MonadFail.Class mixin_fail)) ; - }. -Structure type (S : UU0) := Pack { acto : UU0 -> UU0 ; class : class_of S acto }. -Definition failStateMonadType (S : UU0) (M : type S) := MonadStateReify.Pack (base (class M)). -Definition fail_of_failStateReify (S : UU0) (M : type S) := - MonadFail.Pack (MonadFail.Class (mixin_fail (class M))). -Definition failReify_of_failStateReify (S : UU0) (M : type S) := - MonadFailReify.Pack (MonadFailReify.Class (mixin_failReify (class M))). -Definition failR0_of_failStateReify (S : UU0) (M : type S) := - MonadFailR0.Pack (MonadFailR0.Class (mixin_failR0 (class M))). -Definition failFailR0_of_failStateReify (S : UU0) (M : type S) := - MonadFailFailR0Reify.Pack (@MonadFailFailR0Reify.Class _ _ (MonadFailReify.class (failReify_of_failStateReify M)) (mixin_failR0 (class M))). -Module Exports. -Notation failStateReifyMonad := type. -Coercion failStateMonadType : failStateReifyMonad >-> stateReifyMonad. -Canonical failStateMonadType. -Coercion fail_of_failStateReify : failStateReifyMonad >-> failMonad. -Canonical fail_of_failStateReify. -Coercion failReify_of_failStateReify : failStateReifyMonad >-> failReifyMonad. -Canonical failReify_of_failStateReify. -Coercion failR0_of_failStateReify : failStateReifyMonad >-> failR0Monad. -Canonical failR0_of_failStateReify. -Coercion failFailR0_of_failStateReify : failStateReifyMonad >-> failFailR0ReifyMonad. -Canonical failFailR0_of_failStateReify. -End Exports. -End MonadFailStateReify. - -Export MonadFailStateReify.Exports.*) +#[short(type=failFailR0ReifyMonad)] +HB.structure Definition MonadFailFailR0Reify (S : UU0) := + {M of MonadFailReify S M & MonadFailR0 M}. + +#[short(type=failStateReifyMonad)] +HB.structure Definition MonadFailStateReify (S : UU0) := + {M of MonadStateReify S M & MonadFailFailR0Reify S M}. (* NB: this is experimental, may disappear, see rather foreach in -monad_transformer because it is more general *) -HB.mixin Record isMonadStateLoop (S : UU0) (M : UU0 -> UU0) of MonadState S M := { + monad_transformer because it is more general *) +HB.mixin Record isMonadStateLoop (S : UU0) (M : UU0 -> UU0) + of MonadState S M := { foreach : nat -> nat -> (nat -> M unit) -> M unit ; loop0 : forall m body, foreach m m body = Ret tt ; - loop1 : forall m n body, foreach (m.+1 + n) m body = - (body (m + n)) >> foreach (m + n) m body :> M unit }. + loop1 : forall m n body, + foreach (m.+1 + n) m body = (body (m + n)) >> foreach (m + n) m body }. -HB.structure Definition MonadStateLoop (S : UU0) := {M of isMonadStateLoop S M & }. -Notation loopStateMonad := MonadStateLoop.type. +#[short(type=loopStateMonad)] +HB.structure Definition MonadStateLoop (S : UU0) := + {M of isMonadStateLoop S M & }. -HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0) of Monad M := { +HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0) + of Monad M := { aget : I -> M S ; aput : I -> S -> M unit ; aputput : forall i s s', aput i s >> aput i s' = aput i s' ; @@ -996,29 +982,26 @@ HB.mixin Record isMonadArray (S : UU0) (I : eqType) (M : UU0 -> UU0) of Monad M aput i u >> aput j v = aput j v >> aput i u ; aputgetC : forall i j u (A : UU0) (k : S -> M A), i != j -> aput i u >> aget j >>= k = - aget j >>= (fun v => aput i u >> k v) -}. + aget j >>= (fun v => aput i u >> k v) }. +#[short(type=arrayMonad)] HB.structure Definition MonadArray (S : UU0) (I : eqType) := { M of isMonadArray S I M & isMonad M & isFunctor M }. -Notation arrayMonad := MonadArray.type. +#[short(type=plusArrayMonad)] HB.structure Definition MonadPlusArray (S : UU0) (I : eqType) := { M of MonadPlus M & isMonadArray S I M}. -Notation plusArrayMonad := MonadPlusArray.type. -HB.mixin Record isMonadTrace (T : UU0) (M : UU0 -> UU0) of Monad M := { - mark : T -> M unit -}. +HB.mixin Record isMonadTrace (T : UU0) (M : UU0 -> UU0) of Monad M := + { mark : T -> M unit }. +#[short(type=traceMonad)] HB.structure Definition MonadTrace (T : UU0) := {M of isMonadTrace T M & }. -Notation traceMonad := MonadTrace.type. -HB.mixin Record isMonadTraceReify (T : UU0) (M : UU0 -> UU0) of - MonadReify (seq T) M & MonadTrace T M := { +HB.mixin Record isMonadTraceReify (T : UU0) (M : UU0 -> UU0) + of MonadReify (seq T) M & MonadTrace T M := { reifytmark : forall t l, - reify (@mark _ [the traceMonad T of M] t) l = Some (tt, rcons l t) -}. + reify (@mark _ [the traceMonad T of M] t) l = Some (tt, rcons l t) }. HB.mixin Record isMonadStateTrace (S T : UU0) (M : UU0 -> UU0) of Monad M := { st_get : M S ; @@ -1028,36 +1011,37 @@ HB.mixin Record isMonadStateTrace (S T : UU0) (M : UU0 -> UU0) of Monad M := { st_putget : forall s, st_put s >> st_get = st_put s >> Ret s ; st_getputskip : st_get >>= st_put = skip ; st_getget : forall (A : UU0) (k : S -> S -> M A), - st_get >>= (fun s => st_get >>= k s) = st_get >>= fun s => k s s ; + st_get >>= (fun s => st_get >>= k s) = st_get >>= fun s => k s s ; st_putmark : forall s e, st_put s >> st_mark e = st_mark e >> st_put s ; - st_getmark : forall e (k : _ -> M S), st_get >>= (fun v => st_mark e >> k v) = - st_mark e >> st_get >>= k -}. + st_getmark : forall e (k : _ -> M S), + st_get >>= (fun v => st_mark e >> k v) = st_mark e >> st_get >>= k }. +#[short(type=stateTraceMonad)] HB.structure Definition MonadStateTrace (S T : UU0) := { M of isMonadStateTrace S T M & isMonad M & isFunctor M }. -Notation stateTraceMonad := MonadStateTrace.type. HB.mixin Record isMonadStateTraceReify (S T : UU0) (M : UU0 -> UU0) of MonadReify (S * seq T)%type M & MonadStateTrace S T M := { reifystget : forall s l, - reify (@st_get _ _ [the stateTraceMonad S T of M]) (s, l) = Some (s, (s, l)) ; + reify (@st_get _ _ [the stateTraceMonad S T of M]) (s, l) = + Some (s, (s, l)) ; reifystput : forall s l s', - reify (@st_put _ _ [the stateTraceMonad S T of M] s') (s, l) = Some (tt, (s', l)) ; + reify (@st_put _ _ [the stateTraceMonad S T of M] s') (s, l) = + Some (tt, (s', l)) ; reifystmark : forall t s l, - reify (@st_mark _ _ [the stateTraceMonad S T of M] t) (s, l) = Some (tt, (s, rcons l t)) -}. + reify (@st_mark _ _ [the stateTraceMonad S T of M] t) (s, l) = + Some (tt, (s, rcons l t)) }. + +#[short(type=stateTraceReifyMonad)] HB.structure Definition MonadStateTraceReify (S T : UU0) := { M of isMonadStateTraceReify S T M & isFunctor M & isMonad M & isMonadReify S M & isMonadStateTrace S T M }. -Notation stateTraceReifyMonad := MonadStateTraceReify.type. -HB.mixin Record isMonadFresh (S : UU0) (M : UU0 -> UU0) of Monad M := { - fresh : M S -}. +HB.mixin Record isMonadFresh (S : UU0) (M : UU0 -> UU0) of Monad M := + { fresh : M S }. +#[short(type=freshMonad)] HB.structure Definition MonadFresh (S : UU0) := {M of isMonadFresh S M & }. -Notation freshMonad:= MonadFresh.type. Module segment_closed. Record t A := mk { @@ -1067,12 +1051,11 @@ End segment_closed. Definition segment_closed_p A := @segment_closed.p A. Coercion segment_closed_p : segment_closed.t >-> pred. -Definition symbols S (M : freshMonad S) := fun n => sequence (nseq n (@fresh _ M)). -Arguments symbols {_} {_}. +Definition symbols {S} {M : freshMonad S} := + fun n => sequence (nseq n (@fresh _ M)). HB.mixin Record isMonadFailFresh (S : UU0) (M : UU0 -> UU0) of MonadFresh S M & MonadFail M := Mixin { -(* symbols := fun n => sequence (nseq n fresh);*) (* generated symbols are indeed fresh (specification of fresh) *) distinct : segment_closed.t S ; bassert_symbols : bassert distinct \o (@symbols _ [the freshMonad S of M]) = @@ -1081,7 +1064,7 @@ HB.mixin Record isMonadFailFresh (S : UU0) (M : UU0 -> UU0) failfresh_bindmfail : BindLaws.right_zero (@bind [the monad of M]) (@fail _) }. +#[short(type=failFreshMonad)] HB.structure Definition MonadFailFresh (S : UU0) := { M of isMonadFailFresh S M & isFunctor M & isMonad M & isMonadFresh S M & isMonadFail M }. -Notation failFreshMonad := MonadFailFresh.type. diff --git a/meta.yml b/meta.yml index d98af9d8..c788c570 100644 --- a/meta.yml +++ b/meta.yml @@ -81,7 +81,7 @@ dependencies: [MathComp analysis](https://github.com/math-comp/analysis) - opam: name: coq-infotheo - version: '{ >= "0.3.5" & < "0.4~"}' + version: '{ >= "0.3.7" & < "0.4~"}' description: |- [Infotheo](https://github.com/affeldt-aist/infotheo) - opam: @@ -91,7 +91,7 @@ dependencies: [Paramcoq](https://github.com/coq-community/paramcoq) - opam: name: coq-hierarchy-builder - version: '{ >= "1.1.0" }' + version: '{ >= "1.2.0" }' description: |- [Hierarchy Builder](https://github.com/math-comp/hierarchy-builder) - opam: diff --git a/parametricity_codensity.v b/parametricity_codensity.v deleted file mode 100644 index af1fe2f6..00000000 --- a/parametricity_codensity.v +++ /dev/null @@ -1,223 +0,0 @@ -(* monae: Monadic equational reasoning in Coq *) -(* Copyright (C) 2020 monae authors, license: LGPL-2.1-or-later *) -Declare ML Module "paramcoq". - -From mathcomp Require Import all_ssreflect. -From HB Require Import structures. -Require Import monae_lib hierarchy monad_lib. -Unset Universe Checking. -Require Import fmt_lifting. -Set Universe Checking. -Require Import monad_model. - -(******************************************************************************) -(* Instantiations of uniform lifting (Theorem 27 of [Mauro Jaskelioff, *) -(* Modular Monad Transformers, ESOP 2009]) with: *) -(* - the identity monad (Module Identity) *) -(* - the exception monad (Module Exception) *) -(* - the option monad (Module Option) *) -(* - the list monad (Module List) *) -(* - the state monad (Module State) *) -(* *) -(* WARNING: see fmt_lifting.v *) -(******************************************************************************) - -Local Open Scope monae_scope. - -Set Bullet Behavior "Strict Subproofs". - -Lemma Actm_exponenial_FE (M : monad) (X Y : UU0) (f : X -> Y) : - forall A eX, ([the functor of (exponential_F A \o M)] # f) eX = M # f \o eX. -Proof. by []. Qed. - -(******************************************************************************) - -Unset Universe Checking. -Module Identity. -Section identity_naturality. -Variable A : UU0. - -Realizer A as A_R := (@eq A). - -Let M := [the monad of idfun]. - -Definition Mi (X : UU0) : UU0 := ltac:( - let t := constr:(M X) in - let t := eval cbn in t in - exact t). - -Definition T : UU0 := MK Mi A. - -Parametricity T arity 2. - -Variable m : T. - -Axiom param : T_R m m. - -Lemma naturality : naturality [the functor of (exponential_F A \o M)] M m. -Proof. -move=> X Y f; rewrite boolp.funeqE => eX. -by apply (param X Y (fun x y => (M # f) x = y)) => a _ <-. -Qed. - -End identity_naturality. -End Identity. -Set Universe Checking. - -Check uniform_sigma_lifting (M := [the monad of idfun])(* _ _ Identity.naturality*). - -(******************************************************************************) - -Unset Universe Checking. -Module Exception. -Section exception_naturality. -Variables Z A : UU0. - -Realizer Z as Z_R := (@eq Z). -Realizer A as A_R := (@eq A). - -Let M := [the monad of ExceptMonad.acto Z]. - -Definition Me (X : UU0) : UU0 := ltac:( - let t := constr:(M X) in - let t := eval cbn in t in - exact t). - -Definition T : UU0 := MK Me A. - -Parametricity Recursive T arity 2. - -Variable m : T. - -Axiom param : T_R m m. - -Lemma naturality : naturality [the functor of (exponential_F A \o M)] M m. -Proof. -move=> X Y f; rewrite boolp.funeqE => eX. -set rhs := RHS. -have : Me_R X Y (fun x y => f x = y) (m X eX) rhs. - apply: param => a _ <-; rewrite Actm_exponenial_FE compE. - by case: (eX a) => [e|x]; constructor. -by rewrite compE; case=> [a _ <-|x _ <-]. -Qed. - -End exception_naturality. -End Exception. -Set Universe Checking. - -Check fun Z => uniform_sigma_lifting - (M := [the monad of ExceptMonad.acto Z]) (*_ _ (Exception.naturality Z)*). - -(******************************************************************************) - -Unset Universe Checking. -Module Option. -Section option_naturality. -Variable A : UU0. - -Let M := [the monad of option_monad]. - -Variable m : MK M A. - -Lemma naturality : naturality [the functor of (exponential_F A \o M)] M m. -Proof. exact: Exception.naturality. Qed. - -End option_naturality. -End Option. -Set Universe Checking. - -Check uniform_sigma_lifting (M := [the monad of option_monad]) (*_ _ Option.naturality*). - -(******************************************************************************) - -Unset Universe Checking. -Module List. -Section list_naturality. -Variable A : UU0. - -Realizer A as A_R := (@eq A). - -Let M := [the monad of ListMonad.acto]. - -Definition Ml (X : UU0) : UU0 := ltac:( - let t := constr:(M X) in - let t := eval cbn in t in - exact t). - -Definition T : UU0 := MK Ml A. - -Parametricity Recursive T arity 2. - -Variable m : T. - -Axiom param : T_R m m. - -Lemma naturality : naturality [the functor of (exponential_F A \o M)] M m. -Proof. -move=> X Y f /=; rewrite boolp.funeqE => eX. -set rhs := RHS. -have : Ml_R X Y (fun x y => f x = y) (m X eX) rhs. - apply: param => a _ <-; rewrite Actm_exponenial_FE compE. - by elim: (eX a) => [|? ? ?]; constructor. -by rewrite compE; elim => // x _ <- l _ _ <-. -Qed. - -End list_naturality. -End List. -Set Universe Checking. - -Check uniform_sigma_lifting (M := [the monad of ListMonad.acto]) (*_ _ List.naturality*). - -(******************************************************************************) - -Unset Universe Checking. -Module State. -Section state_naturality. -Variable S A : UU0. - -Realizer S as S_R := (@eq S). -Realizer A as A_R := (@eq A). - -Let M := [the monad of StateMonad.acto S]. - -Definition Ms X : UU0 := ltac:( - let t := constr:(M X) in - let t := eval cbn in t in - exact t). - -Definition T : UU0 := MK Ms A. - -Parametricity Recursive T arity 2. - -Variable m : T. - -Axiom param : T_R m m. - -Lemma Actm_ModelMonadStateE' (X Y : UU0) (f : X -> Y) (eX : (exponential_F A \o M) X) a (s : S): - (M # f \o eX) a s = let (x, y) := eX a s in (f x, y). -Proof. by []. Qed. - -Lemma Actm_ModelMonadStateE (X Y : UU0) (f : X -> Y) (eX : A -> S -> (X * S)) (s : S) - (mX : (A -> Ms X) -> Ms X) : - (M # f \o mX) eX s = (let (x, y) := mX eX s in (f x, y)). -Proof. by []. Qed. - -Lemma naturality : naturality [the functor of (exponential_F A \o M)] M m. -Proof. -move=> X Y f; rewrite boolp.funeqE => eX. -set rhs := RHS. -have H : Ms_R X Y (fun x y => f x = y) (m X eX) rhs. - apply param => // a _ <- s1 _ <-. - rewrite Actm_exponenial_FE Actm_ModelMonadStateE'. - by case: (eX a) => x s2; exact: prod_R_pair_R. -rewrite boolp.funeqE => s. -have {}H : prod_R X Y (fun x y => f x = y) S S S_R (m X eX s) (rhs s) by exact: H. -inversion H as [x y fxy s1 s2 s12 xs1 ys2]. -by rewrite Actm_ModelMonadStateE -xs1 fxy s12. -Qed. -End state_naturality. -End State. -Set Universe Checking. - -Check fun S => uniform_sigma_lifting - (M := [the monad of StateMonad.acto S]) (*_ _ (State.naturality S)*).