liftMetaTactic and friends

Stream: lean4

[Thomas Murrills]

The family of liftMetaTactic functions which lift a MetaM "tactic-like" action to TacticM Unit is in a bit of an unfortunate state re: naming:

• liftMetaTactic (tac : MVarId → MetaM (List MVarId)) : TacticM Unit
• liftMetaTactic1 (tac : MVarId → MetaM (Option MVarId)) : TacticM Unit
• liftMetaTactic' (tac : MVarId → MetaM MVarId) : TacticM Unit (Mathlib)
• liftMetaFinishingTactic (tac : MVarId → MetaM Unit) : TacticM Unit

(Is this the only instance of 1 being used in a name to indicate Option/"1 or 0"? :grinning_face_with_smiling_eyes:)

Because of this, if you search for liftMetaTactic in Mathlib, you can see liftMetaTactic being used when another one of these is appropriate fairly often, yielding some extra brackets or lines in the code.

Although I'd be happy with fixing the names of liftMetaTactic1 and liftMetaTactic', there is another option: change the type of liftMetaTactic to work in place of all of these:

class ToGoalList (α) where toGoalList : α → List MVarId

def liftMetaTactic {α} [ToGoalList α] (tac : MVarId → MetaM α) : TacticM Unit := sorry

The advantage of this is that we reduce the small zoo of similarly-named functions in an already-complex API (and reap the benefits that doing so entails).

The disadvantage is that now you can't read off the type of the action from the source as easily, and some actions might typecheck when you don't mean them to. (This is mitigated, I think, by the fact that liftMetaTactic mostly just calls some definition you're aware of the type of, but still ought to be considered.)

I'm curious to hear others' opinions on what would be a nice approach here. :)

[Aaron Liu]

the 1 means it gives at most one goal as output, so yes to indicate Option

[Thomas Murrills]

The (aside) question isn't whether it indicates Option, but whether it's used in any other name to indicate Option/"1 or 0".

[Aaron Liu]

docs#Lean.Meta.saturate1

[Aaron Liu]

I don't see anything else

[Thomas Murrills]

And there, it seems like it indicates Option (Array MVarId), and therefore means…at most 1 Array MVarId? :sweat_smile:

[Thomas Murrills]

(I suppose the idea might be that 1 is for functions of type (_ -> Option _) -> _, but I’m not sure this is a very legible convention.)

[Aaron Liu]

Thomas Murrills said:

And there, it seems like it indicates Option (Array MVarId), and therefore means…at most 1 Array MVarId? :sweat_smile:

Well none is for failure and some [mvarid1, mvarid2, ...] means success and here are your new goals

[Thomas Murrills]

It’s definitely a good type signature (since some #[] means the goal is closed, and is distinct from none)! :) But naming-wise, if this Option is indeed the reason for 1 in the name, I feel like saturate would be sufficient (and the 1 isn’t evoking much).

[Thomas Murrills]

It looks like the difference is actually (mostly) in the return type, going by docs#Lean.Meta.saturate, which returns MetaM (List MVarId). Therefore, I think saturate? might be more conventional for saturate1.

[Eric Wieser]

I worry that your typeclass proposal makes unification harder which seems likely to make do notation emit confusing type errors while you're in the process of writing the function

[Thomas Murrills]

That's fair, though mitigated a bit by the fact that often arguments to liftMetaTactic are short, simple calls to declarations with types that don't need unification.

(I'm actually a bit more worried about how the typeclass approach would create no error in the case of an unfinished do block that returns Unit, thus behaving like liftMetaFinishingTactic unintentionally! :) )

I suppose it comes down to a tradeoff between API complexity and the complexity introduced by "automatic" flexibility (which renders the types less visible/readable, both in error messages and otherwise).

[Thomas Murrills]

I would be happy if we could at least rename these functions and improve the documentation with pointers to the variants, which would be strictly better than the current state. :) (Happy to make those PRs if welcome.)