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: tactic congr!
and improvement to convert
#2566
Conversation
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.
LGTM
It would be nice to add some tests to the test folder, especially if you think that any of the subfunctions of congr!
are not yet tested in mathlib.
bors d+
✌️ kmill can now approve this pull request. To approve and merge a pull request, simply reply with |
One more remark: |
bors r+ |
This introduces a tactic `congr!` that is an analogue to mathlib 3's `congr'`. It is a more insistent version of `congr` that makes use of more congruence lemmas (including user congruence lemmas), `propext`, `funext`, and `Subsingleton` instances. It also has a feature to lift reflexive relations to equalities. Along with `funext`, the tactic does `intros`, allowing `congr!` to get access to function bodies; the introduced variables can be named using `rename_i` if needed. This also modifies `convert` to use `congr!` rather than `congr`, which makes it work more like the mathlib3 version of the tactic.
Timed out. |
There's nothing on the queue right now, so I guess I'll try again and hope timing out was just a fluke? bors r+ |
This introduces a tactic `congr!` that is an analogue to mathlib 3's `congr'`. It is a more insistent version of `congr` that makes use of more congruence lemmas (including user congruence lemmas), `propext`, `funext`, and `Subsingleton` instances. It also has a feature to lift reflexive relations to equalities. Along with `funext`, the tactic does `intros`, allowing `congr!` to get access to function bodies; the introduced variables can be named using `rename_i` if needed. This also modifies `convert` to use `congr!` rather than `congr`, which makes it work more like the mathlib3 version of the tactic.
Pull request successfully merged into master. Build succeeded: |
congr!
and improvement to convert
congr!
and improvement to convert
This introduces a tactic
congr!
that is an analogue to mathlib 3'scongr'
. It is a more insistent version ofcongr
that makes use of more congruence lemmas (including user congruence lemmas),propext
,funext
, andSubsingleton
instances. It also has a feature to lift reflexive relations to equalities. Along withfunext
, the tactic doesintros
, allowingcongr!
to get access to function bodies; the introduced variables can be named usingrename_i
if needed.This also modifies
convert
to usecongr!
rather thancongr
, which makes it work more like the mathlib3 version of the tactic.