Skip to content

move the bind laws into the basic monad mixin #189

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
t6s wants to merge 1 commit into
base: master
Choose a base branch
from
+118 −114
Open

move the bind laws into the basic monad mixin #189

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 1 addition & 3 deletions theories/applications/monad_composition.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -388,7 +388,5 @@ have @join : [the functor of (T \o S) \o (T \o S)] ~> [the functor of T \o S].
apply: HComp.
exact: f.
exact: NId.
apply: (Monad.Pack (Monad.Class (isMonad.Axioms_ (CRet T S) join _ _ _ _ _))).
move=> A.
rewrite /join.
(* construct monad using (CRet T S) and join... *)
Abort.
228 changes: 117 additions & 111 deletions theories/core/hierarchy.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,10 @@
(* Copyright (C) 2025 monae authors, license: LGPL-2.1-or-later *)
Ltac typeof X := type of X.

Require Import ssrmatching JMeq Morphisms.

Check warning on line 5 in theories/core/hierarchy.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Loading Stdlib without prefix is deprecated.

Check warning on line 5 in theories/core/hierarchy.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

Loading Stdlib without prefix is deprecated.
From mathcomp Require Import all_ssreflect ssralg ssrnum interval_inference.

Check warning on line 6 in theories/core/hierarchy.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

Library File mathcomp.ssreflect.all_ssreflect is deprecated
From mathcomp Require boolp.
From mathcomp Require Import unstable mathcomp_extra reals.

Check warning on line 8 in theories/core/hierarchy.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.5.0-rocq-prover-9.0) 

The unstable.v file should only be used inside analysis.

Check warning on line 8 in theories/core/hierarchy.v

View workflow job for this annotation

GitHub Actions / build (mathcomp/mathcomp:2.4.0-rocq-prover-9.0) 

The unstable.v file should only be used inside analysis.
From infotheo Require Import realType_ext convex.
Require Import preamble.
From HB Require Import structures.
Expand All @@ -29,13 +29,17 @@
(* naturality F G f == the components f form a natural transformation *)
(* F ~> G *)
(* Module JoinLaws == join laws of a monad *)
(* isMonad == mixin of monad *)
(* Module BindLaws == bind laws of a monad *)
(* Functor_isMonad == mixin of monad; has both ret, join and bind laws *)
(* isMonad == compat. factory; = Functor_isMonad - bind laws *)
(* isMonad_ret_join == factory on ret and join *)
(* isMonad_ret_bind == factory on ret and bind; no need of functoriarity *)
(* (i.e., the extension system) *)
(* >>= == notation for the standard bind operator *)
(* m >> f := m >>= (fun _ => f) *)
(* monad == type of monads *)
(* Ret == natural transformation idfun ~> M for a monad M *)
(* Join == natural transformation M \o M ~> M for a monad M *)
(* Module BindLaws == bind laws of a monad *)
(* ``` *)
(* *)
(* Failure and nondeterministic monads: *)
Expand Down Expand Up @@ -167,6 +171,26 @@
Notation "F # g" := (@actm F _ _ g) : monae_scope.
Notation "'fmap' f" := (_ # f) : mprog.

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 ->
G = F.
Proof.
move: F G => [F [[HF1 HF2 HF3]]] [G [[HG1 HG2 HG3]]] /= H.
subst F => /= H.
congr (Functor.Pack (Functor.Class _)).
have ? : HG1 = HF1.
rewrite /actm /= in H.
apply funext_dep => x.
apply funext_dep => y.
apply funext_dep => z.
by move/(congr1 (fun i => i x y z)) : H.
subst HG1.
congr (isFunctor.Axioms_ _); exact/proof_irr.
Defined.

Section functorid.
Let id_actm (A B : UU0) (f : A -> B) : idfun A -> idfun B := f.
Let id_id : FunctorLaws.id id_actm. Proof. by []. Qed.
Expand All @@ -185,6 +209,8 @@
Let comp_id : FunctorLaws.id comp_actm.
Proof. by rewrite /FunctorLaws.id => A; rewrite /comp_actm 2!functor_id. Qed.

(* TODO(bug): `rewrite !functor_o` leads to an infinite loop
(due to expansions of the form `f` = `f \o id`) *)
Let comp_comp : FunctorLaws.comp comp_actm.
Proof.
rewrite /FunctorLaws.comp => A B C g' h; rewrite /comp_actm.
Expand Down Expand Up @@ -225,26 +251,6 @@
Notation "f (o) g" := (fcomp f g) : mprog.
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 ->
G = F.
Proof.
move: F G => [F [[HF1 HF2 HF3]]] [G [[HG1 HG2 HG3]]] /= H.
subst F => /= H.
congr (Functor.Pack (Functor.Class _)).
have ? : HG1 = HF1.
rewrite /actm /= in H.
apply funext_dep => x.
apply funext_dep => y.
apply funext_dep => z.
by move/(congr1 (fun i => i x y z)) : H.
subst HG1.
congr (isFunctor.Axioms_ _); exact/proof_irr.
Defined.

Definition naturality (F G : functor) (f : F ~~> G) :=
forall (A B : UU0) (h : A -> B), (G # h) \o f A = f B \o (F # h).
Arguments naturality : clear implicits.
Expand Down Expand Up @@ -321,41 +327,6 @@
End join_laws.
End JoinLaws.

HB.mixin Record isMonad (F : UU0 -> UU0) of Functor F := {
ret : idfun ~> F ;
join : F \o F ~> F ;
bind : forall (A B : UU0), F A -> (A -> F B) -> F B ;
bindE : forall (A B : UU0) (f : A -> F B) (m : F A),
bind A B m f = join B ((F # f) m) ;
joinretM : JoinLaws.left_unit ret join ;
joinMret : JoinLaws.right_unit ret join ;
joinA : JoinLaws.associativity join }.

#[short(type=monad)]
HB.structure Definition Monad := {F of isMonad F &}.

(* we introduce Ret as a way to make the second arguments of ret implicit,
o.w. Rocq won't let us *)
Notation Ret := (@ret _ _).
Notation Join := (@join _ _).
Arguments bind {s A B} : simpl never.
Notation "m >>= f" := (bind m f) : monae_scope.

Lemma eq_bind (M : monad) (A B : UU0) (m : M A) (f1 f2 : A -> M B) :
f1 =1 f2 -> m >>= f1 = m >>= f2.
Proof. by move=> f12; congr bind; apply boolp.funext. Qed.

Section monad_lemmas.
Variable M : monad.

Lemma fmapE (A B : UU0) (f : A -> B) (m : M A) :
(M # f) m = m >>= (ret B \o f).
Proof.
by rewrite bindE [in RHS]functor_o -[in RHS]compE compA joinMret.
Qed.

End monad_lemmas.

Module BindLaws.
Section bindlaws.
Variable F : UU0 -> UU0.
Expand Down Expand Up @@ -394,40 +365,107 @@
End bindlaws.
End BindLaws.

Definition join_of_bind (F : functor)
(b : forall (A B : UU0), F A -> (A -> F B) -> F B) : F \o F ~~> F :=
fun A : UU0 => (b _ A)^~ id.
HB.mixin Record Functor_isMonad (F : UU0 -> UU0) of Functor F := {
ret : idfun ~> F ;
join : F \o F ~> F ;
bind : forall (A B : UU0), F A -> (A -> F B) -> F B ;
bindE : forall (A B : UU0) (f : A -> F B) (m : F A),
bind A B m f = join B ((F # f) m) ;
joinretM : JoinLaws.left_unit ret join ;
joinMret : JoinLaws.right_unit ret join ;
joinA : JoinLaws.associativity join ;
bindretf : BindLaws.left_neutral bind ret ;
bindmret : BindLaws.right_neutral bind ret ;
bindA : BindLaws.associative bind ;
}.

Definition bind_of_join (F : functor) (j : F \o F ~~> F)
(A B : UU0) (m : F A) (f : A -> F B) : F B :=
j B ((F # f) m).
#[short(type=monad)]
HB.structure Definition Monad := {F of Functor_isMonad F &}.

(* we introduce Ret as a way to make the second arguments of ret implicit,
o.w. Rocq won't let us *)
Notation Ret := (@ret _ _).
Notation Join := (@join _ _).
Arguments bind {s A B} : simpl never.
Notation "m >>= f" := (bind m f) : monae_scope.

Arguments bindretf {s} [A B].
Arguments bindmret {s} [A].
Arguments bindA {s} [A B C].

Section from_join_laws_to_bind_laws.
Variable (F : functor) (ret : idfun ~> F) (join : F \o F ~> F).
HB.factory Record isMonad (F : UU0 -> UU0) of Functor F := {
ret : idfun ~> F ;
join : F \o F ~> F ;
bind : forall (A B : UU0), F A -> (A -> F B) -> F B ;
bindE : forall (A B : UU0) (f : A -> F B) (m : F A),
bind A B m f = join B ((F # f) m) ;
joinretM : JoinLaws.left_unit ret join ;
joinMret : JoinLaws.right_unit ret join ;
joinA : JoinLaws.associativity join }.

HB.builders Context M of isMonad M.

Local Notation "m >>= f" := (bind m f).
Notation Ret := (ret _).

Hypothesis joinretM : JoinLaws.left_unit ret join.
Hypothesis joinMret : JoinLaws.right_unit ret join.
Hypothesis joinA : JoinLaws.associativity join.
Lemma bindE_ext :
bind = fun (A B : UU0) (m : M A) (f : A -> M B) => join B ((M # f) m).
Proof.
do ! apply/funext_dep => ?.
by rewrite bindE.
Qed.

Lemma fmapE (A B : UU0) (f : A -> B) (m : M A) :
(M # f) m = m >>= (ret B \o f).
Proof. by rewrite bindE [in RHS]functor_o -[in RHS]compE compA joinMret. Qed.

Lemma bindretf_derived : BindLaws.left_neutral (bind_of_join join) ret.
Lemma bindretf : BindLaws.left_neutral bind ret.
Proof.
move=> A B a f; rewrite /bind_of_join -(compE (@join _)) -(compE _ (@ret _)).
move=> A B a f.
rewrite bindE -(compE (join _)) -(compE _ (ret _)).
by rewrite -compA (natural ret) compA joinretM compidf.
Qed.

Lemma bindmret_derived : BindLaws.right_neutral (bind_of_join join) ret.
Proof. by move=> A m; rewrite /bind_of_join -(compE (@join _)) joinMret. Qed.
Lemma bindmret : BindLaws.right_neutral bind ret.
Proof. by move=> A m; rewrite bindE -(compE (join _)) joinMret. Qed.

Lemma bindA_derived : BindLaws.associative (bind_of_join join).
Lemma bindA : BindLaws.associative bind.
Proof.
move=> A B C m f g; rewrite /bind_of_join.
rewrite [LHS](_ : _ = ((@join _ \o (F # g \o @join _) \o F # f) m)) //.
rewrite (natural join) (compA (@join C)) -joinA -(compE (@join _)).
transitivity ((@join _ \o F # (@join _ \o (F # g \o f))) m) => //.
by rewrite -2!compA functor_o FCompE -[in LHS](@functor_o F).
move=> A B C m f g; rewrite !bindE_ext.
rewrite [LHS](_ : _ = ((join _ \o (M # g \o join _) \o M # f) m)) //.
rewrite (natural join) (compA (join C)) -joinA -(compE (join _)).
transitivity ((join _ \o M # (join _ \o (M # g \o f))) m) => //.
by rewrite -2!compA functor_o FCompE -[in LHS](@functor_o M).
Qed.

End from_join_laws_to_bind_laws.
HB.instance Definition _ :=
Functor_isMonad.Build M
bindE joinretM joinMret joinA bindretf bindmret bindA.

HB.end.

Lemma eq_bind (M : monad) (A B : UU0) (m : M A) (f1 f2 : A -> M B) :
f1 =1 f2 -> m >>= f1 = m >>= f2.
Proof. by move=> f12; congr bind; apply boolp.funext. Qed.

Section monad_lemmas.
Variable M : monad.

Lemma fmapE (A B : UU0) (f : A -> B) (m : M A) :
(M # f) m = m >>= (ret B \o f).
Proof.
by rewrite bindE [in RHS]functor_o -[in RHS]compE compA joinMret.
Qed.

End monad_lemmas.

Definition join_of_bind (F : functor)
(b : forall (A B : UU0), F A -> (A -> F B) -> F B) : F \o F ~~> F :=
fun A : UU0 => (b _ A)^~ id.

Definition bind_of_join (F : functor) (j : F \o F ~~> F)
(A B : UU0) (m : F A) (f : A -> F B) : F B :=
j B ((F # f) m).

HB.factory Record isMonad_ret_join (F : UU0 -> UU0) of isFunctor F := {
ret : idfun ~> F ;
Expand Down Expand Up @@ -556,38 +594,6 @@
HB.instance Definition _ := isMonad.Build M bindE joinretM joinMret joinA.
HB.end.

Section monad_lemmas.
Variable M : monad.

Lemma bindretf : BindLaws.left_neutral (@bind M) ret.
Proof.
move: (@bindretf_derived M ret join joinretM).
rewrite (_ : bind_of_join _ = @bind M) //.
apply funext_dep => A; apply funext_dep => B.
apply funext_dep => m; apply funext_dep => f.
by rewrite bindE.
Qed.

Lemma bindmret : BindLaws.right_neutral (@bind M) ret.
Proof.
move: (@bindmret_derived M ret join joinMret).
rewrite (_ : bind_of_join _ = @bind M) //.
apply funext_dep => A; apply funext_dep => B.
apply funext_dep => m; apply funext_dep => f.
by rewrite bindE.
Qed.

Lemma bindA : BindLaws.associative (@bind M).
Proof.
move: (@bindA_derived M join joinA).
rewrite (_ : bind_of_join _ = @bind M) //.
apply funext_dep => A; apply funext_dep => B.
apply funext_dep => m; apply funext_dep => f.
by rewrite bindE.
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.
Expand Down
Loading