Add `MThrow` and replace `MGuard`

The MR is the result of !488 (closed) and !501 (closed).

This adds the MThrow E M type class expresses the fact that the monad M allow error of type E to be thrown and any point with signature mthrow : E → M A. There is an alias MFail := MThrow unit and mfail := mthrow () for monads that can fail without any error payload like option.

This then replaces mguard with guard : P → {Decision P} → M P using mfail. The original guard notation disappears. As such we've replaced guard P; mx with guard P;; mx in all lemmas. This MR further more replaces case_option_guard with a more general case_guard.

It also adds guard_or : E → P → {Decision P} → M P that throws an E instead of unit if P is false. Technically guard is just a notation for guard_or () like mfail and MFail.

These changes are very much breaking changes.

This is joint work with @adamAndMath.

mentioned in merge request !501 (closed)

The MR is the result of #488 and #501.

If this MR supersedes the other ones, please close those.

mentioned in merge request !488 (closed)

It appears there is a conflict, could you rebase this MR on master?

changed the description

I really like this MR. I left some comments.

added 47 commits

• f3f6e2e8...c57a2eed - 41 commits from branch iris:master
• cb863c03 - Replace `MGuard` with `MFail`
• 525470b4 - Add changelog entries for MFail
• 4e7dd0c8 - Add comment justifying use of bind in lemmas
• a6096703 - Update comment
• 2ba5db95 - Replace MFail by MThrow
• 6a264ef4 - Update changelog for MThrow

Compare with previous version

added 1 commit

• be8b07a1 - Add elem_of_mfail and set_unfold_elem_of_mfail

Compare with previous version

added 6 commits

• 3c515bc1 - Replace `MGuard` with `MFail`
• 6033d66d - Add changelog entries for MFail
• 880fbd0d - Add comment justifying use of bind in lemmas
• 85515295 - Update comment
• 8366ea79 - Update changelog for MThrow
• c797eac6 - Add elem_of_mfail and set_unfold_elem_of_mfail

Compare with previous version

resolved all threads

added 12 commits

• c797eac6...a6387775 - 6 commits from branch iris:master
• dc7ae560 - Replace `MGuard` with `MFail`
• 3314552a - Add changelog entries for MFail
• c3581c7e - Add comment justifying use of bind in lemmas
• 6622416d - Update comment
• 23dbc0db - Update changelog for MThrow
• 3091478a - Add elem_of_mfail and set_unfold_elem_of_mfail

Compare with previous version

added 2 commits

• 2324921e - Update changelog for MThrow
• bcde0cd0 - Add elem_of_mfail and set_unfold_elem_of_mfail

Compare with previous version

Modulo small comments this looks good to me.

added 2 commits

• 7cb3cad0 - Update changelog for MThrow
• 689d93f2 - Add elem_of_mfail and set_unfold_elem_of_mfail

Compare with previous version

added 2 commits

• aa654072 - Update changelog for MThrow
• 81d3831d - Add elem_of_mfail and set_unfold_elem_of_mfail

Compare with previous version

added 1 commit

• 0cd59db8 - Add elem_of_mfail and set_unfold_elem_of_mfail

Compare with previous version

resolved all threads

added 17 commits

• 0cd59db8...47e0eddc - 11 commits from branch iris:master
• daae68d1 - Replace `MGuard` with `MFail`
• 906c8880 - Add changelog entries for MFail
• f7f98438 - Add comment justifying use of bind in lemmas
• a18e35bb - Update comment
• 3f522a4f - Update changelog for MThrow
• 24d4bcfb - Add elem_of_mfail and set_unfold_elem_of_mfail

Compare with previous version

resolved all threads

Going to merge. Thanks a lot @adamAndMath and @tperami !

@iris-users

Add new typeclass MThrow E M to generally represent throwing an error of type E in monad M. (by Thibaut Pérami and Mathias Adam Møller) As a consequence:

• Replace MGuard with MThrow and define guard in terms of MThrow.
• The new guard is an ordinary function, while the old guard was a notation. Hence, use the monadic bind to compose guards. For example, write guard P;; m/p ← guard P; m instead of guard P; m/guard P as p; m.
• Replace the tactic case_option_guard with a more general case_guard version.

merged

mentioned in commit 75a2c419