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

[Merged by Bors] - feat(tactic/noncomm_ring): add noncomm_ring tactic #2858

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat(tactic/noncomm_ring): add noncomm_ring tactic #2858

wants to merge 11 commits into from

Conversation

ocfnash
Copy link
Collaborator

@ocfnash ocfnash commented May 29, 2020 •
edited by semorrison

Fixes #2727

Co-authored-by: Scott Morrison scott.morrison@gmail.com

ocfnash
ocfnash commented May 29, 2020
View reviewed changes
src/algebra/classical_lie_algebras.lean
@@ -84,7 +84,7 @@ begin
let B := Eb R j i hij.symm,
intros c,
have c' : A.val ⬝ B.val = B.val ⬝ A.val := by { rw [←sub_eq_zero, ←sl_bracket, c.abelian], refl, },
have : 1 = 0 := by simpa [matrix.mul_val, hij] using (congr_fun (congr_fun c' i) i),
have : (1 : R) = 0 := by simpa [matrix.mul_val, hij] using (congr_fun (congr_fun c' i) i),
Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is an unrelated proposed change due to an observation of @kckennylau https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/a.20puzzle

@ocfnash ocfnash added the awaiting-review The author would like community review of the PR label May 29, 2020
Apply suggestions of Rob Lewis
a47b774 
Also adding a few more tests
@semorrison
Copy link
Collaborator

I think it's easy to make this a fair bit more powerful. Instead of using pow_two in your simp set, you could use pow_bit0, pow_bit1, pow_one, and prove things like

example : (a + b)^3 = a^3 + a^2*b + a*b*a + a*b^2 + b*a^2 + b*a*b + b^2*a + b^3 := by noncomm_ring

just as easily.

Similarly, abel likes things written in terms of gsmul, so if you take out mul_two and two_mul from the simp set, and instead add some lemmas that rewrite "numeral times something" into a gsmul, you can generalize.

@semorrison
Copy link
Collaborator

I'm happy to just commit some more suggestions direct to this PR, or leave you to do it, as you prefer.

@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 30, 2020
Apply (part of) Scott Morrison's suggestions.
e2c04a6 
This will cause some tests to fail for now.
@ocfnash
Copy link
Collaborator Author

ocfnash commented May 30, 2020

I'm happy to just commit some more suggestions direct to this PR, or leave you to do it, as you prefer.

Thank you very much for these suggestions. I have dropped the various lemmas you highlighted. I will have time to return to this late this afternoon but please feel free to add commits / take over this PR as you desire!

Restore mul_two, two_mul
7d84e71 
I still trust Scott Morrison that we should prefer to work via gsmul
but brief experiments suggest that this is not totally trivial. I
am thus reinstating the `mul_two` and `two_mul` so that tests pass,
pending further improvements.
@ocfnash
Copy link
Collaborator Author

ocfnash commented May 30, 2020

As noted in the commit message, I still trust that you are right @semorrison but I thought it would be better to leave this with passing tests.

Having experimented with replacing two_mul and mul_two with lemmas stating 2 * r = gsmul 2 r and r * 2 = gsmul 2 r, I had trouble getting the tests to pass. I was able to resolve one failure by replacing abel with abel; simp only [mul_gsmul_assoc] but I felt this was getting disgusting and another test was still blocked by a failure to solve: gsmul (-1) (a * gsmul 2 a) + gsmul 2 a * a = 0.

@semorrison
Copy link
Collaborator

semorrison commented May 30, 2020 •
edited

I added a few more lemmas (which we still need to move to better homes if we decide we like them), that result in more flexible handling of scalars.

@semorrison semorrison added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 30, 2020
@semorrison
Copy link
Collaborator

bors d+

@bors
Copy link

bors bot commented May 30, 2020

✌️ ocfnash can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bryangingechen
bryangingechen reviewed May 30, 2020
View reviewed changes
Copy link
Collaborator

@bryangingechen bryangingechen left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Please add import tactic.noncomm_ring to src/tactic/default.lean.

@ocfnash
Copy link
Collaborator Author

ocfnash commented May 30, 2020

Thanks again @semorrison you have made this so much better than it was, and have helped me learn in the process.

Glancing over the tests, I think we've got a nice little new tool.

@ocfnash
Copy link
Collaborator Author

ocfnash commented May 30, 2020

bors r+

bors bot pushed a commit that referenced this pull request May 30, 2020
@semorrison
feat(tactic/noncomm_ring): add noncomm_ring tactic (#2858)
0827a30 
Fixes #2727

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@semorrison semorrison removed the awaiting-review The author would like community review of the PR label May 31, 2020
@semorrison semorrison added the ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) label May 31, 2020
@bors
Copy link

bors bot commented May 31, 2020

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(tactic/noncomm_ring): add noncomm_ring tactic [Merged by Bors] - feat(tactic/noncomm_ring): add noncomm_ring tactic May 31, 2020
@bors bors bot closed this May 31, 2020
@bors bors bot deleted the tactic_noncomm_ring branch May 31, 2020 00:08
@ocfnash ocfnash mentioned this pull request Jun 29, 2020
Closed
cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022
@semorrison @cipher1024
feat(tactic/noncomm_ring): add noncomm_ring tactic (leanprover-commun…
2544a90 
…ity#2858)

Fixes leanprover-community#2727

Co-authored-by: Scott Morrison <scott.morrison@anu.edu.au>

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@robertylewis robertylewis robertylewis left review comments

@bryangingechen bryangingechen bryangingechen left review comments

Assignees
No one assigned
Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

a noncomm_ring tactic
4 participants
@ocfnash @semorrison @robertylewis @bryangingechen