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.

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

Bug in ring tactic #2672

Closed
robertylewis opened this issue May 13, 2020 · 1 comment
Closed

Bug in ring tactic #2672

robertylewis opened this issue May 13, 2020 · 1 comment
Labels
bug t-meta Tactics, attributes or user commands

Comments

@robertylewis
Copy link
Member 

import tactic.ring 

-- loops
example (A B : ℕ) : A * B = 2 :=
begin 
  -- ring,
end

I'll investigate if/when I find time, teaching is claiming a lot of energy this week though. @digama0 may find it first.
@bryangingechen bryangingechen added bug t-meta Tactics, attributes or user commands labels May 14, 2020
@alexjbest
Copy link
Member

I'm not really sure why but the problem seems to be https://github.com/leanprover-community/mathlib/blob/master/src//tactic/ring.lean#L569 if the guard statement there is deleted then this doesn't loop but it seems the tests still pass. To debug further I'd need more understanding of the c++ code than I currently have.

digama0 added a commit that referenced this issue Jan 12, 2021
@digama0
fix(tactic/ring): fix loop in ring
8e69b0a 
This occurs because when we name the atoms in `A * B = 2`, `A` is the
first and `B` is the second, and once we put it in horner form it ends up
as `B * A = 2`; but then when we go to rewrite it again `B` is named atom
number 1 and `A` is atom number 2, so we write it the other way around
and end up back at `A * B = 2`. The solution implemented here is to
retain the atom map across calls to `ring.eval` while simp is driving
it, so we end up rewriting it to `B * A = 2` in the first place but in the
second pass we still think `B` is the second atom so we stick with the
`B * A` order.

Fixes #2672
@digama0 digama0 mentioned this issue Jan 12, 2021
Closed
@bors bors bot closed this as completed in 5a532ca Jan 13, 2021
b-mehta pushed a commit that referenced this issue Jan 16, 2021
@digama0 @b-mehta
fix(tactic/ring): fix loop in ring (#5711)
c4688ed 
This occurs because when we name the atoms in `A * B = 2`, `A` is the
first and `B` is the second, and once we put it in horner form it ends up
as `B * A = 2`; but then when we go to rewrite it again `B` is named atom
number 1 and `A` is atom number 2, so we write it the other way around
and end up back at `A * B = 2`. The solution implemented here is to
retain the atom map across calls to `ring.eval` while simp is driving
it, so we end up rewriting it to `B * A = 2` in the first place but in the
second pass we still think `B` is the second atom so we stick with the
`B * A` order.

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

Successfully merging a pull request may close this issue.

[Merged by Bors] - fix(tactic/ring): fix loop in ring leanprover-community/mathlib
3 participants
@alexjbest @robertylewis @bryangingechen