lookup_gset_to_gmap: use decide rather than guard

guard is parsing-only notation (which is inherently confusing when comparing the goal state with the Coq sources) and rather rare. decide is a lot more common, and so people are more likely to know how to deal with it.

As I said, I don't strongly care which way we write these lemmas, but we should be consistent. So that means map_filter_lookup and lookup_map_seq and lookup_map_seqZ should change too.

Hm I guess there is a question whether it makes sense to do this for just one of the uses of guard. If we agree guard is confusing we should probably remove it entirely. Or otherwise we should try to find ways to improve it.

• Maybe make the notation also printing?
• I didn't even know about case_option_guard. Instead of having 3 tactics for almost the same thing (case_decide, case_bool_decide, case_option_guard), can we have one tactic for all of them? I think I even tried case_decide when I had my trouble with mguard, but it did not work.

changed the description

Ideally guard would not have a continuation, but should just have type

∀ P `{!Decision P}, M P

Then you can chain it with bind. I think back in the days there was some technical issue preventing this, so we have to try that again.

Separately, instead of having an MGuard typeclass, what about having MFail or Empty, like in the following?

Definition mguard `{Empty (M P), MRet M} P `{Decision P} :=
  match decide P with
  | left H => mret H
  | right _ => mfail
end.

That could subsume option_guard and set_guard. (I first used empty for mfail, but I see adding Empty option := None would be odd).

adding Empty option := None would be odd

Why would that be odd?

I like @Blaisorblade's proposal.

I think having an MFail makes sense, using Empty is a bit like repurposing Singleton for return.

Ralf: My argument is that lawless instances seem problematic, that the laws for Empty come from Set_ or FinMap, and neither is a clear fit for option. Otherwise you risk needing Set Printing All just to find how to reason about the ∅ in your goal. But I thought I was inferring this idea, not making it up...

Robbert: Singleton = MRet isn't that outrageous for collection monads (see elem_of_ret {A} (x y : A) : x ∈@{M A} mret y ↔ x = y;).

And I'd consider extending MonadSet with not_elem_of_fail' : ~(x ∈{M A} mfail), then deriving not_elem_of_fail : x ∈{M A} mfail <-> False.

mentioned in issue #171

Closing in favor of 2 issues (that others can feel free to pick up):

• #170
• #171

closed