re-defining monad notations

[vzaliva]

Currently module ITreeNotations re-defines some standard monad notations already defined in ext-lib:

Notation "t1 >>= k2" := (ITree.bind t1 k2)
  (at level 50, left associativity) : itree_scope.
Notation "x <- t1 ;; t2" := (ITree.bind t1 (fun x => t2))
  (at level 61, t1 at next level, right associativity) : itree_scope.
Notation "t1 ;; t2" := (ITree.bind t1 (fun _ => t2))
  (at level 61, right associativity) : itree_scope.
Notation "' p <- t1 ;; t2" :=
  (ITree.bind t1 (fun x_ => match x_ with p => t2 end))
  (at level 61, t1 at next level, p pattern, right associativity) : itree_scope.
Infix ">=>" := ITree.cat (at level 61, right associativity) : itree_scope.

The recent change in ext-lib changed levels for these notations and now they are conflicting with itrees' notations for projects which depend on both (e.g. Vellvm, Helix).

Additionally, this notation in trees is defined as cat while in ext-lib it is mcompose

  Infix ">=>" := ITree.cat (at level 61, right associativity) : itree_scope.

It would be nice to switch to ext-lib notations everywhere.

[Lysxia]

I agree these notations are currently a pain to maintain. I'm strongly considering removing them and just using ext-lib, but we still have to be especially careful about setting the right version bounds because of the recent fluctuations in notations and definitions, which can break our code.

At the moment branch master works only with coq-ext-lib.0.10.3 (unless one is careful to avoid the notation clash).

[Lysxia]

Hm, this is actually somewhat difficult to fix because type classes behave differently with computation. The problem is that cbn reduces @bind _ Monad_itree back to ITree.bind. I tried setting Monad_itree to simpl never, but this blocks proofs by computation. In particular uses of tau_steps in tutorial/Interoduction.v no longer do anything.

• One could redefine tau_steps to manually unfold, but this is pretty tedious.
• Maybe a better thing to do is to refold ITree.bind back to @bind _ Monad_itree, but that seems extremely fragile; it very easily reduces back to ITree.bind.
• One way to make that solution less fragile is to also replace the Monad record with two unwrapped classes for bind and ret.

I have to experiment more with that.

[Lysxia]

• This issue was originally about a mismatch with ext-lib, a bug which had been fixed early on.
• I left it open as a reminder to ditch the custom monad notations.
• However, after some attempts, I still don't see a good way to build the theory around the Monad class from ext-lib. Marking the Monad_itree instance simpl never blocks computation, and when that happens it is really cumbersome to unstick it, because the dictionary might not actually be visible in the goal so you have to find unfold definitions by hand.
• For now I'll mark this resolved.
• To alleviate that problem I mentioned, some automation for rewriting/unfolding could help, but that will be future work.