Lift from Option to MetaM

Stream: metaprogramming / tactics

[Heather Macbeth]

There is a lift from Option to MetaM implemented in the norm_num code, apparently dating from #519 (@Mario Carneiro).

I want this elsewhere, so I was thinking of moving it to a standalone file in Mathlib.Util. Does this sound ok?

Is there any part of mathlib where this shouldn't be imported? By the way, Lake.Util.Lift apparently contains a MonadLiftT for this: docs#Lake.instMonadLiftTOptionOfAlternative_lake.

[Kyle Miller]

There's at least docs#Option.toMonad and docs#Option.getDM for turning Option into a monadic value

[Kyle Miller]

I often also write things like let some x := v? | failure

[Heather Macbeth]

OK, would it be better to delete the lift instance in the norm_num code and use one of those idioms instead?

[Eric Wieser]

Is using docs#OptionT another helpful approach here?

[Heather Macbeth]

Kyle's suggestions are fine for my purposes, now I'm just wondering about cleanup elsewhere.

[Damiano Testa]

I have a memory of some very confusing behaviour with the lift instance mentioned above. Let me see if I can find the relevant thread.

[Damiano Testa]

I think that these were the threads that I had in mind:

#mathlib4 > MetaM and Option

#mathlib4 > monad puzzle

[Heather Macbeth]

It seems not very user-friendly to have the presence/absence of the norm_num import determine whether this lift is present or not: this is an unpredictable criterion. Maybe the instance in the norm_num file should be downgraded to a local instance?

[Kyle Miller]

Yes, that seems like a good idea to make it local (or to eliminate it)

[Heather Macbeth]

#18680

[Yaël Dillies]

Oooh, that's why I got errors in my positivity extensions when bumping. What's the preferred fix? Adding the instance locally? Using the let some x := v? | failure idiom?

[Yaël Dillies]

I've added the instance locally, but I'm happy to switch to something else

[Kyle Miller]

It depends on specifics, but let some x := v? | failure (or throwError instead of failure) is a reasonable choice I think.

[Yaël Dillies]

I got a weird error doing that, because my v? contains some ← themselves

[Yaël Dillies]

Turns out I had simply forgotten the trailing | failure