Demonstrations for the theory of proveit.numbers.absolute_value ¶

import proveit
from proveit import ExprRange, IndexedVar, used_vars, free_vars
from proveit import a, b, c, k, n, r, x, y, theta
from proveit.core_expr_types import x_1_to_n
from proveit.logic import And, Equals, InSet, NotEquals
from proveit.numbers import zero, one, two, three, e, i, pi
from proveit.numbers import (Abs, Add, frac, Exp, greater,
                            greater_eq, Less, LessEq, Mult, Neg)
from proveit.numbers import (Complex, Integer, Natural, NaturalPos,
                            Real, RealPos, RealNeg, RealNonNeg, RealNonPos)
from proveit.numbers.absolute_value  import abs_val_def_sqrt
%begin demonstrations

Absolute Value (and norm) $|a|$¶

Introduction
Simple Expressions Involving Absolute Value $|a|$
Common Attributes of an Absolute Value Expression
Axioms
Theorems
Further Demonstrations

Simplifying $|x+1|$ and Deducing Number Sets
Simplifying $|a+b+2+3|$ and Deducing Number Sets
Simplifying $1 + |x+1|$

Misc Testing (temporary)

Introduction ¶

The concept of the absolute value of a real number, and its generalization to the norm if a complex number, is ubiquitous in mathematics and often serves a key role in various proofs. The absolute value of a real number $x$, or the norm of a complex number $x$, is captured with the operation `Abs(x)`, along with a standard axiomatic definition and a variety of related theorems.

Simple Expressions Involving Absolute Value $|a|$ ¶

It is straightforward to construct absolute value expressions. Here are some basic examples of such expressions:

# basic absolute value expression
abs_value_a = Abs(a)

# a version of the triangle inequality, where Abs() occurs repeatedly
# inside a larger expression
LessEq(Abs(Add(a, b)), Add(Abs(a),Abs(b)))

Common Attributes of an Absolute Value `Abs` Expression ¶

Let's define a simple absolute value expression, $|a+b|$, and look at some of its attributes.

abs_value_a_plus_b = Abs(Add(a, b))

We can use the `expr_info()` method to look at how the expression is constructed:

abs_value_a_plus_b.expr_info()

The string version of the absolute value operator is simply the `Abs` string:

abs_value_a_plus_b.operator

And we can test for instances of `Abs()` in the usual way, by testing for the `Abs` class:

if isinstance(abs_value_a_plus_b, Abs):
    print("{} is an instance of Abs".format(abs_value_a_plus_b))

|a + b| is an instance of Abs

We can obtain the operand (the expression inside the absolute value) apart from the `Abs()` expression. We can also get a list of the variables and a separate list of the *free* variables in the expression (of course, in this expression, all the variables are also free variables):

# the "bare" operand
abs_value_a_plus_b.operand

# the operand in a (1-element) tuple
abs_value_a_plus_b.operands

# the variables appearing in the expression
used_vars(abs_value_a_plus_b)

# the free variables appearing in the expression
free_vars(abs_value_a_plus_b)

And of course, we can reach into the expression and substitute for variables with other variables in the usual way:

abs_value_c_plus_b = abs_value_a_plus_b.basic_replaced({a:c})

Axioms ¶

At this time, there is a single axiom for absolute value, defining $|x|=\sqrt{x^2}$ for real-valued $x$:

abs_val_def_sqrt

When the `Conditional` class has been established, the axiomatic definition will use the standard piece-wise definition, and the “square root of the square” could then be a theorem instead. The definition for $|a+bi|$, the norm of complex number $z=a+bi$, is still under development.

Theorems ¶

Some typical absolute value-related theorems are illustrated below. The full complement of theorems appears in the `proveit.numbers/absolute_value/_theorems_.ipynb` notebook.

from proveit.numbers.absolute_value import (
        abs_nonzero_closure, abs_is_non_neg, abs_non_neg_elim, triangle_inequality)

# abs value of a non-zero value is a positive real number
abs_nonzero_closure

# abs value of any number is non-negative
abs_is_non_neg

# we can eliminate the abs value wrapper around a non-negative real number
abs_non_neg_elim

# abs value version of a triangle inequality thm
triangle_inequality

Demonstrations ¶

1. Simplifying $|x+1|$ and Deducing Number Sets

Consider the very simple absolute value expression $|x+1|$, where the operand is a sum of a variable and known constant:

demo_expr_01 = Abs(Add(x, one))

The general expression simplification() method can eliminate the absolute value wrapper under the right conditions — for example, when we know that $x$ is a positive real number:

demo_expr_01

demo_expr_01.simplification(assumptions=[InSet(x, RealPos)])

We can deduce that the absolute value expression is in a specific number set (given the right assumptions):

demo_expr_01.deduce_in_number_set(RealNonNeg, assumptions=[InSet(x, Real)])

Now when $x \in \mathbb{R}^{+}$, we should have $|x+1|>1$ and thus $|x+1| \in \mathbb{R}^{+}$. Interestingly, this requires a little more work before Prove-It agrees:

from proveit import InstantiationFailure
try:
    demo_expr_01.deduce_in_number_set(RealPos, assumptions=[InSet(x, RealPos)])
except InstantiationFailure as _e:
    print("SpecializationFailure: " + str(_e))

We could include the information the system seems to want, i.e., that $x+1 \ne 0$, and Prove-It is happy:

demo_expr_01.deduce_in_number_set(
    RealPos,
    assumptions=[InSet(x, RealPos), NotEquals(Add(x, one), zero)])

But that seems a little clunky, with that additional (and redundant) assumption appearing in the result. Instead we can nudge Prove-It by first having it prove that the operand $x+1$ is itself a positive real value, and then it has no problem proving that the absolute value expression $|x+1|$ itself is also a positive real value:

InSet(Add(x, one), RealPos).prove(assumptions=[InSet(x, RealPos)])

InSet(demo_expr_01, RealPos).prove(assumptions=[InSet(x, RealPos)])

2. Simplifying $|a+b+2+3|$ and Deducing Numbers Sets

Now consider a simple absolute value expression, where the operand is a sum of variables and known constants: $|a+b+2+3|$

demo_expr_02 = Abs(Add(a, b, two, three))

We can obtain simplification equivalences, depending on our assumptions about the nature of the variables $a$ and $b$. If $a$ and $b$ are complex numbers or real numbers, for example, Prove-It simplifies the $2+3$ portion to $5$ and keeps the absolute value:

# variables a and b are complex, notated as a tuple
demo_expr_02.simplification(assumptions=[InSet(a, Complex), InSet(b, Complex)])

# variables a and b are real, notated individually
demo_expr_02.simplification(assumptions=[InSet(a, Real), InSet(b, Real)])

We can simplify further if we know that $a$ and $b$ are non-negative reals, with `simplification()` combining the numerical constants *and* removing the absolute value:

demo_expr_02.simplification(
    assumptions=[InSet(a, RealNonNeg), InSet(b, RealNonNeg)])

Similarly, given the assumption that $a$ and $b$ are non-negative reals, we can explicitly deduce that the entire expression is also a non-negative real:

demo_expr_02.deduce_in_number_set(
        RealNonNeg,
        assumptions=[InSet(a, RealNonNeg), InSet(b, RealNonNeg)])

In fact, as long as we explicitly establish that $a$ and $b$ each belong to some defined subset of the complex numbers, the `deduce_in_number_set()` will be able to deduce that our absolute value expression is an element of the non-negative real numbers:

demo_expr_02.deduce_in_number_set(
        RealNonNeg,
        assumptions=[InSet(a, Complex), InSet(b, RealNeg)])

From this, it is straighforward to derive $|a + b + 2 + 3| \geq 0$ exploiting some automation:

demo_expr_02_ge_zero = greater_eq(demo_expr_02, zero).prove(
    assumptions=[InSet(a, Complex), InSet(b, RealNeg)])

The detailed proof includes a number of steps that establish that all the sub-operands can be found in the complex numbers, but we see toward the top of the proof table the explicit use of the modus ponens-like `right_from_iff` theorem (cited in line 1) and the `in_real_non_neg_iff_nonNegative` theorem (cited in line 5), which we were nudging Prove-It toward by our few steps above:

demo_expr_02_ge_zero.proof()

3. Simplifying $1 + |x+1|$

Consider the simple expression $1 + |x+1|$ involving the sum of a constant and an absolute value expression.

demo_expr_03 = Add(one, Abs(Add(x, one)))

If we know that $x\in \mathbb{R}^{+}$, simplification should be able to eliminate the absolute value and commute and combine the known constants:

demo_expr_03.simplification(assumptions=[InSet(x, RealPos)])

Misc Testing¶

The material below was developed to test various absolute_value methods. Some of this material could be integrated into the `_demonstrations_` page eventually and/or deleted as development continues.

Some Example `Abs` Expressions For Testing¶

abs_value_1_plus_2 = Abs(Add(one, two))

abs_value_a_plus_b = Abs(Add(a, b))

abs_value_a_plus_2 = Abs(Add(a, two))

abs_value_a_times_b = Abs(Mult(a, b))

abs_value_a_div_b = Abs(frac(a,b))

from proveit.trigonometry import Sin
abs_value_sin_x = Abs(Sin(x))

from proveit.trigonometry import Cos
abs_value_cos_x = Abs(Cos(x))

Testing the `deduce_in_number_set()` method¶

abs_value_1_plus_2.deduce_in_number_set(Real)

abs_value_1_plus_2.deduce_in_number_set(RealPos)

# Abs(x) is real when x is complex
abs_value_a_plus_b.deduce_in_number_set(
    Real, assumptions=[InSet(Add(a,b), Complex)])

# Abs(a+b) is real if a is real and b a positive natural, etc
abs_value_a_plus_b.deduce_in_number_set(
    Real, assumptions=[InSet(a, Real), InSet(b, NaturalPos)])

# Abs(a+2) is real if a is real
abs_value_a_plus_2.deduce_in_number_set(
    Real, assumptions=[InSet(a, Real)])

abs_value_a_plus_b.deduce_in_number_set(RealPos,
    assumptions=[InSet(a, Complex),
                 InSet(b, Complex),
                 NotEquals(Add(a,b), zero)])

abs_value_1_plus_2.deduce_in_number_set(RealNonNeg)

abs_value_a_plus_b.deduce_in_number_set(RealNonNeg,
    assumptions=[InSet(a, Complex), InSet(b, Complex)])

# what happens if we try to deduce into an incorrect set?
try:
    abs_value_a_plus_b.deduce_in_number_set(RealNeg,
        assumptions=[InSet(Add(a,b), Complex)])
    assert False
except Exception as _e:
    print("Expected Exception: ", _e)

Expected Exception:  Proof step failed assuming {(a + b) in Complex}:
Attempting to instantiate |- forall_{a in Real | a < 0} (a in RealNeg) with {a: |a + b|}:
Unsatisfied condition: |a + b| < 0. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

# but of course, the Complex numbers contain the non-negative Real numbers …
# so it would be nice to be able to be able to deduce_in_number_set(X) if
# X contains a set Y for which deduce_in_number_set(Y) is possible …
abs_value_a_plus_b.deduce_in_number_set(Complex,
    assumptions=[InSet(Add(a,b), Complex)])

Testing the `Abs.deduce_not_equal()` method¶

# recall our Abs(Add(a, b)) expression
abs_value_a_plus_b

abs_value_a_plus_b.deduce_not_equal(
    zero,
    assumptions=[InSet(a, Complex),
                 InSet(b, Complex),
                 NotEquals(Add(a,b), zero)])

# And automation will generally be able to prove
# Abs(x) ≠ 0 when x in a defined set with x ≠ 0.
NotEquals(abs_value_a_plus_b, zero).prove(
    assumptions=[InSet(Add(a,b), Real), NotEquals(Add(a,b), zero)])

Testing the `Abs.abs_elimination()` method¶

# abs_elimination() by itself often needs some
# pre-processing of the expression operand
try:
    abs_value_1_plus_2.abs_elimination()
except Exception as _e:
    print("EXCEPTION: ", _e)

# So prove 1+2 is non-negative real first
InSet(Add(one, two), RealPos).prove()

# And then we should be able to use the basic Abs.abs_elimination()
abs_value_1_plus_2.abs_elimination()

abs_value_a_plus_b.abs_elimination(
    assumptions = [InSet(Add(a,b), RealPos)])

Testing the `Abs.deduce_greater_than_equals_zero()` method¶

abs_value_1_plus_2.deduce_greater_than_equals_zero()

abs_value_a_plus_b.deduce_greater_than_equals_zero(
    assumptions=[InSet(Add(a,b), Complex)])

Testing the `Abs.distribution()` method over products and fractions¶

abs_value_a_times_b

abs_value_a_div_b

abs_value_a_times_b.distribution(
     assumptions=[InSet(a, Complex), InSet(b, Complex)])

# distribution over a fraction works fine
abs_value_a_div_b.distribution(
    assumptions=[InSet(a, Complex),
                 InSet(b, Complex),
                 NotEquals(b, zero)])

abs_value_sin_x.distribution(assumptions=[InSet(x, Real)])

abs_value_cos_x.distribution(assumptions=[InSet(x, Integer)])

Absolute value is an even function which is exploited in its canonical form¶

Abs(Add(a, Neg(b), Neg(c))).canonical_form() == Abs(Add(b, c, Neg(a))).canonical_form()

True

Equals(Abs(Add(a, Neg(b), Neg(c))), Abs(Add(b, c, Neg(a)))).prove(
    assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex)])

Testing Expression simplification() on Abs() Objects¶

abs_value_1_plus_2

abs_value_1_plus_2.simplification()

abs_value_neg_three = Abs(Neg(three))

# an example suggesting we modify the do_reduced_simplification()
# to be on the lookout for double negation results?
abs_value_neg_three.simplification()

# we can simplify the double negation manually with a little work
abs_value_neg_three.simplification().inner_expr().rhs.simplify()

# after which the system now knows:
abs_value_neg_three.simplification()

# see if we can catch these in the do_reduced_simplification …
# add a greater(x, zero) or greater_eq(x, zero) to the routine
abs_value_a_plus_b.simplification(
    assumptions=[InSet(Add(a, b), Real), greater(Add(a, b), zero)])

abs_value_a_plus_b.simplification(
    assumptions=[InSet(a, RealPos), InSet(b, RealPos)])

abs_value_a_plus_b.simplification(
    assumptions=[InSet(Add(a,b), RealPos)])

abs_value_a_times_b

abs_value_a_times_b.simplification(
    assumptions=[InSet(Mult(a,b), RealPos)])

abs_value_a_times_b.simplification(
    assumptions=[InSet(a, RealPos), InSet(b, RealPos)])

# But if we don't know anything about a and b, 'simplication' will raise an exception.
from proveit import InstantiationFailure
try:
    abs_value_a_times_b.simplification()
    assert False
except InstantiationFailure as _e:
    print("Expected exception:", _e)

Expected exception: Proof step failed:
Attempting to instantiate |- forall_{n in NaturalPos} [forall_{x_{1}, x_{2}, ..., x_{n} in Complex} (|x_{1} *  x_{2} *  ... *  x_{n}| = (|x_{1}| *  |x_{2}| *  ... *  |x_{n}|))] with {n: 2, x: (a, b)}:
Unsatisfied condition: a in Complex. For debugging purposes, this is accessible via Instantiation.unsatisfied_condition with applicable assumptions in Instantiation.condition_assumptions.

abs_value_a_times_b.simplification(
    assumptions=[InSet(Mult(a,b), Natural)])

abs_value_a_times_b.simplification(
    assumptions=[InSet(a, RealNonNeg), InSet(b, RealNonNeg)])

abs_value_a_times_b.simplification(
    assumptions=[InSet(a, Natural), InSet(b, Natural)])

abs_value_a_times_b.simplification(
    assumptions=[InSet(a, RealNonNeg), InSet(b, Natural)])

# an extra test expression, slightly more interesting
test_neg = Abs(Neg(Add(Abs(a), two)))

# this one is interesting: reaching down inside an Abs to
# simplify another Abs, but not clear how it knows to do that
test_neg_simp01 = test_neg.simplification(
    assumptions=[InSet(a, RealPos)])

test_neg_simp02 = test_neg.simplification(
    assumptions=[InSet(a, RealNonNeg),
                 InSet(Add(a, two),
                 RealNonNeg)])

# then it takes a little work to then eliminate the double negative
test_neg_simp02.inner_expr().rhs.simplify(
    assumptions=[InSet(a, RealNonNeg)])

abs_value_sin_x.simplification(assumptions=[InSet(x, NaturalPos)])

abs_value_sin_x.simplification(assumptions=[InSet(x, Real)])

abs_value_cos_x.simplification(assumptions=[InSet(x, Natural)])

abs_value_cos_x.simplification(assumptions=[InSet(x, RealNeg)])

Bounding an absolute value¶

Abs(x).deduce_strict_upper_bound(y, assumptions=[Less(Neg(y), x), Less(x, y), ])

Abs(x).deduce_weak_upper_bound(y, assumptions=[LessEq(Neg(y), x), LessEq(x, y)])

Absolute values involving complex numbers in polar form¶

Abs(Mult(r, Exp(e, Mult(i, theta)))).simplification(assumptions=[InSet(r, RealNonNeg), InSet(theta, Real)])

Abs(Mult(r, Exp(e, Neg(Mult(i, theta))))).simplification(assumptions=[InSet(r, RealNonNeg), InSet(theta, Real)])

Abs(Mult(r, Exp(e, Mult(i, Neg(theta))))).simplification(assumptions=[InSet(r, RealNonNeg), InSet(theta, Real)])

Abs(Mult(r, Exp(e, Mult(Neg(theta), i)))).simplification(assumptions=[InSet(r, RealNonNeg), InSet(theta, Real)])

Abs(Mult(Neg(r), Exp(e, Mult(Neg(theta), i)))).simplification(
    assumptions=[InSet(r, RealNonNeg), InSet(theta, Real)])

Abs(Mult(r, Exp(e, Mult(i, theta)))).simplification(assumptions=[InSet(r, RealNonPos), InSet(theta, Real)])

Abs(Mult(a, Exp(e, Mult(i, theta)), b)).simplification(
    assumptions=[InSet(a, RealPos), InSet(b, RealPos), InSet(theta, Real)])

# Since we don't know the sign of 'a', we must take the absolute value.
Abs(Mult(a, b, Exp(e, Mult(i, theta)), c)).simplification(
    assumptions=[InSet(a, Real), InSet(b, RealPos), InSet(c, RealPos), InSet(theta, Real)])

Triangle inequality¶

Abs(Add(a, b)).deduce_triangle_bound(assumptions=[InSet(a, Complex), InSet(b, Complex)])

Abs(Add(a, b, x_1_to_n, c)).deduce_triangle_bound(
    assumptions=[InSet(a, Complex), InSet(b, Complex), InSet(c, Complex),
                 ExprRange(k, InSet(IndexedVar(x, k), Complex), one, n), 
                 InSet(n, Natural)])

%end demonstrations

	core type	sub-expressions
0	Operation	operator: 1 operand: 3
1	Literal
2	ExprTuple	3
3	Operation	operator: 4 operands: 5
4	Literal
5	ExprTuple	6, 7
6	Variable
7	Variable

	step type	requirements	statement
0	instantiation	1, 2	, ⊢
	:
1	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.nonneg_if_in_real_nonneg
2	instantiation	3, 4	, ⊢
	:
3	conjecture		⊢
	proveit.numbers.absolute_value.abs_complex_closure
4	instantiation	5, 6, 7, 8, 9, 10, 11	, ⊢
	: , :
5	conjecture		⊢
	proveit.numbers.addition.add_complex_closure
6	conjecture		⊢
	proveit.numbers.numerals.decimals.nat4
7	instantiation	12	⊢
	: , : , : , :
8	assumption		⊢
9	instantiation	26, 15, 13	⊢
	: , : , :
10	instantiation	26, 15, 14	⊢
	: , : , :
11	instantiation	26, 15, 16	⊢
	: , : , :
12	conjecture		⊢
	proveit.numbers.numerals.decimals.tuple_len_4_typical_eq
13	instantiation	26, 17, 18	⊢
	: , : , :
14	instantiation	26, 20, 19	⊢
	: , : , :
15	conjecture		⊢
	proveit.numbers.number_sets.complex_numbers.real_within_complex
16	instantiation	26, 20, 21	⊢
	: , : , :
17	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.real_neg_within_real
18	assumption		⊢
19	instantiation	26, 23, 22	⊢
	: , : , :
20	conjecture		⊢
	proveit.numbers.number_sets.real_numbers.rational_within_real
21	instantiation	26, 23, 24	⊢
	: , : , :
22	instantiation	26, 27, 25	⊢
	: , : , :
23	conjecture		⊢
	proveit.numbers.number_sets.rational_numbers.int_within_rational
24	instantiation	26, 27, 28	⊢
	: , : , :
25	conjecture		⊢
	proveit.numbers.numerals.decimals.nat2
26	theorem		⊢
	proveit.logic.sets.inclusion.superset_membership_from_proper_subset
27	conjecture		⊢
	proveit.numbers.number_sets.integers.nat_within_int
28	conjecture		⊢
	proveit.numbers.numerals.decimals.nat3

Demonstrations for the theory of proveit.numbers.absolute_value¶