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.
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
[Merged by Bors] - feat: tfae
tactics
#2062
Conversation
failure | ||
catch _ => | ||
throwError "couldn't prove {P} → {P'}" | ||
instantiateMVars t |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I'd like to make sure that this instantiateMVars
is in a good place, and check that it isn't needed further downstream.
@thorimur As far as I can tell, this is looking pretty good and stable. If you agree, let's just merge this. If there are small bugs, we can fix them later. bors d+ |
✌️ thorimur can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
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`
Pull request successfully merged into master. Build succeeded: |
We implement a basic version of #2061 to attain mathlib parity:
tfae_have
followed by e.g. a tactic block, in parallel to mathlibhave
syntax (note:tfae_have 1 → 2 := ...
is not supported yet, as it was not supported by the originaltfae_have
tactic, and would constitute new syntax)tfae_finish
, which looks through the local context and simply tries to prove each implication in a cycle viasolve_by_elim