Source code for proveit.numbers.number_sets.integers.interval

from proveit import Literal, Operation, prover
from proveit import a, b, c, d, n, x


[docs]class Interval(Operation): # operator of the Interval operation. _operator_ = Literal(string_format='Interval', theory=__file__) r''' The Interval class represents a set of of contiguous integers, from lower_bound to upper_bound (inclusively). For example: Interval(2, 6) represents the integer set {2, 3, 4, 5, 6}. Once created, the resulting Interval is interpreted as a SET of elements with no assurances about the elements being in a particular order. ''' def __init__(self, lower_bound, upper_bound, *, styles=None): Operation.__init__(self, Interval._operator_, (lower_bound, upper_bound), styles=styles) self.lower_bound = lower_bound self.upper_bound = upper_bound
[docs] def string(self, **kwargs): return '{' + self.lower_bound.string() + ' .. ' + \ self.upper_bound.string() + '}'
[docs] def latex(self, **kwargs): return r'\{' + self.lower_bound.latex() + r'~\ldotp \ldotp~' + \ self.upper_bound.latex() + r'\}'
def membership_object(self, element): from .interval_membership import IntervalMembership return IntervalMembership(element, self) def nonmembership_object(self, element): from .interval_membership import IntervalNonmembership return IntervalNonmembership(element, self) def readily_includes(self, other_set): ''' Return True if this NumberSet includes the 'other_set' set. ''' from proveit.numbers.number_sets.number_set import NumberSet return NumberSet.readily_includes(self, other_set)
[docs] @prover def deduce_elem_in_set(self, member, **defaults_config): from . import in_interval return in_interval.instantiate( {a: self.lower_bound, b: self.upper_bound, n: member}, auto_simplify=False)
[docs] @prover def deduce_subset_eq_relation(self, sub_interval, **defaults_config): ''' Deduce that self of the form {a...d} has as a subset_eq the Interval of the form {b...c}, if a <= b <= c <= d. Example: {1...5}.deduce_subset_eq_relation({2...4}) should return |- {2...4} \subset_eq {1...5} Not yet implemented for deducing a ProperSubset relation. ''' if isinstance(sub_interval, Interval): from . import interval_subset_eq _a = self.lower_bound _d = self.upper_bound _b = sub_interval.lower_bound _c = sub_interval.upper_bound return interval_subset_eq.instantiate( {a:_a, b:_b, c:_c, d:_d}, auto_simplify=False) else: raise NotImplementedError ( "In calling the Interval.deduce_subset_eq_relation() " "method, the proposed subset {} needs to be an Interval.". format(sub_interval))
@prover def deduce_cardinality(self, **defaults_config): ''' Deduce and return the equality between Card(self) and algebraic expression representing the cardinality (size) of the finite contiguous integers Interval set {a..b} in the form |- |{a..b}| = b - a + 1. For example, given the Interval I = {3..8}, calling I.deduce_cardinality returns |- |{3..8}| = 6 (assuming some appropriate auto_simplification of the numeric expression 8 - 3 + 1). Might have to pre-prove or include as assumptions enough information to establish that a and b in Interval(a, b) are both integers with a <= b. ''' from . import interval_cardinality from proveit.logic.sets import Card _a, _b = interval_cardinality.all_instance_params() _a_sub = self.lower_bound _b_sub = self.upper_bound return interval_cardinality.instantiate( {_a: _a_sub, _b: _b_sub}, preserve_expr = Card(self)) @prover def deduce_disjointness(self, disjoint_expr, **defaults_config): ''' Prove that two intervals are disjoint sets. ''' from proveit.logic import Disjoint from . import disjoint_intervals if (not isinstance(disjoint_expr, Disjoint) or not disjoint_expr.sets.is_double() or not isinstance(disjoint_expr.sets[0], Interval) or not isinstance(disjoint_expr.sets[1], Interval)): raise NotImplementedError( "'Interval.deduce_disjointness' only implemented to " "prove that two Intervals are correct, not %s" %disjoint_expr) interval1 = disjoint_expr.sets[0] interval2 = disjoint_expr.sets[1] _a, _b = interval1.operands _c, _d = interval2.operands return disjoint_intervals.instantiate( {a:_a, b:_b, c:_c, d:_d})