Zulip Chat Archive

Stream: general

Topic: underscore variants


Johan Commelin (May 29 2020 at 04:50):

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 (May 29 2020 at 05:45):

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 (May 29 2020 at 05:52):

_. might be confused with _ followed by .

Mario Carneiro (May 29 2020 at 06:06):

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

Mario Carneiro (May 29 2020 at 06:07):

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

Mario Carneiro (May 29 2020 at 06:07):

rather than using these marks everywhere

Mario Carneiro (May 29 2020 at 06:08):

(this could even be implemented without lean support)

Johan Commelin (May 29 2020 at 06:36):

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 (May 29 2020 at 06:56):

it can be implemented in mathlib easily

Mario Carneiro (May 29 2020 at 06:58):

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 (May 29 2020 at 07:29):

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

Johan Commelin (May 29 2020 at 07:30):

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

Johan Commelin (May 29 2020 at 07:30):

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

Johan Commelin (May 29 2020 at 07:31):

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

Scott Morrison (May 29 2020 at 07:32):

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 (May 29 2020 at 07:32):

Is there some kind of doubles underline in Unicode?

Mario Carneiro (May 29 2020 at 07:51):

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 (May 29 2020 at 07:52):

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


Last updated: Dec 20 2023 at 11:08 UTC