Source code for proveit.relation.transitivity

"""
A TransitiveRelation is a generic base class for binary
relationships that are transitive.  Less than and greater than
relationships are examples (so are subset and superset relationships).
For example, transitivity in the "less than" theory means that
a<b and b<c implies that a<c.  The "equivalence class"
(proveit.logic.Equals by default) is special kind of TransitiveRelation
that is also symmetric; that is, y=x if x=y.
proveit.logic.Equals is a TransitiveRelation, but
overloads the default methods.  The TransitiveRelation class
provides convenient automation capabilities for performing
a transitive search to conclude a new relation from known relations
using transitivity rules.  To enable this, each TransitiveRelation
needs to track to define known_left_sides and known_right_sides as
class dictionaries; these will be populated as side effects for
each proven relation (see derive_side_effects).  Also, the
apply_transitivity method should be appropriately implemented.
The default version handles the case when the "other" relation
is an equality (in which case, substitution may simply be performed).
"""

from proveit import defaults, USE_DEFAULTS, Judgment, ProofFailure
from proveit.decorators import prover
from proveit.util import OrderedSet
from .sorter import TransitivitySorter
from .relation import Relation


[docs]class TransitiveRelation(Relation): r''' Base class for generic transitive relations. Examples are <, <=, >, >= as well as subset, subseteq, superset, and superseteq relations. proveit.logic.Equals is a special TransitiveRelation which is also symmetric (x=y means that y=x). ''' def __init__(self, operator, normal_lhs, normal_rhs, *, styles): Relation.__init__(self,operator, normal_lhs, normal_rhs, styles=styles) def _record_as_proven(self, judgment): ''' Store known left sides and known right sides in class member dictionaries: known_left_sides, known_right_sides which will enable transitivity searches. ''' if (not hasattr(self.__class__, 'known_left_sides') or not hasattr(self.__class__, 'known_right_sides')): raise NotImplementedError( "Expressions derived from TransitiveRelation should define " "'known_left_sides' and 'known_right_sides' as class " "variables") self.__class__.known_left_sides.setdefault( self.normal_lhs, OrderedSet()).add(judgment) self.__class__.known_right_sides.setdefault( self.normal_rhs, OrderedSet()).add(judgment) def _readily_provable(self, *, check_transitive_pair=True): ''' If check_transitive_pair is True, we will return True if we can find a combination of a known plus a provable pair of relations that is a transitive decomposition of this relation. For example, for "a < c" it may return (a < b, b < c) as a transitive decomposition if one is known and the other is provable. ''' if check_transitive_pair: transitive_pair = self.known_plus_provable_transitive_pair() if transitive_pair is not None: return True return False
[docs] @prover def conclude(self, check_transitive_pair=True, **defaults_config): ''' Try to conclude the TransitivityRelation using other TransitivityRelations or Equals that are known to be true via transitivity. For example, if a<b, b=c, and c<=d are known truths (under the given assumptions), we can conclude that a<d (under these assumptions). ''' if check_transitive_pair: transitive_pair = self.known_plus_provable_transitive_pair() if transitive_pair is not None: # Prove via transitivity from a known relation and a # readily provable relation. transitive_pair[0].apply_transitivity(transitive_pair[1]) return self.prove() # relax if needed. try: # Try to conclude via simplification of each side. return Relation.conclude(self) except ProofFailure: pass # Use a breadth-first search approach to find the shortest # path to get from one end-point to the other. try: return self.conclude_via_transitivity() except TransitivityException as e: # indicate the expression we were trying to prove raise TransitivityException(self, defaults.assumptions, e.message)
[docs] @prover def conclude_via_transitivity(self, **defaults_config): from proveit.logic import Equals try: proven_relation = self.__class__._transitivity_search( self.normal_lhs, self.normal_rhs) except TransitivityException as e: # indicate the expression we were trying to prove raise TransitivityException(self, defaults.assumptions, e.message) relation = proven_relation.expr if relation.__class__ != self.__class__: if self.__class__ == self.__class__._checkedWeakRelationClass(): if relation.__class__ == self.__class__._checkedStrongRelationClass(): return relation.derive_relaxed() elif relation.__class__ == Equals: # Derive a weaker relation via the strong relation # of equality: return self.conclude_via_equality() msg = ("Not able to conclude the desired relation of %s" " from the proven relation of %s." % (str(self), str(relation))) raise TransitivityException(self, defaults.assumptions, msg) return proven_relation
@classmethod def _RelationClasses(cls): ''' Return the strong and weak relation classes. ''' return (cls._checkedStrongRelationClass(), cls._checkedWeakRelationClass())
[docs] @classmethod def known_relations_from_left(RelationClass, expr, *, assumptions=USE_DEFAULTS): ''' Yield (Judgment, right-hand-side) pairs for this transitive relationship (or equality) that involve the given expression on the left side and are known to be true under the given assumptions. Equality relations will always be yielded first. Strong relations will be yielded next. Weak relations will only be yielded if this is a weak relation class. ''' from proveit.logic import Equals equiv_class = RelationClass.EquivalenceClass() # equivalence relationships are strongest and should come first. _kwargs = {'assumptions':assumptions} if equiv_class==Equals: _kwargs['include_canonical_forms'] = False equiv_left_relations = equiv_class.known_relations_from_left( expr, **_kwargs) for (judgment, other_expr) in equiv_left_relations: if expr != other_expr: # exclude reflexive equations -- they don't count yield (judgment, other_expr) if RelationClass is not equiv_class: relation_classes = RelationClass._RelationClasses() # stronger then weaker relations for _Relation in relation_classes: for judgment in list(_Relation.known_left_sides.get(expr, [])): if judgment.is_applicable(assumptions): yield (judgment, judgment.normal_rhs)
[docs] @classmethod def known_relations_from_right(RelationClass, expr, *, assumptions=USE_DEFAULTS): ''' Yield (Judgment, left-hand-side) pairs for this transitivie relationship (or equality) that involve the given expression on the right side and are known to be true under the given assumptions. Equality relations will always be yielded first. Strong relations will be yielded next. Weak relations will only be yielded if this is a weak relation class. ''' equiv_class = RelationClass.EquivalenceClass() # equivalence relationships are strongest and should come first. equiv_right_relations = equiv_class.known_relations_from_right( expr, assumptions=assumptions) for (judgment, other_expr) in equiv_right_relations: if expr != other_expr: # exclude reflexive equations -- they don't count yield (judgment, other_expr) if RelationClass is not equiv_class: relation_classes = RelationClass._RelationClasses() # stronger then weaker relations for _Relation in relation_classes: for judgment in list(_Relation.known_right_sides.get(expr, [])): if judgment.is_applicable(assumptions): yield (judgment, judgment.normal_lhs)
def known_plus_provable_transitive_pair(self): ''' Find and return a pair of relations that form a transitive decomposition of this relation in which one of the relations is known and the other is readily provable under default assumptions. For example, if self is "a < c", "a < b" is known, and "b < c" is provable, it may return (a < b, b < c). If no such pair is found, return None. To keep this manageable and relevant, known relations starting from irreducible values are not considered. We also skip relations with the same canonical form (e.g., trivial equalities). ''' from proveit.logic import is_irreducible_value MyClass = type(self) WeakRelationClass = type(self).WeakRelationClass() if not is_irreducible_value(self.normal_lhs): for relation, _ in WeakRelationClass.known_relations_from_left( self.normal_lhs): if (relation.lhs.canonical_form()== relation.rhs.canonical_form()): continue completing_relation = MyClass(relation.normal_rhs, self.normal_rhs) if completing_relation.readily_provable( check_transitive_pair=False): return (relation, completing_relation) if not is_irreducible_value(self.normal_rhs): for relation, _ in WeakRelationClass.known_relations_from_right( self.normal_rhs): if (relation.lhs.canonical_form()== relation.rhs.canonical_form()): continue completing_relation = MyClass(self.normal_lhs, relation.normal_lhs) if completing_relation.readily_provable( check_transitive_pair=False): return (relation, completing_relation) if WeakRelationClass is MyClass: # Trying to prove a weak relation; we check weak relations # so we are don. return None # Trying to prove a strong relation. We check a combination # of a known weak relation and a provable strong relation. Now # check for a known strong relation and provable weak relation. if not is_irreducible_value(self.normal_lhs): for relation, _ in MyClass.known_relations_from_left( self.normal_lhs): if not isinstance(relation, MyClass): continue completing_relation = WeakRelationClass(relation.normal_rhs, self.normal_rhs) if completing_relation.readily_provable( check_transitive_pair=False): return (relation, completing_relation) if not is_irreducible_value(self.normal_rhs): for relation, _ in MyClass.known_relations_from_right( self.normal_rhs): if not isinstance(relation, MyClass): continue completing_relation = WeakRelationClass(self.normal_lhs, relation.normal_lhs) if completing_relation.readily_provable( check_transitive_pair=False): return (relation, completing_relation)
[docs] @prover def apply_transitivity(self, other, **defaults_config): ''' Apply transitivity to derive a new relation from 'self' and 'other'. For example, from self:a<b, other:b=c, derive a<c. This must be implemented for the different types of transitive relations. This default version handles the case where 'other' is an Equals expression. ''' from proveit.logic import Equals # print 'apply transitivity', self, other if isinstance(other, Equals): if other.normal_lhs in (self.normal_lhs, self.normal_rhs): subrule = other.sub_right_side_into common_expr = other.normal_lhs elif other.normal_rhs in (self.normal_lhs, self.normal_rhs): subrule = other.sub_left_side_into common_expr = other.normal_rhs else: raise ValueError( "Equality does not involve either side of inequality!") if common_expr == self.normal_lhs: # replace the normal_lhs of self with its counterpart # from the "other" equality. return subrule(self.inner_expr().normal_lhs) elif common_expr == self.normal_rhs: # replace the normal_rhs of self with its counterpart # from the "other" equality. return subrule(self.inner_expr().normal_rhs) raise NotImplementedError( 'Must implement apply_transitivity appropriately for each ' 'kind of TransitiveRelation')
[docs] @staticmethod @prover def apply_transitivities(chain, **defaults_config): ''' Apply transitvity rules on a list of relations in the given chain to proof the relation over the chain end points. Each element of the chain must represent a TransitiveRelation. The chain must "connect" in the sense that any two neighbors in the chain can be joined via apply_transitivity. If the relation types are all the same, and that relation class has a 'relate_across_chain_transitively' method, apply that method for a potentially streamlined proof. Otherwise, use 'apply_transitivity' on the relations in a pairwise fashion from the left. ''' if len(chain) == 0: raise TransitivityException( None, defaults.assumptions, 'Empty transitivity relation train') transitive_relation_types = set() #print('chain', chain) for relation in chain: if isinstance(relation, Judgment): relation = relation.expr if not isinstance(relation, TransitiveRelation): raise TypeError("The 'chain' must be composed of " "TransitiveRelation expressions/judgments, " "not %s of type %s"%(relation, type(relation))) transitive_relation_types.add(type(relation)) if len(chain) == 1: # Trivial case of a single relation. return chain[0].prove() if len(transitive_relation_types) != 1 or ( not hasattr(next(iter(transitive_relation_types)), 'relate_across_chain_transitively')): # When there is more than one relation type, we will # simply use 'apply_transitivity' in a pairwise fasion. return (TransitiveRelation. _apply_transitivities_via_apply_transitivity(chain)) # Extract the successive elements being related along the # chain and then call 'relate_across_chain_transitively'. chain_iter = iter(chain) _x = [] # Expressions being related in the transitivity chain first = next(chain_iter) second = next(chain_iter) is_reversed = first.is_reversed() # Add the first two items of _x by looking at the first two # relations. if first.rhs in (second.lhs, second.rhs): _x.extend((first.lhs, first.rhs)) elif first.lhs in (second.lhs, second.rhs): _x.extend((first.rhs, first.lhs)) else: raise TransitivityException( None, defaults.assumptions, 'Transitivity cannot be applied unless there is something ' 'in common in the equalities: %s vs %s' % (str(first), str(second))) # Add subsequently to _x by looking at each relation. for relation in chain_iter: first = second second = relation if _x[-1] == first.lhs: _x.append(first.rhs) else: _x.append(first.lhs) if _x[-1] not in (second.lhs, second.rhs): raise TransitivityException( None, defaults.assumptions, 'Transitivity cannot be applied unless there is ' 'something in common in the equalities: %s vs %s' % (str(first), str(second))) # Add the last item to _x. if _x[-1] == second.lhs: _x.append(second.rhs) else: _x.append(second.lhs) relation_class = next(iter(transitive_relation_types)) try: relation = relation_class.relate_across_chain_transitively(*_x) except NotImplementedError: # Fall back to the serial approach. return (TransitiveRelation. _apply_transitivities_via_apply_transitivity(chain)) if is_reversed: # Reverse the direction in the style, consistent with # the first relation of the chain. return relation.with_direction_reversed() return relation
@staticmethod @prover def _apply_transitivities_via_apply_transitivity(chain, **defaults_config): ''' Apply transitvity rules on a list of relations in the given chain to proof the relation over the chain end points. Each element of the chain must be a Judgment object that represents a proven relation for which transitivity rules may be applied via an 'apply_transitivity' method (such as a Judgment for a proven Equals statement). The chain must "connect" in the sense that any two neighbors in the chain can be joined vie apply_transitivity. The transitivity rule will be applied left to right. ''' if len(chain) == 0: raise TransitivityException( None, defaults.assumptions, 'Empty transitivity relation train') for relation in chain: if isinstance(relation, Judgment): relation = relation.expr if not isinstance(relation, TransitiveRelation): raise TypeError("The 'chain' must be composed of " "TransitiveRelation expressions/judgments, " "not %s of type %s"%(relation, type(relation))) chain = list(chain) while len(chain) >= 2: first = chain.pop(0) second = chain.pop(0) new_relation = first.apply_transitivity(second) if not isinstance(new_relation, Judgment): raise TypeError( "apply_transitivity should return a Judgment, not %s" % new_relation) chain.insert(0, new_relation) return chain[0] # we are done
[docs] @staticmethod def EquivalenceClass(): from proveit.logic import Equals return Equals
[docs] @staticmethod def WeakRelationClass(): raise NotImplementedError( "The Expression class for the weak form of the relation (that include equality as a possibility) should be returned")
[docs] @staticmethod def StrongRelationClass(): raise NotImplementedError( "The Expression class for the strong form of the relation (that excludes equality as a possibility) should be returned")
@classmethod def _checkedWeakRelationClass(RelationClass): equiv_class = RelationClass.EquivalenceClass() if RelationClass == equiv_class: return equiv_class # ("equal to" or "equal to" is just "equal to") try: Relation = RelationClass.WeakRelationClass() except NotImplementedError: raise NotImplementedError( "The Expression class for the weak form %s (that include equality as a possibility) should be returned" % str(RelationClass)) assert issubclass( Relation, TransitiveRelation), "WeakRelationClass() should return a sub-class of TransitiveRelation" return Relation @classmethod def _checkedStrongRelationClass(RelationClass): try: Relation = RelationClass.StrongRelationClass() except NotImplementedError: raise NotImplementedError( "The Expression class for the strong form %s (that excludes equality as a possibility) should be returned" % str(RelationClass)) assert issubclass( Relation, TransitiveRelation), "StrongRelationClass() should return a sub-class of TransitiveRelation" return Relation
[docs] @classmethod def sorted_items(cls, items, reorder=True, **defaults_config): ''' Return the given items in sorted order with respect to this TransitivityRelation class (cls) under the given assumptions using known transitive relations. If reorder is False, raise a TransitivityException if the items are not in sorted order as provided. Weak relations (e.g., <=) are only considered when calling this method on a weak relation class (otherwise, only equality and strong relations are used in the sorting). ''' from proveit.numbers import is_numeric_int if all(is_numeric_int(item) for item in items): # All the items are integers. Use efficient n log(n) sorting to # get them in the proper order and then use fixed_transitivity_sort # to efficiently prove this order. items = sorted(items, key=lambda item: item.as_int()) reorder = False if reorder: sorter = TransitivitySorter(cls, items) return list(sorter) else: return cls._fixed_transitivity_sort(items).operands
[docs] @classmethod @prover def sort(cls, items, reorder=True, **defaults_config): ''' Return the proven total ordering (conjunction of relations presented in the total ordering style) representing the sorted sequence according to the cls.sorted_items method. Weak relations (e.g., <=) are only considered when calling this method on a weak relation class (otherwise, only equality and strong relations are used in the sorting). ''' automation = True if reorder: items = cls.sorted_items(items, reorder) #print("sorted", items) automation = False # Direct relations already proven. return cls._fixed_transitivity_sort(items, automation=automation)
[docs] @classmethod def mergesorted_items(cls, item_iterators, skip_exact_reps=False, skip_equiv_reps=False, requirements=None): ''' Given a list of Expression item iterators, with each generator yielding items in sorted order, yield every item (from all the generators) in sorted order. If skip_exact_reps is True, only yield the first of an 'item' that is repeated exactly (equal Expressions). If skip_equiv_reps is True, only yield the first of an 'item' that is repeated via a known equivalence. Passes back requirements (if provided) that are the specific merger relations. Weak relations (e.g., <=) are only considered when calling this method on a weak relation class (otherwise, only equality and strong relations are used in the sorting). ''' # item_iterators may be actual iterators or something that # can produce an iterator. Convert them all to actual iterators. for k, iterator in enumerate(item_iterators): try: # Try to convert to an actual iterator. item_iterators[k] = iter(iterator) except BaseException: pass # Assume it is already an actual iterator. # Start with the first item from each generator and track # the generator(s) for each item so we no where to get the # item(s) to be added after yielding the "next" sorted item. first_items = [] front_item_to_iterators = dict() for iterator in item_iterators: try: item = next(iterator) first_items.append(item) front_item_to_iterators.setdefault(item, []).append(iterator) except StopIteration: pass if requirements is None: requirements = [] # Create a TransitivitySorter. sorter = TransitivitySorter(cls, first_items, skip_exact_reps=skip_exact_reps, skip_equiv_reps=skip_equiv_reps) # Yield items in sorted order from the TransitivitySorter, # add to the TransitivitySorter as new items become "exposed", # and keep front_item_to_iterators updated. prev_item = None prev_iters = None for next_item in sorter: yield next_item # Yield the next item. if next_item not in front_item_to_iterators: prev_item = next_item prev_iters = set() continue # Add newly "exposed" items and update # front_item_to_iterators. iterators = front_item_to_iterators.pop(next_item) if prev_item is not None and prev_iters.isdisjoint(iterators): # next_item and prev_item are in different iterators, # so their relationship is important for establishing # the sorted order of the merger. requirement = cls._transitivity_search(prev_item, next_item, automation=False) requirements.append(requirement) for iterator in iterators: try: item_to_add = next(iterator) # Add "exposed" item. sorter.add(item_to_add) # Update front_item_to_iterators. front_item_to_iterators.setdefault(item_to_add, []).append(iterator) except StopIteration: pass # Nothing more from this generator. prev_item = next_item prev_iters = set(iterators)
[docs] @classmethod @prover def mergesort(cls, item_iterators, skip_exact_reps=False, skip_equiv_reps=False, requirements=None, **defaults_config): ''' Return the proven Sequence, a judgment for an expression of type cls.SequenceClass(), representing the sorted sequence according to the cls.mergesorted_items method. Weak relations (e.g., <=) are only considered when calling this method on a weak relation class (otherwise, only equality and strong relations are used in the sorting). ''' items = cls.mergesorted_items(item_iterators, skip_exact_reps, skip_equiv_reps, requirements) items = list(items) #print("merge sorted", items) return cls._fixed_transitivity_sort(items, automation=False)
[docs] @classmethod def insertion_point(cls, sorted_items, item_to_insert, equiv_group_pos='any', requirements=None): ''' Return the position to insert the "item to insert" into the sorted items to maintain the sorted order (according to the TransitivityRelation class cls). The sorted_items should be provably sorted, with relations between consecutive items that are Judgments. If equiv_group_pos is 'first', the insertion point will be one that would place he "item to insert" prior to any equivalent items; if equiv_group_pos is 'last', the insertion point will be one that would place the "item to insert" after any equivalent items. If it is 'first&last', both insertion points are returned as a tuple pair (first, last). The default of equiv_group_pos='any' will result in an arbitrary position relative to equivalent items. ''' equiv_class = cls.EquivalenceClass() if item_to_insert in sorted_items: point = sorted_items.index(item_to_insert) else: item_iterators = [sorted_items, [item_to_insert]] # Don't skip equivalent or exact representations because # we don't want the insertion point index to be thrown # off and we need to make sure the 'item_to_insert' is # included: skip_exact_reps = skip_equiv_reps = False # And don't skip exact representations for k, item in enumerate(cls.mergesorted_items(item_iterators, skip_exact_reps, skip_equiv_reps, requirements)): if item == item_to_insert: point = k # If equiv_group_pos is 'first' or 'last', we need to make sure # we get the insertion point in the right spot with respect to # equivalent items. orig_point = point equiv_item = item_to_insert if equiv_group_pos == 'first' or equiv_group_pos == 'first&last': while point > 1: prev_point = point - 1 if item_to_insert == sorted_items[prev_point]: point -= 1 continue item1, item2 = sorted_items[prev_point], equiv_item try: relation = \ cls._transitivity_aearch(item1, item2, automation=False) except ProofFailure: msg = ("Unknown %s relationship between %s and %s" % (cls, item1, item2)) raise TransitivityException(None, defaults.assumptions, msg) if isinstance(relation.expr, equiv_class): equiv_item = sorted_items[prev_point] point -= 1 else: break first = point if equiv_group_pos == 'last' or equiv_group_pos == 'first&last': point = orig_point while point < len(sorted_items): if item_to_insert == sorted_items[point]: point += 1 continue item1, item2 = equiv_item, sorted_items[point] try: relation = \ cls._transitivity_search(item1, item2, automation=False) except ProofFailure: msg = ("Unknown %s relationship between %s and %s" % (cls, item1, item2)) raise TransitivityException(None, defaults.assumptions, msg) if isinstance(relation.expr, equiv_class): equiv_item = sorted_items[point] point += 1 else: break last = point if equiv_group_pos == 'first&last': return (first, last) return point
@classmethod @prover def _transitivity_search(cls, left_item, right_item, **defaults_config): ''' Performs a breadth-first, bidirectional (meet in the middle) search attempting to prove a relation between left_item and right_item according to the RelationClass by applying transitivity derivations. If successful, the approprate Judgment relating these items (in weak or strong form as can be determined) is returned; otherwise a TransitivityException is raised. ''' equiv_class = cls.EquivalenceClass() # Check if the relation is already known directly: if left_item == right_item: # Items are the exact same, so they are equal. return equiv_class(left_item, right_item).prove() try: # Try the strong relation first. StrongClass = cls._checkedStrongRelationClass() relation = StrongClass(left_item, right_item) return relation.prove(automation=False) except (ProofFailure, NotImplementedError): # Try equality. try: # Maybe the equality is known. relation = equiv_class(left_item, right_item) return relation.prove(automation=False) except ProofFailure: pass # Try the weak relation if cls is weak. if cls == cls._checkedWeakRelationClass(): try: # Maybe the weak relation is known. WeakClass = cls._checkedWeakRelationClass() relation = WeakClass(left_item, right_item) return relation.prove(automation=False) except (ProofFailure, NotImplementedError): pass if not defaults.conclude_automation: relation = cls(left_item, right_item) msg = ('No proof found via applying transitivity amongst' ' known proven relations.') raise TransitivityException(relation, defaults.assumptions, msg) sorter = TransitivitySorter(cls, [left_item, right_item], skip_exact_reps=False, skip_equiv_reps=False, presorted_pair=True) list(sorter) # should prove desired relation # Return the proven relation. return cls._transitivity_search(left_item, right_item, automation=False) @classmethod @prover def _fixed_transitivity_sort(cls, items, **defaults_config): ''' Check that the given items are in sorted order, returning the proven total ordering (conjunction of relations presented in a total ordering style) if they are or raising a TransitivityException if they are not. If automation is False, don't generate new relations through transitivities; assume that we already have the necessary direct relationships proven. ''' from proveit import ExprTuple if isinstance(items, ExprTuple): items_list = items.entries else: # in case the items are a non-indexable iterable items_list = list(items) relations = [] for item1, item2 in zip(items_list[:-1], items_list[1:]): relations.append(cls._transitivity_search(item1, item2)) return total_ordering(*relations, prove=True)
[docs]class TransitivityException(ProofFailure): def __init__(self, expr, assumptions, message): ProofFailure.__init__(self, expr, assumptions, message)
[docs]def total_ordering(*relations, prove=False): ''' Return a conjunction of relations in the total ordering style. For example, "a > b >= c = d > e" is a total ordering style for "(a > b) and (b >= c) and (c = d) and (d > e)". If there is a single relation, just return the relation. If 'prove' is True, return a proven Judgment. ''' from proveit import ExprRange from proveit.logic import And if len(relations) == 1 and not isinstance(relations[0], ExprRange): # Return a trivial, singular relation. relation = relations[0] if prove: relation = relation.prove() return relation # Return a conjunction with the proper style. conjunction = And(*relations) conjunction = conjunction.with_total_ordering_style() if prove: # Prove via composition. # Allow automation to prove the length requirement. return conjunction.conclude_via_composition(automation=True) return conjunction