Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

port and enhance tfae tactics #2061

Open
2 of 3 tasks
thorimur opened this issue Feb 4, 2023 · 3 comments
Open
2 of 3 tasks

port and enhance tfae tactics #2061

thorimur opened this issue Feb 4, 2023 · 3 comments
Labels
t-meta Tactics, attributes or user commands

Comments

@thorimur
Copy link
Collaborator

thorimur commented Feb 4, 2023 •
edited by Komyyy

  • We need to port tfae_have and tfae_finish. We have basic versions for mathlib parity via [Merged by Bors] - feat: tfae tactics #2062.

  • The internals could be made more efficient (e.g. by finding strongly connected components).

  • We'd also like to add a block tactic version of tfae, i.e. tfae with .... using | and =>.
@thorimur thorimur added the t-meta Tactics, attributes or user commands label Feb 4, 2023
@thorimur thorimur mentioned this issue Feb 4, 2023
Closed
@thorimur thorimur linked a pull request Feb 4, 2023 that will close this issue
[Merged by Bors] - feat: tfae tactics #2062
Closed
@thorimur thorimur removed a link to a pull request Feb 5, 2023
[Merged by Bors] - feat: tfae tactics #2062
Closed
bors bot pushed a commit that referenced this issue Feb 21, 2023
@thorimur
feat: tfae tactics (#2062)
1930992 
We implement a basic version of #2061 to attain mathlib parity:
* `tfae_have` followed by e.g. a tactic block, in parallel to mathlib `have` syntax (note: `tfae_have 1 → 2 := ...` is not supported yet, as it was not supported by the original `tfae_have` tactic, and would constitute new syntax)
```
example : TFAE [P, Q, R] := by
  tfae_have h : 1 → 2
  { /- proof of P → Q -/ }
  tfae_have 2 → 3
  { /- proof of Q → R -/ }
  ...
```
* `tfae_finish`, which looks through the local context and simply tries to prove each implication in a cycle via `solve_by_elim`
@urkud
Copy link
Member

urkud commented May 7, 2023

Should we close this issue now?

@thorimur thorimur changed the title port tfae tactics port and enhance tfae tactics May 10, 2023
@thorimur
Copy link
Collaborator Author

Should we close this issue now?

This issue was initially intended to be slightly more general than its original title ("port tfae tactics"); I've adjusted the title and clarified the body accordingly. :)

@Komyyy
Copy link
Collaborator

Komyyy commented May 22, 2023 •
edited

The internals could be made more efficient (e.g. by finding strongly connected components).

This is now #4154.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
t-meta Tactics, attributes or user commands
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
3 participants
@urkud @Komyyy @thorimur