make `tfae` tactics a block tactic?

Stream: mathlib4

[Thomas Murrills]

tl;dr I'd like to combine tfae_have and tfae_finish (at least behind the scenes) into a single block tactic instead of two disconnected tactics.

Currently (in mathlib3) the tfae tactics work by having tfae_finish look through all the hypotheses in the context, not just those generated by tfae_have. Is this really necessary (or a good idea)?

In all the examples I’ve looked at so far we use tfae_have to introduce every assumption (so we don’t actually need to use any other assumptions in the context that tfae_finish gathers). (Plus naively it seems like it might mean a lot of defeq checks between types in assumptions and parts of the goal, since we can’t keep track of which assumption connects which two tfae goals.)

We could simplify things if tfae_have and tfae_finish were combined into a single “block tactic” like e.g.

tfae
| 1 → 2 := by …
| 2 → 3 := by …
| 3 → 1 := by …

Also tbh (and perhaps most practically important) a block-like tactic would be easier for me to implement, at least by my current assessment. :sweat_smile:

(Actually we could even keep the lean4-ified version of the old syntax and just make it magically a block tactic:

tfae_have : 1 → 2 := by …
tfae_have : 2 → 3 := by …
tfae_have : 3 → 1 := by …
tfae_finish

where behind the scenes this is all one big syntax node.)

My question here isn’t about the syntax; it’s just about whether it would be okay to change the nature of these tactics to be more of a “single tactic” than separately-called ones.

That is, as long as I can verify that mathlib doesn’t rely on tfae_finish being able to access the full context, and that we never “interrupt” a sequence of tfae_haves with some other tactic for some reason (which would also make it non-block-able).

[Mario Carneiro]

I think it would be best to design the tfae_have and tfae_finish tactics with roughly the behavior they have in lean 3, and then add a tfae block tactic and use mathport to translate to the block tactic form when possible, or use a linter which detects the syntactic pattern and suggests the block tactic

[Mario Carneiro]

Perhaps it should be spelled tfae for the current tfae_finish, and tfae with for the block tactic, for consistency with the lean 4 cases tactic

[Yury G. Kudryashov]

BTW, is it hard to fix mathport so that it doesn't generate very long error messages for proofs that use tfae?

[Yury G. Kudryashov]

https://github.com/leanprover-community/mathlib4/pull/2052/files#diff-2120274c41c22080464ed7c284ab18bb00a8b6c2e202089ba2c2a605c77f455cR1581

[Mario Carneiro]

geez, why aren't people reporting these things

[Mario Carneiro]

that kind of message is always a bug in mathport

[Yury G. Kudryashov]

We started porting files with tfae not so long ago. Deleting 100 lines is easy.

[Mario Carneiro]

yes I know that's what I mean by "why aren't people reporting these things"

[Mario Carneiro]

when you see a bug, report it, don't just work around

[Mario Carneiro]

the output syntax after the 100 lines is also garbage

[Thomas Murrills]

Mario Carneiro said:

I think it would be best to design the tfae_have and tfae_finish tactics with roughly the behavior they have in lean 3, and then add a tfae block tactic and use mathport to translate to the block tactic form when possible, or use a linter which detects the syntactic pattern and suggests the block tactic

sounds reasonable! which should I do first?

the block version is probably easier for me to implement—I can just build the proof directly instead of doing a search through the context. Aside from a test I think it covers everything in mathlib (that is, all uses of tfae_finish are immediately preceded by all necessary tfae_haves) and so would be sufficient for porting, if mathport could handle the change (I can double check this if necessary). but idk if it’s important to have mathlib behavior first

[Mario Carneiro]

mathlib behavior first is definitely important

[Mario Carneiro]

not to mention that with my proposal you would need the non-block structured version anyway

[Mario Carneiro]

@Yury G. Kudryashov tfae construction is fixed on mathport master

[Yury G. Kudryashov]

IMHO, "rewrite in a block structure" is a simple fix. There are only 33 calls to tfae_finish in mathlib.

[Mario Carneiro]

I'm thinking more along the lines of what we want to have eventually, plus preserving compatibility

[Mario Carneiro]

For sure we can encourage block structure, but there are use cases that prefer to avoid block structure, and code outside of mathlib as well which will be translated by mathport after the port

[Mario Carneiro]

it's the same as the situation with cases vs cases'

[Mario Carneiro]

At least, a block structured version of tfae should allow the blocks to be ?_ and filled after the tactic, like cases / induction

[Thomas Murrills]

gotcha, I just thought that if we wanted to speed up the porting that’s happening immediately we’d want a rudimentary (block) version that handled all porting cases, and then we could expand to handle backwards compatibility, ?_ cases, and non-mathlib files like, over the next couple weeks 🙃

[Mario Carneiro]

I think it will be simpler not to refactor this now

[Thomas Murrills]

? what’s the refactor?

[Mario Carneiro]

making tfae a block tactic

[Mario Carneiro]

the mathlib implementation has two tactics with specified semantics

[Mario Carneiro]

this is already implemented in mathport

[Thomas Murrills]

oh you mean so that mathport doesn’t have to change?

[Thomas Murrills]

because all instances of use are basically already in block form, just not internally

[Mario Carneiro]

changing mathport can be done, but I don't think removing tfae_have and tfae_finish entirely is an option

[Mario Carneiro]

we can add another tactic but that's not simplifying things

[Mario Carneiro]

both of these tactics have simple implementations, please don't complicate this

[Mario Carneiro]

refactoring stuff to use a block tactic is easy to do later

[Thomas Murrills]

well, one uses scc which I was hoping to avoid re-implementing for v1

[Yury G. Kudryashov]

If we port all files that have tfae before the tactic is implemented, then compatibility won't be a problem.

[Mario Carneiro]

sure, as I said you don't need that you can use solve_by_elim

[Mario Carneiro]

Yury G. Kudryashov said:

If we port all files that have tfae before the tactic is implemented, then compatibility won't be a problem.

unless tfae is used outside mathlib

[Mario Carneiro]

and even then, what will we use for cases where there are tactics in the middle etc

[Thomas Murrills]

just writing solve_by_elim instead of tfae_finish will work? I’m not really familiar with solve_by_elim, I guess I’ll look it up

[Mario Carneiro]

tfae_finish should be implementable as solve_by_elim with some settings

[Thomas Murrills]

Ok, that sure is easier then lol

[Thomas Murrills]

Ok, basic (mathlib-parity) versions of tfae_have and tfae_finish now exist: !4#2062 (All that's missing from this very basic version is the copyright header and the docstrings—and, of course, more tests, to make sure that they do actually function as intended)

[Thomas Murrills]

(docs are done too now! It's just that copyright header, and I'm not sure how that works exactly :grimacing: Most code is original, but I did take inspiration from a couple existing definitions, such as mathlib's have, and of course the whole thing is a re-implementation of something that existed already...I welcome anyone who knows how to sort that out correctly either telling me "what counts" in principle or, if it's easier simply telling me exactly what the header should be. :sweat_smile: (In this case also feel free to commit it if it speeds things up, as I'll be out of commission for several hours now.))

EDIT: maybe the lint-necessary docs aren’t done, actually, I’m not sure—but the main user-facing docs that people will see on hover are done.

[Mario Carneiro]

Copy the mathlib3 tfae header and add yourself as author

[Thomas Murrills]

If I adapted a function from another file (Have, mathlib version) do I add all of those authors as authors to this file?

[Mario Carneiro]

no

[Thomas Murrills]

alright, we have :check: for v1!

all that we might want to do is rename tfae_finish to tfae, as you mentioned, @Mario Carneiro. Should I go ahead and do that? We just need an #align tfae_finish tfae, right?

EDIT: I re-read what you wrote and I think you might mean something else, right? use tfae(block tactic) to mean just tfae_finish, and tfae with ... for when cases are necessary?

[Mario Carneiro]

no #align is not relevant for tactics. This change would have to be done directly in mathport

[Thomas Murrills]

I see. so do you think we should we change tfae_finish to tfae in this PR or not?

[Jireh Loreaux]

Don't rename now in any case. That can always be done later if it's desired.