Alternate constructor code action

Stream: lean4

[Oliver Nash]

Kevin highlighted this very nice PR https://github.com/leanprover/std4/pull/577 to me earlier this morning. It makes me wonder if we could ask for even more!

There are various places in Mathlib where we have multiple constructors available for a given structure and it would be lovely if the "generate skeleton" code action could offer the user a choice in such cases.

[Oliver Nash]

So for example in this situation:

import Mathlib

variable {G : Type*} [Group G]

example (H : Subgroup G) : Group H := _

[Oliver Nash]

The code action would provide a little menu allowing me to choose to use docs#Group.ofLeftAxioms and leaving me in the new state:

import Mathlib

variable {G : Type*} [Group G]

example (H : Subgroup G) : Group H :=
  Group.ofLeftAxioms _ _ _

[Oliver Nash]

Any thoughts @Mario Carneiro ?

[Mario Carneiro]

PSA: don't be afraid to ask for features in this regard! The behavior Kevin highlighted is easily solved, the main question is determining what users want in the first place

[Mario Carneiro]

To implement this, we would need some tagging system for "smart constructors"

[Oliver Nash]

@[constructor]?

[Mario Carneiro]

would it work on non-structures?

[Mario Carneiro]

another observation is that we might want to phase out smart constructors in favor of something more like haskell's minimal sets in the future, in which case you wouldn't even need to mention ofLeftAxioms by name

[Oliver Nash]

Mario Carneiro said:

would it work on non-structures?

I don't think I get this point: to me Lean has only three things, def, structure, theorem.

[Mario Carneiro]

right, so would it work on defs

[Mario Carneiro]

I think it would be better (performance-wise) if the answer was 'no'

[Oliver Nash]

I say no, but I might change my mind if someone comes up with an example where this would be desirable.

[Eric Rodriguez]

Mario Carneiro said:

another observation is that we might want to phase out smart constructors in favor of something more like haskell's minimal sets in the future, in which case you wouldn't even need to mention ofLeftAxioms by name

what would this do?

[Mario Carneiro]

I think we might want to have a more extensible notion of what a 'structure' is in the future, such that structure instances and the like work even though they aren't literally inductive types implemented by the structure command

[Mario Carneiro]

for example, coinductive types really need this to be usable

[Eric Rodriguez]

I'm also confused why using lemmas tagged as @[constructor] for non-structures would be slow

[Mario Carneiro]

because it's no good defining a thing which is isomorphic to the coinductive type you want but then tactics like cases and induction totally ignore the inductive-like view and just complain that it has some other implementation detail definition

[Oliver Nash]

Unfortunately I have a call now so I must disappear but I'm already very grateful that this idea is being considered.

[Mario Carneiro]

Eric Rodriguez said:

I'm also confused why using lemmas tagged as @[constructor] for non-structures would be slow

Code actions are performance-sensitive, it's the difference between running this code on every _ and on ones that have structure type

[Eric Rodriguez]

oh, I see, because you need to identify that _ is actually wanting to trigger a code action. Maybe it should have a different syntax? or is it desired that, e.g., refine ?_ ?_ ?_ _ _ would let you run code actions on the end two _s?

[Mario Carneiro]

hole code actions run on any _ or ?_

[Eric Rodriguez]

I think it'd be nice to have @[constructor] on anything, likely with a different signifier for code actions, but I think that's probably way beyond what this feature needs; I think it'd be fine to limit it to structures as-is

[Mario Carneiro]

what else would you use @[constructor] for?

[Eric Rodriguez]

type synonyms are the only things that come to mind quickly, hmm

[Mario Carneiro]

no, I mean what other purpose would you put them to, besides the code action

[Johan Commelin]

@Mario Carneiro Could the code action just be "Fill in a skeleton for _", and only when the user selects it, the code action starts looking up available @[constructor]s?

[Johan Commelin]

That would mean that it could even be an expensive action, because it almost never runs. Only when the user intends it to.

[Mario Carneiro]

no, because code actions don't have staged evaluation

[Mario Carneiro]

you present options, the user selects one, the text is edited

[Johan Commelin]

And we can't hack them to do that?

[Mario Carneiro]

not that I know of

[Johan Commelin]

The text is edited to become (by choose_skeleton). And choose_skeleton is a tactic that displays options in a widget view.

[Eric Rodriguez]

Mario Carneiro said:

no, I mean what other purpose would you put them to, besides the code action

oh I meant some other _-like thing, so as to not slow down normal code actions. Maybe something used more rarely within normal Lean code

[Mario Carneiro]

lol

[Mario Carneiro]

It's not as bad as that @Eric Rodriguez , it only runs on the _ where the cursor is

[Mario Carneiro]

the main performance issue is that it runs on every cursor motion

[Mario Carneiro]

but if you don't put the cursor over a _ then the framework never calls the hole code action

[Oliver Nash]

I say we just declare that this is a structure-only feature then.

[Kevin Buzzard]

As I've said in the other thread, the place where this would be great for me is when undergraduates are making an type with two terms and then attempting to put a group structure on it without being totally bamboozled by (a) DivInvMonoids (which is what happens if you read the source code) or (b) nsmul (which is what happens if you use the code action).

[Kevin Buzzard]

But Chris Hughes wrote some really nice (minimal) constructors for Groupand if we can use those then even better!

[Eric Wieser]

A related feature, when building instances, would be to not generate fields that can be found by inferInstance

[Eric Wieser]

If I've already shown AddCommGroup X I don't want to generate a skeleton with all the fields again when proving NormedGroup X

[Mario Carneiro]

I think the "minimal structure" PR will do that automatically, let me double check

[Mario Carneiro]

it's supposed to yield the same list of fields that you would get in the error message if you omitted everything

[Kevin Buzzard]

Yeah -- I'm pretty sure that's a good strat because it's the one I use in practice when I can't be bothered to delete all the nsmul's

[Eric Wieser]

I think I'm requesting a variant that fills in all the fields that inferInstance implies, but not the ones with default values

[Eric Wieser]

Though maybe that would be better handled by my previous suggestion to replace default values with nsmul := by default or something explicit in the source code that makes it clear that a default is being used behind the scenes

[Matthew Ballard]

It shouldn’t be terrible to log a more informative error during elaboration of the default values. Even with that, there is value in wrapping default values in a tactic