TransitiveRelation

class proveit.TransitiveRelation(operator, normal_lhs, normal_rhs, *, styles)

Bases: proveit.relation.relation.Relation

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).

Methods Summary

EquivalenceClass()
StrongRelationClass()
WeakRelationClass()
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.
apply_transitivity(self, other, …)	Apply transitivity to derive a new relation from ‘self’ and ‘other’.
conclude(self[, check_transitive_pair])	Try to conclude the TransitivityRelation using other TransitivityRelations or Equals that are known to be true via transitivity.
conclude_via_transitivity(self, …)	Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.
insertion_point(sorted_items, item_to_insert)	Return the position to insert the “item to insert” into the sorted items to maintain the sorted order (according to the TransitivityRelation class cls).
known_relations_from_left(expr, \*[, …])	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.
known_relations_from_right(expr, \*[, …])	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.
mergesort(item_iterators[, skip_exact_reps, …])	Return the proven Sequence, a judgment for an expression of type cls.SequenceClass(), representing the sorted sequence according to the cls.mergesorted_items method.
mergesorted_items(item_iterators[, …])	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.
side_effects(self, judgment)	Yield methods to attempt as side-effects when this expression is proven as a judgment.
sort(items[, reorder])	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.
sorted_items(items[, reorder])	Return the given items in sorted order with respect to this TransitivityRelation class (cls) under the given assumptions using known transitive relations.

Methods Documentation

static EquivalenceClass()

static StrongRelationClass()

static WeakRelationClass()

static 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.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

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.

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

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).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

conclude_via_transitivity(self, \*\*defaults_config)

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

classmethod insertion_point(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.

classmethod known_relations_from_left(expr, \*, assumptions=None)

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.

classmethod known_relations_from_right(expr, \*, assumptions=None)

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.

classmethod mergesort(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).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

classmethod mergesorted_items(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).

side_effects(self, judgment)

Yield methods to attempt as side-effects when this expression is proven as a judgment. These should each accept an ‘assumptions’ parameter. These should be obvious and useful consequences, trivial and limited. There is no need to call this manually; it is called automatically when the corresponding Judgment is created. It also may be desirable to store the judgment for future automation.

classmethod sort(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).

Keyword arguments are accepted for temporarily changing any of the attributes of proveit.defaults.

classmethod sorted_items(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).