underscore variants

Stream: general

[Johan Commelin]

Yesterday I was talking with Reid, and we thought it might be nice if we can have variants on the ever-awesome underscore _.

• _ The good old underscore that does what it currently does
• _₁ An underscore that tells lean: no matter what, whenever this tactic is over, you must have figured out how to assign this meta-variable
• _₂ An underscore that tells lean: no matter what, whenever this tactic is over, you must not assign this meta-variable. It has to become a new goal

We can discuss the notation later. Is this possible? Would others like this?

Here's a reason _₂ might be useful. Now that interactive calc is using refine, some of the underscores in a calc-block will become new goals, and others will be filled in by lean. For readability, it can be very useful to have a visual cue as to which underscores will generate goals that will be filled in later. Currently the visual cue is a comment, but it would be much better if this is tied in to the actual code. After all, comments rot.

[Scott Morrison]

Interesting! I like the idea, but it sounds hard to implement.

How about _. instead of _₁, denoting "this ends here!", and _? instead of _₂, for "this one remains a mystery"?

[Bryan Gin-ge Chen]

_. might be confused with _ followed by .

[Mario Carneiro]

It could also be confused with ._ which means an inaccessible pattern

[Mario Carneiro]

I think I would rather have a new tactic like exact but with _₂ markings

[Mario Carneiro]

rather than using these marks everywhere

[Mario Carneiro]

(this could even be implemented without lean support)

[Johan Commelin]

I would like to keep the notation short (if we are discussing notation anyways) because I want to encourage this to be used in place of _. But first of all, we need to figure out whether this can be implemented.

[Mario Carneiro]

it can be implemented in mathlib easily

[Mario Carneiro]

you make _₂ a notation for id_subgoal _ and then in the exact_with_marked_subgoals tactic (name TBD) you scour the term for these id_subgoal terms, remove them from the input, produce subgoals for them, elaborate the term, double check that the subgoals are still unassigned and add them to the tactic state

[Johan Commelin]

Je ne comprend pas... would you mind translating that to Latin?

[Johan Commelin]

As in... it sounds cool and reasonable, but I have no idea what you are really suggesting.

[Johan Commelin]

Do you want to write a new tactic exact_with_marked_subgoals that should help here?

[Johan Commelin]

Is this going to be a user facing tactic, or is this supposed to be hidden behind notation/api etc...

[Scott Morrison]

I think the idea is that you'd initially write some tactic under a new name, and if it works nicely you could imagine eventually dropping it in as a replacement for the core exact.

[Kevin Buzzard]

Is there some kind of doubles underline in Unicode?

[Mario Carneiro]

I don't think we should change exact or refine. This requires special handling at tactic granularity, so I think it is appropriate to have a new exact/refine combination tactic

[Mario Carneiro]

it sounds like it will mostly only be used for things like calc anyway