wwitzel
commented
1 year ago 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.
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.