Prove-It
Prove-It copied to clipboard
When preserved_exprs and replacements conflict?
The order in which default attributes are updated makes a difference, and in particular the order in which replacements vs. preserved_exprs are updated/processed can make a difference when there is a conflict (e.g. when an expr is included in the preserved_exprs and also included as the lhs of a replacement). Unfortunately, the order in which such attributes are updated can be arbitrary, causing preserved_exprs to over-ride replacements sometimes and sometimes the other way around (leading to what appears to be nondeterministic behavior, with an expr sometimes being preserved but sometimes being replaced). This was happening recently in the proof notebook for the QPE thm _alpha_l_eval, in which two exponential factors were sometimes preserved but sometimes combined into a single exponential factor.
One possible solution to this would be to check and raise an exception when we discover we have an expr that is both in the preserved_expr list and appearing in the lhs of a replacement. Some brief testing of this approach on Wed 7/6/22 led to some promising results (for example, in the demos nbs), but also led to some (hopefully) sporadic errors in some of the demos/proofs.