Mini-RFC: have `intros x y z` be `intro x y z; intros`

Stream: lean4

[Kyle Miller]

There's some previous discussion about this, but it's a little hard to search for.

Background

A strange complexity in basic Lean tactics is intros. The intros tactic with no argument introduces all obvious hypotheses, but then intros x y z is the same as intro x y z, while being a little worse since it doesn't support everything intro can do. Plus, it suddenly stops introducing all obvious hypotheses.

Proposed change

I'm proposing here that intros x y z should be a macro for intro x y z; intros. The effect of this is that intros will introduce each of the given hypotheses, even if it takes unfolding, and then introduce all the obvious hypotheses, if any remain.

Benefits and costs

The change to intros has the following benefits:

• Now intros x y z isn't a synonym for intro x y z
• Now writing x in intros x doesn't make all the hypotheses in the local context suddenly disappear, which makes for a less-janky experience
• My impression is that users are confused by the role of intros and will benefit from a clearer distinction between the tactics

It is a breaking change, but the remediation is to use intro instead of intros, which is easy to do. Instances of intros without introducing all obvious hypotheses do occur, but I expect it to be the minority.

Other designs

We could disallow intros-with-arguments and instead require intro x y z; intros. This is makes the distinction between the tactics even clearer, but it's more backwards incompatible, and also it's less convenient than being able to add arguments directly to intros.

We could remove intros and instead have ellipsis syntax on intro, like intro x y z ... One reason not to is that we may want intro x y z .. to be a macro for intro x y z; repeat intro, that is, it would eagerly introduce even non-obvious hypotheses that require the goal to be unfolded. Whichever way ellipses would work, a conservative approach is to change intros itself.

Reference PR

lean4#9943

[Ruben Van de Velde]

I forgot intros was a thing, so I'd go with your last alternative instead. But I'm fine with anything, really

[Yaël Dillies]

Kyle Miller said:

We could remove intros and instead have ellipsis syntax on intro, like intro x y z ... One reason not to is that we may want intro x y z .. to be a macro for intro x y z; repeat intro, that is, it would eagerly introduce even non-obvious hypotheses that require the goal to be unfolded. Whichever way ellipses would work, a conservative approach is to change intros itself.

Stupid suggestion: What about having two ellipses, depending on how unobvious we want the variable introductions to be? I am thinking something like intro x y z .. vs intro x y z ..!

[Yaël Dillies]

Personally, I would much prefer intros goes away entirely, as it would reduce the API surface with little to no loss of functionality in practice (who uses intros? who does so to introduce only non-obvious hypotheses?)

[Kyle Miller]

intros; some_tactic is fairly common. You can find it in many structure/instance fields, as a way to automate some trivial arguments.

The larger question of "should the tactic exist" is valid, but I think that's too disruptive to carry out (at least that will take more time than iI can put into this!). The RFC is low disruption while making the existing tactic more useful, I think.

[Kyle Miller]

The ellipsis variation idea is interesting. There's also messing with with_reducible, though you can't completely disable unfolding that way.

[Chris Henson]

Yaël Dillies said:

Personally, I would much prefer intros goes away entirely, as it would reduce the API surface with little to no loss of functionality in practice (who uses intros? who does so to introduce only non-obvious hypotheses?)

I use intros, though for no particular reason, just muscle memory. It's been around since Lean 3, right? @Kyle Miller could you briefly describe the "being a little bit worse aspect"? I've been using it for years and never really thought about the difference, so maybe I am the target confused user!

[Kyle Miller]

@Chris Henson It's missing patterns, like intro (x, y), and it's missing type ascriptions, like intro (h : p).

Eliminating these small differences -- and avoiding duplicate tactic elaboration code -- is a motivation for this RFC. Another motivation is that intros bugged me again recently :-)

[Chris Henson]

That makes sense, thanks! I then agree with @Yaël Dillies that the ideal would be to eliminate it completely, but given the time/disruption constraints support your idea of making it a macro.

[Eric Wieser]

Could we make it a (lint) error to write intros x y when it means intro x y?

[Eric Wieser]

As an aside, I have an intros? tactic that expands to intro x y

[Patrick Massot]

If you are tweaking intro(s) then could you consider making my dream come true and get rid of the intro vs rintro dichotomy?

[Kyle Miller]

That dream is a bit tough to realize @Patrick Massot, since rintro uses rcases patterns, but intro uses match patterns.

Are there features of rintro that intro could support that would approximate your dream? One that comes to mind is rfl patterns, which intro doesn't have a good analogue for (you can do intro (.refl _), but it can do the wrong thing depending on the whether it's x = 1 or 1 = x).

[Patrick Massot]

I understand those are not the same. The dream is to have a unified version. And indeed the main missing thing is the rfl pattern.

[Kyle Miller]

I know you know the difference :-) What I was intending to mean by this is that the difference looks too big to unify to me. Maybe you have an idea how it could look?

In any case, a version of intro with rfl patterns is on the merge queue. This is potentially a mistake since the rfl patterns can't be used recursively (e.g. intro ⟨rfl, rfl⟩ won't work, just intro rfl) but perhaps it's a step toward match supporting rfl patterns, or toward a unified intro/rintro.

[Kyle Miller]

The biggest gap between rcases patterns and match patterns are the | patterns in rcases.

The difficulty with trying to merge these things is that match patterns are plain Terms. A benefit to them being terms is that there are no subtle parsing differences between terms and patterns; any changes to Term syntax affects both. It's helpful for metaprogramming too, since you don't need to convert a Term to a "Pattern". Plus, any macros defined for Terms apply to patterns as well. (In LoL, Hoyte calls this general principle "duality of syntax"; that section discusses lexical vs dynamic variables, but in the book he tends to use it more generally as "syntax that can be used in multiple contexts with different semantics"). The downside is that every pattern-only syntax must be a Term as well, even if it has no term interpretation. E.g. @ outside of a pattern gives an elaboration error.

It would be nice if there were a way to have a syntax category that's temporarily extensible. Imagine if Pattern were the term category, plus some additional term parsers. The key here is that all the existing term parsers that recursively refer to term would then implicitly be extended with these pattern parsers. It's as if every term parser has an implicit argument for how to parse terms — so parameterized parsers — and then this can be swapped out.

[Kyle Miller]

The reason for thinking in that direction is that | patterns can't be normal terms, since they'd cause issues for | in syntax like match.

However, maybe it's possible to use | anyway: we could make the syntax be "(" term|+ ")", with parentheses. You just wouldn't be able to write things like intro ⟨h1|h1', h2|h2'⟩. It would have to be intro ⟨(h1|h1'), (h2|h2')⟩. Maybe that's better, since then both sorts of pattern syntaxes are bracketed?

[Kyle Miller]

If the syntax were "(" (term?)|+ ")", this syntax could also be used for anonymous constructors, like (h |) and (h |) for Or.inl h and Or.inr h, which is interesting. If there are more than two alternatives, you'd have to be sure to add spaces, like (| | h), since || and ||| are already operators. I'd worry that there are people using brackets out there ((| ... |)) that would be affected.

I guess the notation could special case placeholders instead, like (h | _), instead of using optional terms.

[Jireh Loreaux]

I always write (h₁ | h₂) for clarity anyway.

[neil]

Yaël Dillies said:

who uses intros?

I recently switched over from using Rocq (Coq) to using Lean and wound up using intros because that's what the corresponding rocq tactic is named. Nothing in the intros documentation (at least, what the LSP pulls up) suggests that intro should be used instead of intros, though from reading through this thread, it looks like I should swap over my usages to intro.

[Kyle Miller]

@neil The intros tactic has basically been forgotten for years. I looked deeper into the history, and intros-with-arguments was effectively replaced by intro back in 2020.

Timeline:

• 2014: intros was added to Lean 2, with roughly its current features (though with no arguments it used whnf), and intro x (with only one argument!) was a synonym for intros x. A year later, argument-free intro was introduced.
• 2016: intro and intros were added to Lean 3, and, like Coq, argument-free intros no longer used whnf. Note that Lean 2 and 3 tended to have singular and plural versions of commands (e.g. variable and variables). The intro tactic could only accept zero or one argument, and intros could accept zero or more.
• 2020: Lean 4 got an implementation of intros, which matched the behavior of the Lean 3 tactic. A few months later, intro was generalized to accept any number of arguments. Indeed, in 2021, Lean 4 did away with singular/plural for commands like variable.

[Kyle Miller]

Given the feedback so far, this history, and Lean 4's convergence to the singular, it seems to me that the plan should be to

• implement intro .. or intro * (syntax TBD) to do what intros now does, possibly with some mild reduction (maybe it would be better if it unfolded abbreviations — after all, the implicit lambda feature unfolds the expected type); then
• deprecate intros, leaving it in its current form until it is eventually removed.

[Thomas Murrills]

(If we use .., it would be nice if fun supported it too for consistency/predictability! In fact, I already occasionally find myself reaching for it based on the current usage of ...)