feat(tactic/expand_exists): create in namespace & docstring

[0x182d4454fb211940]

expand_exists now creates definitions in the same namespace as the lemma, and allows creating docstrings.

Closes #15723.

---

[0x182d4454fb211940]

It's worth noting this is a breaking change for anyone who was using namespaces. It would be possible to reverse it (i.e. by default use the root namespace, to stay backwards-comptable), but I think this is the obvious behaviour, and I can't see any use of the attribute yet in the master branch.

[0x182d4454fb211940]

The = docstring syntax is used because otherwise it seems like failure is unrecoverable. Calling parser.pexpr when what remains isn't a string (eg @[expand_exists name_a name_b], with cursor between names) brings up an error stating that name_b is an unknown identifier.

[robertylewis]

An alternative syntax -- but this time I'm not sure if it's better -- @[expand_exists [foo "a foo with property bar", bar]]. This should also avoid any pexpr/name ambiguity and is easy enough to parse.

[0x182d4454fb211940]

I haven't tried implementing this yet but I'm a bit torn: it seems cleaner but also slightly more verbose and less like other attribute syntaxes. I guess it would be possible to accept both but I think that just adds maintenance burden. I also imagine your proposed syntax could allow for more features more gracefully in future? Again, I'm unsure.

[robertylewis]

We definitely shouldn't support both = and lists. In favor of the list syntax: lists are already used in some attributes (@[derive [class1, class2]]), and = is not AFAIK. Against the list syntax, in the no-doc-strings case, it clashes with the syntax for e.g. simps (@[simps id1 id2 id3] vs @[expand_exists [id1, id2, id3]]).

Maybe the move is to support both the bare stream of idents (without doc strings at all) and the more verbose list style? Something like parse (ident* <|> list_of ident_with_opt_string), see https://github.com/leanprover-community/lean/blob/22b09be35ef66aece11e6e8f5d114f42b064259b/library/init/meta/interactive_base.lean#L61 .

@digama0 any preference here?

[digama0]

I think the simplest approach would be to simply copy the docstring from the theorem to all generated declarations. That way you don't have to shove a doc string into the middle of an attribute. For lean 4, I would probably be looking at a syntax closer to

expand_exists ⟨
  /-- doc string -/ defn,
  /-- doc string -/ thm
⟩ (param : type) : type -> \exists x, p x := proof

[0x182d4454fb211940]

Perhaps it makes sense for now to use the docstring with the exists lemma by default, allow the = syntax for now to override this, and add a note stating the planned syntax for lean 4?

[eric-wieser]

Whatever choice we make here could be retrospectively applied to simps, since in principle we could want to set docstrings there too.

[0x182d4454fb211940]

@robertylewis Interestingly that worked but only the other way around (trying to parse as a list, then falling back to idents). I don't really understand what would cause this behaviour: is there some intentional design decision behind this?

[0x182d4454fb211940]

@digama0 One other idea is we could have an auto-generated string saying something like "See exists_lemma" provided it has a docstring, though either approach would work. Both are quite easy to implement.

[robertylewis]

Perhaps it makes sense for now to use the docstring with the exists lemma by default, allow the = syntax for now to override this, and add a note stating the planned syntax for lean 4?

I still don't love the = syntax, but this sounds fine to me. It's not really worth quibbling over! I think this is better than

@digama0 One other idea is we could have an auto-generated string saying something like "See exists_lemma" provided it has a docstring, though either approach would work. Both are quite easy to implement.

since it's best for doc strings to be self-contained whenever possible, since they show up in hover tooltips.

[robertylewis]

@robertylewis Interestingly that worked but only the other way around (trying to parse as a list, then falling back to idents). I don't really understand what would cause this behaviour: is there some intentional design decision behind this?

I would have expected it to work either way since an ident can't start with [. Can't say why without playing around with it myself!