When preserved_exprs and replacements conflict?

[wdcraft01]

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.

[wwitzel]

This will be easier to fix after effecting #291. Conflicts that occur between "replacements" and "preserved expressions" are often a result of preserving the lhs for a @relation_prover. If the lhs was preserved via some other mechanism, this wouldn't be so tricky.

But are there still going to be unavoidable conflicts? Does it make sense to have one override the other? This requires more thought.

[wdcraft01]

Here is a related thought, for completeness of the record. I have this kind of gut-level reaction against having replacements vs. preserved_exprs over-ride each other based only on when they are specified or encountered, and instead would argue for having one or the other (to me it makes most sense for the preserved_exprs) to always over-ride the other. So we might include expr x in the preserved_exprs, and later someone might come along and include x = y in the replacements, in which case we might (1) simply ignore the replacement; (2) ignore the replacement but also produce some textual output explaining why; or (3) raise an error, pointing out that the user has provided a replacement for an expression that has been previously set to be preserved. I don't have any explicit justification for my inclination to take preserved_exprs as over-riding replacements instead of vice-versa.

Perhaps we are expecting preserved_exprs to work too hard in accomplishing the various types of preservation in various contexts? Perhaps we need some elaboration of distinctions between between preserving an expr in the assumptions vs. on the lhs of a relation vs. on the rhs of a relation vs. within an inner_expr() operation?