-
Notifications
You must be signed in to change notification settings - Fork 11
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
Make @prover implementation easier w.r.t. auto_simplify and replacements #308
Comments
After some experimentation with this, I've come to the conclusion that the best way to handle this for now is to make versions of @Prover, @relation_prover, and @equality_prover that function in this new "easy" way but keep the old ones and switch to the "easy" way gradually. Trying to switch everything over at once breaks too many things and is not worth the headache at this time. It may not be wise to switch everything over, but that is something to determine at a later time. For now, I've created @auto_prover, @auto_relation_prover, and @auto_equality_prover which execute the method after setting preserve_all=True and then perform auto-simplifications/replacements afterwards. I don't think these naming conventions are great. Eventually, we may decide to rename these back to @Prover, @relation_prover, @equality_prover and rename the originals something else to denote them as special (if they are kept around). For now, I'm going to play around with switching to the "easy" way for a few select methods and see how well it works. |
We will gradually switch over to @auto_prover/@auto_relation_prover/ @auto_equality_prover which simply work by executing the wrapped method with preserve_all=True and then updating the resulting proof with auto-simplifications and replacements. After we switch everything over that we can and understand the exceptions (such as substitution where simplification should only apply to the 'touched' portion), we will likely rename the prover decorators.
Currently, one needs to 'preserve_all' for all but the last step and this can get tricky. It would be slightly less efficient but easier to handle auto_simplify and replacements in the wrapper after the first pass by re-running the last instantiation. Not sure how to handle it if the last step is modus ponens, generalization, or deduction, but there should be a way to do this.
The text was updated successfully, but these errors were encountered: