Source code for proveit.numbers.absolute_value.abs

from proveit import (defaults, Literal, Operation, ExprRange, InnerExpr,
                     UnsatisfiedPrerequisites, ProofFailure, 
                     prover, relation_prover, equality_prover)
from proveit import a, b, c, n, r, x, theta
from proveit.logic import InSet
from proveit.logic.sets import ProperSubset, SubsetEq
from proveit.numbers import NumberOperation, readily_provable_number_set


[docs]class Abs(NumberOperation): # operator of the Abs operation. _operator_ = Literal(string_format='Abs', theory=__file__) def __init__(self, A, *, styles=None): NumberOperation.__init__(self, Abs._operator_, A, styles=styles)
[docs] def string(self, **kwargs): return '|' + self.operand.string() + '|'
[docs] def latex(self, **kwargs): return r'\left|' + self.operand.latex() + r'\right|'
def _build_canonical_form(self): ''' Returns a form of this Abs that deterministically chooses either Abs of the canonical form of the operand or its negation since |x| = |-x|. ''' from proveit.numbers import Neg operand_cf = self.operand.canonical_form() neg_operand_cf = Neg(self.operand).canonical_form() if hash(operand_cf) < hash(neg_operand_cf): return Abs(operand_cf) # Choose |x| else: return Abs(neg_operand_cf) # Choose |-x| def _deduce_canonically_equal(self, rhs): ''' Prove Abs equal to 'rhs' asssuming they have the same canonical form. ''' from proveit.numbers import Neg from proveit.logic import Equals assert isinstance(rhs, Abs) operand_cf = self.operand.canonical_form() rhs_operand_cf = rhs.canonical_form() if operand_cf == rhs_operand_cf: # Prove equality using standard techniques. return NumberOperation._deduce_canonically_equal(self, rhs) else: # Prove equality via |x| = |-x|. assert (Neg(self.operand).canonical_form()== rhs.operand.canonical_form()) from . import abs_even_rev _x = self.operand replacements = [Equals(Neg(_x), rhs.operand).prove()] return abs_even_rev.instantiate( {x:_x}, replacements=replacements, auto_simplify=False) @prover def deduce_not_equal(self, rhs, **defaults_config): # accessed from conclude() method in not_equals.py from . import abs_not_eq_zero from proveit.logic import NotEquals from proveit.numbers import zero if rhs == zero: return abs_not_eq_zero.instantiate({a: self.operand}) return NotEquals(self, rhs).conclude_as_folded()
[docs] @prover def deduce_greater_than_equals_zero(self, **defaults_config): from . import abs_is_non_neg return abs_is_non_neg.instantiate({a: self.operand})
@equality_prover('distributed', 'distribute') def distribution(self, **defaults_config): ''' Equate this absolute value with its distribution over a product, fraction, or a sin() or cos(). ''' from . import abs_frac, abs_prod, abs_even from proveit import n, t, x from proveit.numbers import zero, Neg, Div, Mult from proveit.trigonometry import Sin, Cos if isinstance(self.operand, Neg): return abs_even.instantiate({x: self.operand.operand}) elif isinstance(self.operand, Div): # before returning, first prove that the abs value of the # original denom is not zero, and thus maintain that # property _b = self.operand.denominator Abs(_b).deduce_not_equal(zero) return abs_frac.instantiate( {a: self.operand.numerator, b: _b}) elif isinstance(self.operand, Mult): _x = self.operand.operands _n = _x.num_elements() return abs_prod.instantiate({n: _n, x: _x}) elif isinstance(self.operand, Sin): from proveit.trigonometry import abs_sin _t = self.operand.operand return abs_sin.instantiate({t: _t}) elif isinstance(self.operand, Cos): from proveit.trigonometry import abs_cos _t = self.operand.operand return abs_cos.instantiate({t: _t}) else: raise ValueError( 'Unsupported operand type for Abs.distribution() ' 'method: ', str(self.operand.__class__))
[docs] @equality_prover('abs_eliminated', 'abs_eliminate') def abs_elimination(self, **defaults_config): ''' For some |x| expression, deduce either |x| = x (the default) OR |x| = -x (for operand_type = 'negative'). Assumptions may be needed to deduce x >= 0 or x <= 0, respectively. ''' from . import abs_non_neg_elim, abs_neg_elim from proveit.numbers import LessEq, zero operand = self.operand if LessEq(zero, operand).readily_provable(): return abs_non_neg_elim.instantiate({x: operand}) elif LessEq(operand, zero).readily_provable(): return abs_neg_elim.instantiate({x: operand}) else: raise ValueError( "Unsupported operand type for Abs.abs_elimination() " "method; the sign of %s is not readily provable."%operand)
@equality_prover('double_abs_eliminated', 'double_abs_eliminate') def double_abs_elimination(self, **defaults_config): ''' ||x|| = |x| given x is complex. ''' from . import double_abs_elem if not isinstance(self.operand, Abs): raise ValueError("'double_abs_elimination' is only applicable " "for double absolute value cases, not %s" %self) return double_abs_elem.instantiate({x:self.operand.operand}) @equality_prover('shallow_simplified', 'shallow_simplify') def shallow_simplification(self, *, must_evaluate=False, **defaults_config): ''' Returns a proven simplification equation for this Abs expression assuming the operand has been simplified. Handles a number of absolute value simplifications: 1. ||x|| = |x| given x is complex 2. |x| = x given x ≥ 0 3. |x| = -x given x ≤ 0 (may try to prove this if easy to do) 4. |-x| = |x| 5. |x_1 * ... * x_n| = |x_1| * ... * |x_n| 6. |a / b| = |a| / |b| 7. |exp(i a)| = 1 given a in Real 8. |r exp(i a) - r exp(i b)| = 2 r sin(|a - b|/2) given a and b in Real. 9. |x_1 + ... + x_n| = +/-(x_1 + ... + x_n) if the terms are known to be all non-negative or all non-positive. 10. |sin(t)| = sin|t| for any real t 11. |cos(t)| = cos|t| for any real t ''' from proveit.logic import Equals from proveit.numbers import zero, e, Add, Neg, LessEq, Mult, Div, Exp from proveit.numbers import ( RealNeg, RealPos, RealNonNeg, RealNonPos, Complex) from proveit.logic import EvaluationError, is_irreducible_value from proveit.trigonometry import Cos, Sin if is_irreducible_value(self.operand): if isinstance(self.operand, Neg): # |-x| where 'x' is a literal. return self.distribution() elif must_evaluate: # The simplification of the operands may not have # worked hard enough. Let's work harder if we # must evaluate. self.operand.evaluation() return self.evaluation() # among other things, convert any assumptions=None # to assumptions=() (thus averting len(None) errors) # Check if we have an established relationship between # self.operand and zero. operand_ns = readily_provable_number_set(self.operand, default=Complex) if RealNonPos.readily_includes(operand_ns) or ( RealNonNeg.readily_includes(operand_ns)): # Either |x| = x or |x| = -x depending upon the sign # of x (comparison with zero). return self.abs_elimination() if isinstance(self.operand, Abs): # Double absolute-value. We can remove one of them. return self.double_abs_elimination() # Distribute over a product or division. if (isinstance(self.operand, Mult) or isinstance(self.operand, Div) or isinstance(self.operand, Neg)): # Let's distribute the absolute values over the product # or division (the absolute value of the factors/components # will be simplified seperately if auto_simplify is True). return self.distribution() # |exp(i a)| = 1 if isinstance(self.operand, Exp) and self.operand.base == e: try: return self.unit_length_simplification() except ValueError: # Not in a complex polar form. pass # |r exp(i a) - r exp(i b)| = 2 r sin(|a - b|/2) if (isinstance(self.operand, Add) and self.operand.operands.is_double()): try: return self.chord_length_simplification() except (ProofFailure, ValueError): # Not in a complex polar form. pass # |x_1 + ... + x_n| = +/-(x_1 + ... + x_n) # if the terms are known to be all non-negative or all # non-positive. if isinstance(self.operand, Add): all_nonneg = True all_nonpos = True for term in self.operand.terms: # Note that "not proven" is not the same as "disproven". # Not proven means there is something we do not know. # Disproven means that we do know the converse. if all_nonneg and not LessEq(zero, term).readily_provable(): all_nonneg = False if all_nonpos and not LessEq(term, zero).readily_provable(): all_nonpos = False if all_nonpos: InSet(self.operand, RealNonPos).prove() elif all_nonneg: InSet(self.operand, RealNonNeg).prove() if all_nonpos or all_nonneg: # Do another pass now that we know the sign of # the operand. return self.shallow_simplification() # |sin(t)| = sin|t| for any real t # |cos(t)| = cos|t| for any real t if (isinstance(self.operand, Sin) or isinstance(self.operand, Cos)): return self.distribution() # Default is no simplification. return Equals(self, self).prove() @equality_prover('reversed_difference', 'reverse_difference') def difference_reversal(self, **defaults_config): ''' Derive |a - b| = |b - a|. ''' from proveit.numbers import Add, Neg from . import abs_diff_reversal if not (isinstance(self.operand, Add) and self.operand.operands.is_double() and isinstance(self.operand.operands[1], Neg)): raise ValueError("Abs.difference_reversal is only applicable " "for an expression of the form |a - b|, not %s" %self) _a = self.operand.operands[0] _b = self.operand.operands[1].operand return abs_diff_reversal.instantiate({a:_a, b:_b})
[docs] @relation_prover def deduce_in_number_set(self, number_set, **defaults_config): ''' Given a number set number_set (such as Integer, Real, etc), attempt to prove that the given expression is in that number set using the appropriate closure theorem. ''' import proveit.numbers.absolute_value as abs_pkg from proveit.numbers import ( ZeroSet, Natural, NaturalPos, Integer, IntegerNonZero, Rational, RationalNonZero, RationalPos, RationalNonNeg, Real, RealNonNeg, RealPos, RealNonZero, ComplexNonZero) thm = None if number_set == ZeroSet: thm = abs_pkg.abs_zero_closure elif number_set in (NaturalPos, IntegerNonZero): thm = abs_pkg.abs_integer_nonzero_closure elif number_set in (Integer, Natural): thm = abs_pkg.abs_integer_closure elif number_set in (RationalPos, RationalNonZero): thm = abs_pkg.abs_rational_nonzero_closure elif number_set in (Rational, RationalNonNeg): thm = abs_pkg.abs_rational_closure elif number_set in (RealPos, RealNonZero, ComplexNonZero): thm = abs_pkg.abs_nonzero_closure else: thm = abs_pkg.abs_complex_closure if thm is not None: in_set = thm.instantiate({a: self.operand}) if in_set.domain == number_set: # Exactly the domain we were looking for. return in_set # We must have proven we were in a subset of the # one we were looking for. return InSet(self, number_set).prove() # To be thorough and a little more general, we check if the # specified number_set is already proven to *contain* one of # the number sets we have theorems for -- for example, # Y=Complex contain X=Real, and # Y=(-1, inf) contains X=RealPos, # but we don't have specific thms for those supersets Y. # If so, use the appropiate thm to determine that self is in X, # then prove that self must also be in Y since Y contains X. if SubsetEq(Real, number_set).readily_provable(): abs_pkg.abs_complex_closure.instantiate({a: self.operand}) return InSet(self, number_set).prove() if SubsetEq(RealPos, number_set).readily_provable(): abs_pkg.abs_nonzero_closure.instantiate({a: self.operand}) return InSet(self, number_set).prove() if SubsetEq(RealNonNeg, number_set).readily_provable(): abs_pkg.abs_complex_closure_non_neg_real.instantiate({a: self.operand}) return InSet(self, number_set).prove() # otherwise, we just don't have the right thm to make it work raise NotImplementedError( "'Abs.deduce_in_number_set()' not implemented for " "the %s set" % str(number_set))
def readily_provable_number_set(self): ''' Return the most restrictive number set we can readily prove contains the evaluation of this number operation. ''' from proveit.numbers import ( ZeroSet, Integer, IntegerNonZero, NaturalPos, Natural, Rational, RationalNonZero, RationalPos, RationalNonNeg, Real, RealNonNeg, RealPos, RealNonZero, ComplexNonZero, Complex) operand_ns = readily_provable_number_set(self.operand, default=Complex) if operand_ns is None: return None if operand_ns == ZeroSet: return ZeroSet if IntegerNonZero.readily_includes(operand_ns): return NaturalPos if Integer.readily_includes(operand_ns): return Natural if RationalNonZero.readily_includes(operand_ns): return RationalPos if Rational.readily_includes(operand_ns): return RationalNonNeg if RealNonZero.readily_includes(operand_ns): return RealPos if Real.readily_includes(operand_ns): return RealNonNeg if ComplexNonZero.readily_includes(operand_ns): return RealPos return RealNonNeg @equality_prover('unit_length_simplified', 'unit_length_simplify') def unit_length_simplification(self, **defaults_config): ''' |exp(i * theta)| = 1 simplification given theta in Real. ''' from proveit.numbers import unit_length_complex_polar_angle from . import complex_unit_length replacements = set() _theta = unit_length_complex_polar_angle( self.operand, reductions=replacements) # |exp(i*theta)| = 1 return complex_unit_length.instantiate( {theta:_theta}, replacements=replacements) @equality_prover('chord_length_simplified', 'chord_length_simplify') def chord_length_simplification(self, **defaults_config): ''' |r exp(i a) - r exp(i b)| = 2 r sin(|a - b|/2) or |x exp(i a) - x exp(i b)| = 2 |x| sin(|a - b|/2) simplification given a, b in Real and either r in RealNonNeg or x in Real (depending upon what is known). ''' from proveit.numbers import (one, two, Add, Neg, subtract, Div, complex_polar_coordinates) from proveit.trigonometry import (complex_unit_circle_chord_length, complex_circle_chord_length) def raise_not_valid_form(): raise ValueError( "Complex circle coord length is only applicable to " "expressions of the form |r exp(i a) - r exp(i b)| " "or obviously equivalent. " "%s does not qualify." % self) if not (isinstance(self.operand, Add) and self.operand.operands.is_double()): raise_not_valid_form() replacements = set() term1 = self.operand.terms[0] term2 = self.operand.terms[1] if isinstance(term2, Neg): term2 = term2.operand else: term2 = Neg(term2) replacements.add(Neg(term2).double_neg_simplification( preserve_all=True)) _r1, _theta1 = complex_polar_coordinates( term1, reductions=replacements) _r2, _theta2 = complex_polar_coordinates( term2, reductions=replacements) if _r1 == _r2: if _r1 == one: return complex_unit_circle_chord_length.instantiate( {a:_theta1, b:_theta2}, replacements=replacements) else: return complex_circle_chord_length.instantiate( {r: _r1, a:_theta1, b:_theta2}, replacements=replacements) raise_not_valid_form() @relation_prover def deduce_triangle_bound(self, **defaults_config): ''' Return the proven triangle bound (or generalized triangle bound) of this absolute value. For example, |a + b| ≤ |a| + |b| or |x_1 + ... + x_n| ≤ |x_1| + ... + |x_n| for the generalized triangle bound. The terms of the sum must be complex numbers. ''' from proveit.numbers import Add, Sum from . import triangle_inequality, generalized_triangle_inequality if isinstance(self.operand, Sum): # We should add a theorem for the triangle bound applicable # to a general summation. raise NotImplementedError("The triangle bound for a summation " "has not been implemented just yet.") if not isinstance(self.operand, Add): raise ValueError("The triangle bound is only applicable on " "the absolute value over a sum, not %s") terms = self.operand.terms if terms.is_double(): return triangle_inequality.instantiate({a:terms[0], b:terms[1]}) else: _n = terms.num_elements() return generalized_triangle_inequality.instantiate( {n:_n, x:terms}) @relation_prover def deduce_strict_upper_bound(self, bound, **defaults_config): # Deduce that this absolute value has the given strict lower # bound by bounding the operand. For example, # |a| < c given -c < a < c. from . import strict_upper_bound return strict_upper_bound.instantiate( {a:self.operand, c:bound}) @relation_prover def deduce_weak_upper_bound(self, bound,**defaults_config): # Deduce that this absolute value has the given weak lower # bound by bounding the operand. For example, # |a| ≤ c given -c ≤ a ≤ c. from . import weak_upper_bound return weak_upper_bound.instantiate( {a:self.operand, c:bound}) @relation_prover def deduce_positive(self, **defaults_config): # Deduce that this absolute value is greater than zero # given its argument is not equal zero. from proveit.numbers import RealPos, zero, greater InSet(self, RealPos).prove() return greater(self, zero).prove()
""" def is_equal_to_or_subset_eq_of( number_set, equal_sets=None, subset_sets=None, subset_eq_sets=None, assumptions=None): ''' A utility function used in the do_reduced_simplification() method to test whether the number set specified by number_set: • is equal to any of the number sets provided in the list of equal_sets • OR is already known/proven to be a proper subset of any of the number sets provided in the list of subset_sets, • OR is already known/proven to be an improper subset of any of the number sets provided in the list of subset_eq_sets, returning True at the first such equality, subset, or subset_eq relation found to be True. ''' # among other things, convert any assumptions=None # to assumptions=() (thus averting len(None) errors) assumptions = defaults.checked_assumptions(assumptions) if equal_sets is not None: for temp_set in equal_sets: if number_set == temp_set: return True if subset_eq_sets is not None: for temp_set in subset_eq_sets: if SubsetEq(number_set, temp_set).readily_provable(assumptions): return True if subset_sets is not None: for temp_set in subset_sets: if ProperSubset(number_set, temp_set).readily_provable(assumptions): return True return False """