TFAE discussion

Stream: mathlib4

[Jireh Loreaux]

In this GitHub discussion, @Eric Wieser and I were going back and forth about the value of TFAE. (Note: the following discussion will not apply to the PR because I have already delegated it, the point is to have a discussion about TFAE in Mathlib more generally.) To quote some relevant excerpts:

[Jireh Loreaux]

Eric Wieser said:

Personally I don't think TFAE's have any value unless:

• None of the spellings are canonical
• The TFAE makes the proof shorter

My claim is that TFAE's are no good as an API surface because:

• They are unergonomic to use (as you have to refer to the statements by index). This could indeed be addressed by using names, but I don't see foo_tfae.out foo bar being more ergonomic than foo_iff_bar.
• They end up with weird asymmetries. You can't possibly put every foo_iff_$BAR in the same tfae, as some will have import constraints forcing them to be placed in other files.

TFAEs definitely have their place in setting up APIs, but I claim they should be an implementation detail.

[Jireh Loreaux]

Jireh Loreaux said:

I think that our current tooling for TFAE is the problem. I think we at least need a way to name the things in the list so that they can be used with List.TFAE.out

TFAEs have tremendous value from a readability perspective. Even if you have other ↔ statements lying around. This alone is enough to merit writing them, even if the full TFAE only holds under special circumstances (i.e., with sufficiently strong type class assumptions).

Moreover, proving a big TFAE is generally easier because if you have n statements you often only need n distinct tfae_haves, whereas to prove 1 ↔ 2, ..., 1 ↔ n, you need to show 2 * (n - 1) different implications. A TFAE with 3 equivalences is arguably of insufficient value to warrant it, but a TFAE with 5 or more I think is easily worthwhile.

[Jireh Loreaux]

I would like community input here. I can see Eric's argument to some extent (e.g., if there's a canonical spelling, then just prove everything is equivalent to that and use that spelling everywhere), but I still disagree with the totality of the argument. Simply, I think we only need better tooling to make TFAE more useful. And note, I don't claim we should replace all existing ↔ with TFAE; sometimes it's worth having a dedicated ↔ for the most commonly used equivalences.

[Jireh Loreaux]

Just to add one more point in favor of TFAE: it's nice if there is a go-to declaration for all the equivalences instead of trying to find if the library has the particular one you want (or which chain of rws you need to use to get there).

[Eric Wieser]

Thanks for starting this thread; I agree this is beyond the scope of that PR and deserves wider discussion

[Yaël Dillies]

Eric, do you remember that PR of mine where you had a similar comment?

[Jireh Loreaux]

@David Loeffler :up: in case you are interested

[Eric Wieser]

I think the core of my claim is that "TFAE's are no good as an API surface". They are certainly useful as a tool to build an API surface, and indeed can be handy for documentation purposes; but using them in downstream proofs is almost always going to be:

• Less readable; rw [foo_tfae.out 1 2] is not an improvement over rw [<- foo_iff_bar, foo_iff_baz], and something like rw [%tfae_out foo_tfae bar baz] at best breaks even, at the cost of needing clever elaborators.
• Less general; the tfae will assume the strongest typeclass used by all the iffs, whereas if a suitable foo exists it usually needs only weaker ones
• Less symmetric; foo_tfae can't reasoanably contain every equivalent characterization of foo, so at some point you end up with rw [foo_tfae.out 1 0, foo_iff_a_baz_defined_downstream]

[Jireh Loreaux]

Counterpoints:

• if we had naming, then rw [foo_tfae.out bar baz] would be more readable than rw [← foo_iff_bar, foo_iff_baz]
• sometimes you simply already have the generality you need to use any of them (this is very much true in the case of the PR that generated this discussion)
• less symmetric: sometimes, yes, but maybe in those cases a TFAE really isn't appropriate. Or maybe you should just put the TFAE sufficiently far downstream that you get (almost) all of these.

[Eric Wieser]

Yaël Dillies said:

Eric, do you remember that PR of mine where you had a similar comment?

My gmail inbox does, here.

[Eric Wieser]

I don't think rw [foo_tfae.out bar baz] could ever work. We can probably have either rw [foo_tfae.out `bar `baz]`, or `rw [%tfae_out foo_tfae bar baz], where the latter has the advantage that hovering over bar and baz could display the lemma statement

[Jireh Loreaux]

again, that's just a tooling problem. We just need to come up with a way that works. It's not a true argument against using TFAEs.

[Andrew Yang]

I suppose there is no harm in having both TFAE lemmas and also iff lemmas in the mean time?

[Jireh Loreaux]

sure, it's just a discussion about how prevalent TFAEs should be. Of course, even if we have a big TFAE, it still makes sense to have some of the individual ↔, especially as @[simp] lemmas.

[Jireh Loreaux]

I'm not arguing in any way for the abolition of ↔.

[Thomas Murrills]

Maybe the tfae surface should use an environment extension. That way, it’s extensible, and it might be easier to support naming and other kinds of tooling. (It might even be possible to solve the typeclass generality problem to some extent, as we wouldn’t need to actually rely on a single term.)

[Jireh Loreaux]

Thomas, that sounds cool, but I have absolutely no idea how it would work, or if it could be made readable and useable. Would you mind elaborating a bit?

[Thomas Murrills]

Sure! So, here's what I'm envisioning, more or less:

[Thomas Murrills]

When you make a TFAE term, you can add @[tfae foo] to it, where foo is the name of the "tfae group" (so, just analogous to the foo in the name of the term foo_tfae.) If such a foo already exists, you also have to prove a "link" to the existing TFAE.

(Where you prove this is ultimately an implementation/UX detail: do you use @[tfae foo (link := <proof>)], or do you demand it's part of the proven term's overall type somehow? Either way, you give it to the extension, and the extension constructs the overall TFAE term from it.)

Also...

[Thomas Murrills]

...you include the names of the propositions somehow. There are basically three choices here imo: (1) via the @[], e.g. @[tfae foo (names := [bar, baz, ...])], (2) by metadata in the existing TFAE terms, or (3) we change what TFAE terms are such that they have "intrinsic" names even if they're not part of the extension. (I like 3.)

When you want to infer a tfae lemma, you use nice syntax, e.g. infer bar → baz. (We could also then support infer bar ↔︎ baz.) (infer is just a placeholder, though.) This would look in the extension and extract the appropriate lemma.

Note the absence of foo: it would be nice to to try to infer the tfae group from the individual names! Since the extension knows about the names, we can check if there's ambiguity when elaborating—if necessary, or for readability, we'd also support naming the group (e.g. infer bar → baz from foo—or whatever syntax is nicest. Again, just placeholders.).

For potentially handling the typeclass generality...

[Thomas Murrills]

...we could have a feature that lets you "overlap" parts of a TFAE group manually. Honestly, it would be nicest if you didn't have to do this manually, but I'm not sure this is possible (but maybe it is?).

Nonetheless, I'm imagining something roughly like: you prove your general more restricted TFAE lemma that takes advantage of stronger hypotheses and tag it @[tfae foo]; and you prove the subset that relies only on the weaker typeclasses, then write @[tfae foo subset] or something like that. It would maybe use the individual names to figure out how to "align" these, and when you wrote infer bar → baz from foo, it would elaborate using the weaker version if both bar and baz were in the weaker subset, and the stronger version otherwise. Just a partial idea at this point, though.

[Jireh Loreaux]

Just to note: for the typeclass generality, I think you maybe said it backwards. You probably want to prove the general version with weak hypotheses first, then overlap with versions that have stronger hypotheses and more equivalences.

[Thomas Murrills]

That does make more sense! :) (I also mixed up some words about generality—the wording is corrected now, but the content is left as-is.)

[Jireh Loreaux]

What do you do with the situation where file A has @[tfae foo] and file B has @[tfae foo] and then file C imports A and B? I guess we just error and it has to get fixed? (I'm thinking out loud; so half of what I say may be garbage.)

[Thomas Murrills]

Hmm, good question...I guess we could demand that neither of them can initialize the foo group. So if the foo group is initialized in X and then both A and B import and extend it, in principle we could be okay: A's enlargening of the tfae group links up to the initial tfae group from X, and so does B's, so the new things from A and B are still equivalent (by going through the initial group).

But how do we actually get this equivalence? We either: (1) do some import-time computation and construct the broader TFAE term in the extension (I don't know if we get the chance to do this; I think we do though?), or (2) store the additions to a TFAE group separately in the extension (no overall TFAE term), and compute the equivalences needed on the fly when we write infer (by going through the initial group).

[Thomas Murrills]

(So, for example, in the latter case, the extension would have: (1) the initial foo TFAE group from X (2) the TFAE group from A plus a link to the one from X and (3) the TFAE group from B plus a link to the one from X. Then infer bar → baz would construct a path through the groups via the links as necessary.)

[Jireh Loreaux]

I think we should avoid doing computation on import. There's no reason to slow that down.

[Jireh Loreaux]

I really like the draft of the above idea, but it would be good if others would weigh in. :smile:

[Yury G. Kudryashov]

If we get naming, then IMHO we should have automation to generate n(n-1) lemmas foo_iff_bar.

[Jireh Loreaux]

Thomas, for extending, maybe you do something like this:

@[tfae foo_group]
theorem general_tfae : List.TFAE [foo₁, foo₂, foo₃] := sorry

@[tfae bar_group]
theorem special_tfae : List.TFAE [bar₁, bar₂, bar₃] := sorry

tfae bar_group extends foo_group (here you must provide proofs that fooᵢ → barⱼ and barₖ → fooₗ for some i,j,k,l under the hypothese specified by `special_tfae`)

Then the when you write infer foo₂ → bar₃ the extension would lookup the groups containing foo₂ and bar₃, and see that one extends the other. Then it could generate the necessary → on the fly. I'm not sure what to do if foo₂ occurs in both foo_group and bar_group though.

Of course, this doesn't solve the problem of repeated group names, but maybe it's fine if those need to be unique anyway. If infer can get the group names correct anyway, then we shouldn't have to reference them. :fingers_crossed:

[Jireh Loreaux]

Yury, that's a lot of lemmas that we shouldn't even have automation create. If we can generate them on the fly, then what's the point? (I'm open to being convinced otherwise.)

[Thomas Murrills]

Re: extending, is this for the weakening/strengthening notion of overlapping, or for enabling the linking of previously-defined groups? If the former I really like it!

If the latter I think we should first strive to get the group names right from the get-go, so that they're both foo if possible (and so that the foo group originates in a single file imported by everything that uses it); but when that's not possible, or (importantly) when we want to enable linking up two groups that were not proveably equivalent prior to some downstream file, I think we should use a notion of "linking" or "merging" as opposed to extending (since there's no hierarchy involved)! (Should we also get to name the newly-formed supergroup so that stuff can get added to it "directly" (for organizational purposes)?)

Re: potential proposition naming conflicts where fooᵢ appears in two linked groups: maybe names should be implicitly namespaced by the group, and we open all namespaces inside the elaboration of infer? E.g. we have foo.foo₁, but can still write infer foo₁ → ... , and if we have to disambiguate after linking , we can write infer foo.foo₁ → .... This would also keep us from polluting the overall namespace.

[Thomas Murrills]

(It also makes me wonder: why stop at TFAE? :eyes: We could allow adding one-way implications to the extension as well! SCC can be pretty powerful. But sorting that out is definitely for another time.)

[Jireh Loreaux]

Regarding naming: yes, I was assuming TFAE item names would be namespaced within the group and that infer would open these namespaces.

[Jireh Loreaux]

As for linking: I feel like it's much less common to merge two previously unrelated groups than it is to extend by tacking on new equivalences under stronger hypotheses. In other words, I do implicitly think of this as a hierarchy, so in my mind the strengthing / linking are one and the same.

[Jireh Loreaux]

However, to really determine that we'll need a test bed of examples.

[Thomas Murrills]

Gotcha, yeah, if weaker/stronger hypotheses are involved I agree that the hierarchical extends perspective is a good one. :)