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

Rethink preserving lhs for @equality_prover methods #291

Open
wwitzel opened this issue Jun 22, 2022 · 0 comments
Open

Rethink preserving lhs for @equality_prover methods #291

wwitzel opened this issue Jun 22, 2022 · 0 comments

Comments

@wwitzel
Copy link
Collaborator

wwitzel commented Jun 22, 2022

What are the odds that the original expression occurs on the right hand side after calling @equality_prover? Well, it can happen. Here is an example:

Let's call disassociation on 3*(a*a). Well, unless auto_simplify is disabled or the 'combine_exponents' simplification directive of Mult is turned off (which would be sensible thing to do if you really want to disassociate), the a's will be regrouped in the attempt to combine the exponents. It will attempt to do this by setting a replacement of "a*a = a^2". But that replacement doesn't occur, because after regrouping we have the original expression which is preserved. So instead you end up with
3*(a*a) = 3*(a*a)
which makes no sense after trying to disassociate. It's neither disassociated nor simplified. The appropriate thing to do (although still silly) would be to end up with
3*(a*a) = 3*a^2
this would at least clue the user into the fact that the auto-simplification is thwarting their attempt to disassociate.

One fix is to make the preservation of the lhs be more targeted rather than preserving all instances of the expression. I'm not yet sure if this is what we need to do, though.

wwitzel added a commit that referenced this issue Jan 15, 2023
Implemented Issue #291 to specifically preserve the lhs (rather
than the lhs expression in a blanket way) for @auto_prover_..'s
(see Issue #308).
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant