tfae_have 1 → 2 := syntax

Stream: mathlib4

[Johan Commelin]

This is a tiny feature request for the tfae tactic suite, and it isn't a particularly urgent one.

The current syntax for tfae_have is

  tfae_have 1 → 2
  · -- some proof

For the sake of consistency and brevity, I think it would be great to be able to write

  tfae_have 1 → 2 := -- some proof *term*
  tfae_have 2 → 3 := by
    -- some proof

[Thomas Murrills]

#10653 :)

[Thomas Murrills]

(This is an easy change, so I thought I might as well Just Do It. I'm not officially putting it out for review yet until I look it over tomorrow, but given that the change is relatively small, if someone wants to review it and put it on the queue, feel free. :) )

[Thomas Murrills]

(Ok, now it's out for review—note that half of the PR is just changes to the docs!)

[Thomas Murrills]

Question: should it support tfae_have 1 → 2 := f ?a ?b like have does to prevent any unexpected jolts? I have a commit ready to go which does this, it just complicates things a little.

[Eric Wieser]

Is there a reason it can't fallback to the have tactic and inherit the behavior?

[Thomas Murrills]

Let me see if we can do it without losing the monadic version of the tactic.

[Eric Wieser]

Perhaps also worth noting that the have h : P; tactic syntax seems to be on its way out, in case dropping that makes things notably easier for you

[Johan Commelin]

I think I would be sad to see that syntax be completely removed. I'm happy with a style guide saying that it shouldn't be used. But I can imagine situations where you want to assert 5 haves without proof, and then hand over to a single tactic that works on all goals simultaneously.

[Sébastien Gouëzel]

As a datapoint, #10640 (ready for review, will rot very quickly) is eliminating almost all uses of the old-fashioned have, suffices and replace throughout the library. Among these (2000 lines changed in 438 files), there are exactly zero fancy uses of the kind you're mentioning.

In fact, I would argue against this use, because it would feel to me to be favoring golfing and obfuscation over readability (but I know not everyone shares my feeling against golfing).

[Thomas Murrills]

I thought it might make sense to actually just refactor tfae_have completely in terms of have. This means we have a couple ugly parsers up front to get the parsing to work—but these are almost identical to the ones for have except for simple, obvious changes, so they should be easy to check. (Likewise, later on, what seems like a chunky block of code is actually just repeating very similar one- or two-liners for the different parsing possibilities, completely formulaically.)

This means we now get matching (for →) and destructuring (for Iff) basically for free.

I also thought it made sense to change tfae_have 1 → 2 ... to tfae_have : 1 → 2. (1 → 2 does represent the type, after all!) There were 207 instances of these, so that makes up the bulk of the numbers you see on the top of the PR; I got to remove some code from the actual tactic file. (This could also be changed pretty easily.)

Anyway, this is all just an experiment (and the "Mathlib have" behavior is relegated to a single commit, so can be easily excluded if we like). Let me know what you like and/or don't like. :)

[Yaël Dillies]

Well, 1 → 2 is not a type, right? Maybe if you change the syntax to have : tfae($1 → $2) then you can start arguing it's a type.

[Thomas Murrills]

We write tfae_have h : 1 → 2, though.

[Thomas Murrills]

Does 1 → 2 make sense as anything else but (local) notation for a type?

[Yaël Dillies]

Thomas Murrills said:

We write tfae_have h : 1 → 2, though.

Your message above says tfae_have h : 1 → 2 is the syntax you want to migrate to? So I assume it's not current syntax.

[Yaël Dillies]

Thomas Murrills said:

Does 1 → 2 make sense as anything else but (local) notation for a type?

In a combinatorics class it would most certainly denote Fin 1 → Fin 2 (or rather {1} → {1, 2}, but that's beside the point).

[Thomas Murrills]

No, it is current syntax; that's not the syntax we're migrating to. tfae_have 1 → 2 and tfae_have h : 1 → 2 are the current syntax options. I'm saying we should migrate to tfae_have : 1 → 2 and tfae_have h : 1 → 2.

[Thomas Murrills]

My point is that here, by writing 1 → 2, you really are gesturing to the type P1 → P2 for the propositions P1, P2 in your TFAE, so this really does amount to a (very) local notation for a type!

[Yaël Dillies]

I am claiming that you should use quotes if you really want this analogy to work

[Thomas Murrills]

Why?

[Thomas Murrills]

(Though, btw, I have found a grand total of 0 extant uses of tfae_have h : 1 → 2, so it may as well not exist. :P That's besides the point anyway, though.)

[Yaël Dillies]

because everywhere else in Lean the : α syntax means that α is a type, and 1 → 2 is not a type. It's a type after "processing" it and replacing the 1 and 2 by actual propositions, but it's not a type. And incidentally that "processing, replacing some subexpressions by other subexpressions" sounds exactly like something a quote would do.

[Thomas Murrills]

It sounds to me exactly like something notation would do. :)

[Thomas Murrills]

Like, I guess the thing for me is that it doesn't seem like a technicality: both "spiritually" and literally, 1 → 2 seems like notation for P1 → P2. It undoubtedly gestures to the type P1 → P2, with 1 gesturing to P1 and 2 gesturing to P2 (in this context, anyway—but we're allowed to use the context for interpreting notation!); but also, in a literal sense, we elaborate the num syntax into these expressions.

[Thomas Murrills]

What I can see is that maybe having notation that's only active in a type annotation for tfae_have feels unsavory—personally I'd prioritize communicating the roles of things over banishing "invisible" scopes (tfae_have is indeed there, so it's not totally invisible, but I can still understand its type annotation "feeling unconstrained" by tfae_have, unlike tfae(something)...), but that's ultimately a matter of aesthetics/preferences, and both views are reasonable, I think. :)

[Thomas Murrills]

(Which is why the only solution is to create local OfNat Prop instances.) (I am kidding here, that sounds extremely cursed.)

[Eric Wieser]

Johan Commelin said:

I think I would be sad to see that syntax be completely removed. I'm happy with a style guide saying that it shouldn't be used. But I can imagine situations where you want to assert 5 haves without proof, and then hand over to a single tactic that works on all goals simultaneously.

have : P := ?p should still work for this use-case

[Anatole Dedecker]

By the way, I think at some point there was some mismatch between the numbering inside the proof (starting at 1) and the numbering in TFAE.out (starting at 0). Is that still the case?

[Thomas Murrills]

It looks like it, unfortunately. Btw, @Jireh Loreaux and I are trying to implement a nice interface for accessing and using TFAE statements (see #mathlib4 > TFAE discussion), so that you can simply write something like infer : foo → bar and the right lemma will be extracted for you, so hopefully TFAE.out won't need to be used directly. (We're also eventually considering proposing a change to the TFAE type itself so that it doesn't have to be a simple list, and the lemmas can actually have names, though that's a secondary goal.) Early days, but happening! :)

[Thomas Murrills]

Btw, re: tfae tactic syntax, if we're talking ideals: there's also the option of soon just abandoning tfae_have in favor of some kind of block tactic and/or term, like

  tfae
  | 1 → 2 => pq
  | 2 → 1 => qp
  | 2 ↔ 3 => qr

or something like

  tfae_where
    1 → 2 := pq
    2 → 1 := qp
    2 ↔ 3 := qr

The first looks nicer imo, but the second is really more in keeping with the typical meaning of lean syntax: we're not matching on anything like 1 → 2 (or even a term of that type) and using it in the body; instead, we're providing something like 1 → 2 (like := does). Also, in practice a lot of tfae_haves are followed by intro a b c or exact fun a b c ..., and now we can just write tfae_have : 1 → 2 | a, b, c => ... (with a newline, typically). That's more compatible with the where-like syntax than the => syntax. (tfae where is not a great initial token, though. Maybe just tfae? This could also be given syntax like a structure instance, e.g. TFAE{ 1 → 2 := pq, 2 → 1 := qp .... }. No solid proposal here, just some thoughts.)

It looks like almost every TFAE proves goals in this manner anyway, without using other tactics on the main goal besides tfae_haves before tfae_finish.

This could initially be just a macro over tfae_have and tfae_finish, but could later be optimized further since we have access to all the indices used at once (and don't need to search through the local context).

[Yury G. Kudryashov]

AFAIR, one of these syntaxes was suggested when tfae was ported, but we decided to go with mathlib3 syntax for compatibility reasons.

[Mario Carneiro]

yes, I think it is safe to migrate from tfae_have / tfae_finish to a single tfae tactic now that the port is done

[Thomas Murrills]

Ok! Given that we want to migrate to a block tactic, there's not really any point in using tfae_have : over tfae_have. As such, I've reverted that change in #10653.

Currently #10653 still supports the "Mathlib have"/"old style" syntax. I wonder how we should handle deprecating that syntax (and for that matter, deprecating the old-style have syntax) without causing too much strife for anyone downstream. It does de-document the old-style syntax (i.e. removes mention of it from the dosctring), though.

Likewise, I wonder how to "deprecate" tfae_have/tfae_finish when moving to a block tactic. Currently I simply put a note at the start of the docstring of the old tactics stating that the block tactic is preferred. Maybe that's the best we can do for now? Open to suggestions.

[Johan Commelin]

Thanks for all your work on this!

Can code actions transform one tactic script to another?

[Thomas Murrills]

The sequence of PR's is currently:

• #10653 (awaiting-review): introduce tfae_have ... := syntax
• #11000 (awaiting-review): banish "old-style" tfae_have syntax from mathlib
• #10991 (awaiting-review): introduce a (simply-implemented) tfae block tactic
• #11003 (awaiting-review): transition mathlib to a block tactic

(Note that none of these actually remove functionality.)

[Thomas Murrills]

Johan Commelin said:

Thanks for all your work on this!

Can code actions transform one tactic script to another?

In principle! Hmm...if we wanted a code action coming from tfae_have, the issue might be that we'd have to reach up from the tfae_have syntax to get the rest of the syntax, and organize it all at once. This isn't necessarily an insurmountable issue, though.

[Thomas Murrills]

The syntax I settled on for the block tactic so far is

  tfae
    1 → 2 := /- proof of `P₁ → P₂` -/
    2 → 3 := /- proof of `P₂ → P₃` -/
    3 → 1 := /- proof of `P₃ → P₁` -/

I figured the simplest-possible initial token plus the most semantically consistent field notation was the best bet (see above), but I'm open to other opinions! :)

[Thomas Murrills]

I've been employed and inactive for the past few months, but now that my contract's up (and I've had a bit of a break), I've freshened these PRs, and hope to add to them soon. :)

(I figure the code actions and deprecation are best done in subsequent PRs to keep the PRs (relatively) small and single-purpose, so I've only modified these PRs very slightly.)

[Thomas Murrills]

I'm wondering what the best way to deprecate the old-style tactic syntax is here.

In general, when deprecating syntax, there's a spectrum from "more graceful/lenient deprecation" to "hard deprecation"/"completely breaking change".

We can do a lot to be graceful if we want; the most graceful deprecation (A), I think, involves

1. Preserving the old syntax and implementation in the same import, so old-style code logs a warning but doesn't break
2. Providing a set_option to turn off the warning
3. Providing a code action to transform the syntax

A less graceful deprecation (B) might involve eliminating A.2 and/or A.3, or might look like

1. Moving the old-style implementation to a new file, but
2. Preserving the old syntax in the current import so that it parses, and logging a warning that instructs the user to import the new file if they wish to use it. (This will break the rest of the proof, but still be visible to the user.)

I'm using the term "hard deprecation" (C) to refer to removing both the old syntax and the old implementation from the import hierarchy in such a way that proofs break (fail to parse) with no informative message.

This may or may not also involve maintaining the old-style syntax and implementation in a "leaf" file outside the import hierarchy, like Mathlib-style have.

Note that a staggered deprecation (a graceful deprecation which warns of an impending hard deprecation) is also an option. These possibilities can, of course, be mixed and matched to some extent.

---

I thought I'd outline these options both to make it easier to choose a deprecation path for old-style tfae_have syntax and to provide some public consideration of options for deprecating syntax in general.

[Thomas Murrills]

So, do people have an opinion on how we should deprecate the old-style tfae_have (which is like Mathlib have) in favor of tfae_have ... :=?

tfae_have is, er, not exactly a contender for "most-used tactic", to say the least—so, for example, less graceful deprecations seem to be more acceptable in this instance when balanced against the cost of more graceful deprecations.

There seems to be support on #10653 for moving old-style tfae_have to its own file, which might suggest options (B) or (C). But it's not too onerous to provide option A (excluding A.3—it's a little awkward to provide a reliable code action for this case, since there's no guarantee on how the goals will be handled. You don't even have to prove them immediately!).

After reflection I think I might lean towards A.1 and A.2 instead of what I suggested on the PR.

Thoughts?

[Damiano Testa]

I think that A.1 and A.2 are good choices.

[Damiano Testa]

I do not use tfae at all in the course that I teach, but, if I did, it would be really helpful to get hints on how to modify code so that it keeps working, when updating for the new year.

[Ruben Van de Velde]

How about

1. Land the new syntax next to the old one, no warnings (done in #10653)
2. In one or more PRs, replace the uses in mathlib
3. Add a warning for downstream projects
4. Wait six months
5. Remove the old syntax

[Damiano Testa]

Ruben Van de Velde said:

How about

4. Wait six months a year?

Most teaching is year-based, so six months would unlikely be helpful for updating a course.

[Ruben Van de Velde]

Read "at least" before "six months" :)

[Kim Morrison]

Damiano Testa said:

Ruben Van de Velde said:

How about

4. Wait six months a year?

Most teaching is year-based, so six months would unlikely be helpful for updating a course.

I think people are going to have to get used to bumping to intermediate versions. (e.g. using the v4.X.0 tags on Mathlib). That is too long for us to currently keep deprecations / warnings around.

[Ruben Van de Velde]

Is it?

But yeah, going version by version makes sense

[Thomas Murrills]

Kim Morrison said:

Damiano Testa said:

Ruben Van de Velde said:

How about

4. Wait six months a year?

Most teaching is year-based, so six months would unlikely be helpful for updating a course.

I think people are going to have to get used to bumping to intermediate versions. (e.g. using the v4.X.0 tags on Mathlib). That is too long for us to currently keep deprecations / warnings around.

What does this mean in practical terms for deprecating syntax? Jump straight to a hard deprecation, or provide a warning until some future version?

[Eric Wieser]

I think a deprecation is fine; I don't see why we should treat tactic deprecations that differently to lemma renames

[Thomas Murrills]

Do lemma renames typically get a @[deprecated] attribute? (If so, then you mean we should at least log a deprecation warning to treat them similarly, right?)

[Ruben Van de Velde]

Thomas Murrills said:

Kim Morrison said:

Damiano Testa said:

Ruben Van de Velde said:

How about

4. Wait six months a year?

Most teaching is year-based, so six months would unlikely be helpful for updating a course.

I think people are going to have to get used to bumping to intermediate versions. (e.g. using the v4.X.0 tags on Mathlib). That is too long for us to currently keep deprecations / warnings around.

What does this mean in practical terms for deprecating syntax? Jump straight to a hard deprecation, or provide a warning until some future version?

It means that if v4.11 doesn't support the new syntax yet, v4.12 should print a helpful warning on the old syntax, and it should not be removed before v4.13. Then a downstream project can update from 11 to 12, see and address the warning, and can safely update to 13 without worrying whether the old syntax still works

[Thomas Murrills]

Ah, ok, sounds good. Is there some way of "scheduling" a PR/issue for a later version, or does someone just have to remember to address it again after a while? :)

[Jon Eugster]

theres a label blocked-by-core-release. Maybe lets try to use that and specify in the PR description that it should be merged "after the v4.12.0 bump".

[Thomas Murrills]

I decided to split off the deprecation PR from the syntax migration PR; #11000 only modifies proof syntax (and can be safely merged without causing any warnings/breakages downstream), and #17045 is responsible for actually causing a deprecation warning to be logged. (Wow, 6000+ PRs in between those two!)

Should that warning include something like "this syntax will be removed/moved to its own file(?) when Mathlib bumps to v4.13.0"?

(Am I understanding correctly that adding the deprecation warning on the old syntax (which currently exists alongside the new syntax) in #17045 should also occur on or near a bump if possible? Or is that alright to merge now?)

[Ruben Van de Velde]

No, add the warning asap once mathlib doesn't trigger it anymore

[Thomas Murrills]

Okay, in that case #11000 and #17045 should be merged closely together. :)

[Thomas Murrills]

@Eric Wieser mentioned on #17045 that old-style have is not actually deprecated (and is used in a couple of places), so we shouldn’t deprecate old-style tfae_have.

Here are the options as I see them:

1. Leave the old-style tfae_have syntax in place and not deprecated, possibly with documentation expressing that it’s discouraged.
2. Move the syntax and implementation to its own file off the import hierarchy like Mathlib have, with a warning that this will happen until we do.
3. Just be inconsistent in how we treat tfae_have and have (and deprecate old-style tfae_have) especially since tfae_have is used far less.
4. Deprecate (or simply warn against) both Mathlib have and old-style tfae_have—possibly just in Mathlib, possibly everywhere.

[Thomas Murrills]

Old-style tfae_have syntax is beginning to creep back into Mathlib! :grimacing:

I propose merging #17045 as-is (up to potential review comments): it deprecates the old-style syntax via deprecation warning (preserving functionality) but provides an option to turn the deprecation warning off.

I think providing the ability to use a set_option to turn off the deprecation warning provides enough of an escape hatch (equivalent to sequestering old-style have in its own import) if it's ever truly necessary to use the old-style syntax.

[Thomas Murrills]

I'm happy to make a poll if there's still disagreement, though. (Just thumbs-up this message. :) I'll wait a day for objections then remove the awaiting-zulip tag. Okay, I've removed the tag.)

[Thomas Murrills]

Gently pinging this PR, since even more old-style syntax has crept in since the last time it crept in. :)