affeldt-aist/monae

Monadic effects and equational reasonig in Coq

monae's Issues

Minimization of dependencies

First of all, I would like to thank all the contributors to this library!
For our project, we've been searching for a Coq library of monad theory and among few alternatives we chose monae.
Currently, we need just a basic stuff: basic hierarchy (functors, natural transformations, monads, nondet monads) and basic instances (list, state, etc). We've been really happy to find everything we need in monae.
However, a big list of library dependencies was a bit disappointing.

For example, a dependency on coq-infotheo was surprising, as well as dependencies on mathcomp-fingroup, mathcomp-solvable, etc. From what I understood after a quick pass over the sources, coq-infotheo is used mostly for the probability monad. The boolp.v library from mathcomp-analysis is used heavily for "classical" reasoning. I haven't understood how mathcomp-fingroup, mathcomp-field, etc are used.

Since the monad theory is a cornerstone of PL theory, it would be really nice to have a core library of monad theory with a minimalistic list of dependencies. If you'll be interested in achieving this goal I would be happy to help with this and prepare a PR.

I think there are two possible ways to achieve this:
(1) split the library into two: something like monae-core with a basic hierarchy of monads and common theory,
and e.g. monae-prob with the probability monad
(2) use opam's depopts feature and install various advanced features of the library (e.g. prob monad) only if the user already has all required packages installed.

global notation

monae/hierarchy.v

Line 1168 in 66032e5

Notation "a <| p |> b" := (choice p _ a b).

should be attached to proba_monad_scope

notation broken

The notations on top of hierarchy.bind (>>=, the do notation) seem to be broken with HB.
They parse but do not always display.

document liftM2

monae/monad_lib.v

Line 53 in 3119194

Definition liftM2 {M : monad} (A B C : UU0) (oplus : A -> B -> C) m1 m2 : M C :=

freshMonad should inherit failR0

now that failR0 has been introduced (should be easier with HB)

Remove when available from analysis

monae/gcm_model.v

Lines 659 to 667 in 5bfc22a

	Section move_to_classical_sets_ext.
	Lemma eq_bigcup_cond :
	forall (T U : Type) (P Q : set U) (X Y : U -> set T),
	P = Q -> (forall i, P i -> X i = Y i) -> \bigcup_(i in P) X i = \bigcup_(i in Q) Y i.
	Proof.
	move=> ? ? P Q X Y pq XY.
	by rewrite eqEsubset; split=> x; case=> j; rewrite -?pq=> ?; rewrite -?XY // => ?; eexists j; rewrite -?pq // -XY //.
	Qed.
	End move_to_classical_sets_ext.

A similar lemma should appear in analysis soon. Let us keep this one for a while until it is subsumed
instead of moving it to infotheo.

@t6s

A shorter proof of image_preserves_convex_hull, using Fintype.fin_all_exists

(Put it here because I do not have writing rights, and not really worth forking for just that)

Lemma image_preserves_convex_hull (A B : finType) (f : {affine {dist A} -> {dist B}})
  (Z : set {dist A}) : f @` hull Z = hull (f @` Z).
Proof.
rewrite predeqE => b; split.
  case=> a [n [g [e [Hg]]]] ->{a} <-{b}.
  exists n, (f \o g), e; split.
    move=> b /= [i _] <-{b} /=.
    by exists (g i) => //; apply Hg; exists i.
  by rewrite affine_function_Sum.
case=> n [g [e [Hg]]] ->{b}.
suff [h Hh] : exists h : 'I_n -> dist_convType A, forall i, h i \in Z /\ f (h i) = g i.
  exists (\Sum_e h).
    exists n; exists h; exists e; split => //.
    move=> a [i _] <-.
    move: (Hh i) => [].
    by rewrite in_setE.
  rewrite affine_function_Sum; apply eq_convn => // i /=.
  by case: (Hh i).
apply (@fin_all_exists _ _ (fun i hi => hi \in Z /\ f hi = g i)) => i.
case: (Hg (g i)); first by exists i.
move=> a // HZa Hfa.
exists a; split; by rewrite // in_setE.
Qed.

factory to buil monads from adjoint functors

https://github.com/affeldt-aist/monae/blob/2ff1137336af00f4e1566b8375b328ef561b6ab1/category.v#L960-961

reduce dependency wrt infotheo

monae/monad_model.v

Line 191 in acf8728

by move=> ? ?; rewrite /bind classical_sets_ext.bigcup_of_singleton image_id.

bigcup_of_singleton and bigcup_image will be in the next version of mathcomp-analysis
and this dependency wrt infotheo can be removed

NB: bigcup_of_singleton became bigcup_of_set1

model of array monad

monae/hierarchy.v

Line 1389 in e5b7ecd

Module MonadArray.

move to better location

monae/example_quicksort.v

Line 114 in 3026410

Definition refin (M : altMonad) A (m1 m2 : M A) : Prop := m1 [~] m2 = m2.

might go the fail_lib.v

generalize bind law

monae/hierarchy.v

Line 374 in 56087f1

Definition left_neutral (r : FId ~> M) :=

this does not need to be constrained to the type of natural transformations ~>

@t6s

code duplicated in infotheo

monae/example_array.v

Lines 24 to 43 in 56087f1

	(* TODO: Pr to infotheo *)
	Local Open Scope zarith_ext_scope.
	Reserved Notation "n %:Z" (at level 2, left associativity, format "n %:Z").
	Definition natZ := nosimpl Z_of_nat.
	Notation "n %:Z" := (natZ n) : zarith_ext_scope.
	Notation "z .+1Z" := (Z.succ z) (at level 2, left associativity,
	format "z .+1Z") : zarith_ext_scope.
	Lemma add1Z z : (1 + z)%Z = z.+1Z.
	Proof. by rewrite Z.add_1_l. Qed.
	Lemma natZ0 : 0%:Z = 0%Z. Proof. exact: Nat2Z.inj_0. Qed.
	Lemma natZS n : n.+1%:Z = n%:Z.+1Z.
	Proof. by rewrite -Zpos_P_of_succ_nat. Qed.
	Local Close Scope zarith_ext_scope.
	(* TODO: Pr to infotheo (end) *)

Avoid explicit definition of aliases with HB

using the following pragma

#[short(type="blahType", pack="BlahType")]

non forgetful inheritance detected

monae/category.v

Lines 906 to 907 in 30808b4

	HB.instance Definition _ := isMonad.Build C F bindE joinretM joinMret joinA.
	(* TODO: eliminate Warning: non forgetful inheritance detected *)

monae/category.v

Lines 959 to 961 in 30808b4

	HB.instance Definition monad_of_adjoint_mixin :=
	isMonad.Build C M bindE join_left_unit join_right_unit join_associativity.
	(* TODO: eliminate Warning: non forgetful inheritance detected *)

@t6s

document factories

in hierarchy.v

try using ssrint

monae/example_relabeling.v

Line 6 in 0a28475

From infotheo Require Import ssrZ.

instead of ssrZ.v

Adding monadic fixpoint to define Mu's quicksort

The definition of qperm function in the quicksort branch requires an interaction between fixpoints and binds to show its termination.
Currently there is no such mechanism, and it seems hard to finish the definition.

One possible solution is in http://leventerkok.github.io/papers/mfix.pdf : the monadic fixpoint operator mfix.
Let's see if this mfix can be added to monae with useful laws and if this enables quicksort.

remove notation

monae/example_quicksort.v

Line 106 in 3026410

Reserved Notation "m2 `>=` m1" (at level 70, no associativity).

keep only the <= versions

typo in Record isMonadArray

In Record isMonadArray in hierarchy.v,

  agetpustskip : forall i, aget i >>= aput i = skip ;

this line has a typo: agetpustskip -> agetputskip ?

remove file?

Do we want to keep the file demo_plusMonad.v? @AyumuSaito