SetOfAllMembership conclude() method errors

[wdcraft01]

trafficstars

The SetOfAllMembership and SetOfAllNonmembership classes have been created in branch 329-QEC-development-…, along with the usual class methods, using the UnionMembership and IntervalMembership classes as models.

The SetOfAllMembership.conclude() method ends up instantiating the following theorem (in one branch of the code):

In many cases, the expression created during the instantiation process does not match the original expression and an error is raised in the _make_decorated_prover() method in proveit/decorators.py:

File ~/Desktop/Prove-It/packages/proveit/decorators.py:225, in _make_decorated_prover.<locals>.decorated_prover(*args, **kwargs)
    223 else:
    224     if proven_truth.expr != expr:
--> 225         raise ValueError("@prover method %s whose name starts with "
    226                          "'conclude' must prove %s but got "
    227                          "%s."%(func, expr, proven_truth))
    228     # Match the style of self.
    229     return proven_truth.with_matching_style(expr)

The cases that seem to cause problems are ones in which we have multiple explicit conditions in the original SetOfAll sub-expression, leading to initial expressions in which the domain.condition expression consists of a flattened conjunction of conditions, while the instantiated expression has a domain.condition expression that consists of a nested conjunction.

For example, if we begin with the SetOfAllMembership expression expr given by:

then inside the .conclude() method, the expr.domain.condition looks like this:

(a conjunction of three sub-expressions), while the instantiated result has a domain.condition that looks like this:

(a conjunction of two expressions, one of which is itself another conjunction).

It has proven difficult to find a code location to enact some preservation or simplification process to alleviate this problem (@wwitzel will recall that he and I explored this together for a good chunk of time on Fri 3/21/2025). In many of these problematic cases, simply re-running or re-calling the .conclude() method on the original expression allows the desired conclusion without an error message.

[wwitzel]

After giving this more thought, the issue is that the SetOfAllMembership.conclude method is not versatile enough to work for all cases. It works when the condition of the SetOfAll is a binary conjunction whose first element is the domain condition and the second element is the rest (and may be a conjunction as well). However, when the second part is a conjunction, the overall condition can simplify to a conjunction with arity > 2. This is the problem we are encountering. The instantiation of fold_basic_comprehension will then result in a judgment that is not directly applicable but should be equal to what is wanted. It should simplify to what is wanted, so why is that failing? Well, it's pretty subtle and convoluted. What is happening in this example is that Relation.conclude is first trying to see if it can conclude via simplifying both sides first. That problem is that it already add the original to the list of "preserved_exprs" thereby thwarting the ability to simplify to the correct form after instantiating fold_basic_comprehension. Here is a possible simple fix (@wdcraft01 , give this a try and let me know if it works). Inside then SetOfAllMembership.conclude, when instantiating fold_basic_comprehension, set "auto_simplify=True" and "preserved_exprs = (self.domain,)". Note, the latter is different than "preserve_expr = self.domain" which will add to the list of preserved_exprs and retain something that is unwanted.

To avoid this type of problem entirely, we might consider modifying decorators.py so that instead of automatically adding "self" to preserved_exprs when calling a "conclude" prover, it will change the preserved_exprs to only include "self". First, let's double-check that I'm correctly diagnosing the issue and understanding what is going on.

[wdcraft01]

From @wwitzel above:

After giving this more thought ... Here is a possible simple fix .... Inside the SetOfAllMembership.conclude(), when instantiating fold_basic_comprehension, set "auto_simplify=True" and "preserved_exprs = (self.domain,)". Note, the latter is different than "preserve_expr = self.domain" which will add to the list of preserved_exprs and retain something that is unwanted.

This approach does appear to address one class of errors that were arising, in particular the errors arising for the case in which the SetOfAllMembership object has a SetOfAll domain with a single instance_var and the instance_var is the same as the instance_element, for example in cases like:

$a \in \{x | 0 \le x \le 1 \}_{x \in \mathbb{R}}$

Such cases instantiate the fold_basic_comprehension theorem:

I am still trying to address errors arising for cases in which we have multiple instance variables and/or have an instance_element that is not simply an instance variable, for example a case like:

$a \in \{x^{2} | 0 \le x \le 1 \}_{x \in \mathbb{R}}$

The problem doesn't appear to arise because of the multiple instance variables or the more complicated instance_element, per se, but instead appears to be an issue with the instantiation of the more complicated fold theorem

used for such cases and the resulting instantiated form playing a bit “fast and loose” with the existential antecedent. In particular, a problem arises when the original SetOfAllMembership object has a domain with an explicit condition involving a conjunction, like $(0 \le x) \land (x \le 1)$ or even the implicit conjunction involved in the example above with the number_order() condition $0 \le x \le 1$. For example, given the expression:

the instantiation of the fold theorem produces:

despite various attempts to specify preserved_exprs = {...} in the instantiation process. For example, using:

preserved_exprs = {self.domain, *self.domain.explicit_conditions()}

doesn't work. The instantiation's result eventually leads to an error when trying to derive_consequent() if one uses the “natural" assumption

whose explicit condition matches the explicit condition in the original expression.

[wdcraft01]

After work with @wwitzel on Wed 4/09/2025, and introducing a number of relatively minor modifications plus now including a "switch" for setting auto_simplify to True vs. False in the fold instantiation depending on whether or not we have induced an empty conjunction And() (and thus want auto_simplify = True) vs. simply wanting to preserve the explicit conditions (and thus want auto_simplify = False), we have the example above working fine now — i.e. when the original expression produced a nested conjunction, the instantiation now produces a matching nested conjunction. Yay!

But now we seem to have the reverse problem (where it wasn't a problem previously): when the original expression does NOT have an inherently nested conjunction of conditions, the instantiation is producing a nested conjunction. Here's the basic example (screen shot of output along with diagnostic print statements):

A kludgy fix for this that works for a variety of examples: put the fold.instantiate() and derive_consequent() in a try except block. If the try fails, then reverse the auto_simplify setting and perform the fold.instantiate() & derive_consequent() again. That is inefficient, of course, plus the approach still doesn't address errors that arise when trying to work with SetOfAll objects that simultaneously have multiple instance variables with multiple explicit conditions.