# Demonstrations for the theory of proveit.core_expr_types.tuples¶

In [1]:
import proveit
from proveit import (Lambda, ExprTuple, ExprRange, IndexedVar, safe_dummy_var,
defaults, Function, ProofFailure)
from proveit import A, a, b, f, g, i, j, k, l, m, n, x, y
from proveit.logic import Equals, NotEquals, Not, EvaluationError, InSet
from proveit.linear_algebra import TensorProd
from proveit.numbers import (zero, one, two, three, four, e as e_nat, Add, Exp,
Integer, Mult, Natural, NaturalPos, Neg, num, subtract)
from proveit.core_expr_types import Len
from proveit.core_expr_types import (
a_i_to_j, x_1_to_n, y_1_to_n, f_i_to_j, f_i_to_jp1)
from proveit.core_expr_types.tuples import (
len_of_ranges_with_repeated_indices_from_1, range_from1_len,
len_of_ranges_with_repeated_indices_from_1, len_of_ranges_with_repeated_indices,
len_of_empty_range_of_ranges)
from proveit.core_expr_types.tuples import general_range_of_ranges
%begin demonstrations


### Proving the equality of ExprTuples¶

In [2]:
Equals(ExprTuple(a, b, x, y), ExprTuple(a, b, x, y)).prove()

In [3]:
ExprTuple(a, b, x, y).deduce_equal_or_not(ExprTuple(x, y))

In [4]:
ExprTuple(a, b, x, y).deduce_equal_or_not(
ExprTuple(x, b, x, y), assumptions=[NotEquals(a, x)])

In [5]:
defaults.assumptions = [InSet(n, NaturalPos)]

defaults.assumptions:
In [6]:
partitioned = x_1_to_n.partition(one, assumptions=[InSet(n, NaturalPos)])

partitioned:
In [7]:
eq = Equals(ExprTuple(*partitioned.lhs.entries, y),
ExprTuple(*partitioned.rhs.entries, y))

eq:
In [8]:
eq.prove(assumptions=[InSet(n, NaturalPos)])

In [9]:
shifted = x_1_to_n.shift_equivalence(new_start=zero, assumptions=[InSet(n, NaturalPos)])

shifted:
In [10]:
eq = Equals(ExprTuple(*shifted.lhs.entries, y),
ExprTuple(*shifted.rhs.entries, y))

eq:
In [11]:
eq.lhs.inner_expr()[0].partition(one)

In [12]:
eq.lhs.deduce_equal(eq.rhs, assumptions=[InSet(n, NaturalPos)])

In [13]:
eq = Equals(ExprTuple(a, y, *partitioned.lhs.entries),
ExprTuple(a, y, *partitioned.rhs.entries))

eq:
In [14]:
eq.prove(assumptions=[InSet(n, NaturalPos)])

In [15]:
eq.lhs.deduce_equal(eq.rhs, assumptions=[InSet(n, NaturalPos)])


### Mapping elements can be useful for building new ExprTuples from existing ones¶

In [16]:
eq.lhs.map_elements(lambda x : Not(x))

In [17]:
ExprTuple.map_elements_together(lambda x, y : Equals(x, y), eq.lhs, eq.lhs)


For efficiency, this is limited: ExprRanges must be aligned

In [18]:
try:
ExprTuple.map_elements_together(lambda x, y : Equals(x, y), eq.lhs, eq.rhs)
assert False, "ValueError expected"
except ValueError as e:
print("Expected error:", e)

Expected error: Each of the ExprTuples must have the same number of entries when mapping elements together


### Testing the ExprRange(order='decreasing') flag¶

An ExprRange with the order='decreasing' flag produces an ExprRange of the form f(i),...,f(j), where 0 <= (i-j) and j < i (i.e. the ExprRange represents 0 or more elements and is in decreasing order)

For example, if

self = $f(3),...,f(6)$,

then order='decreasing' would return:

$|- f(6),...,f(3)$

In [19]:
test = ExprRange(i, IndexedVar(a, i), j, zero, order='decreasing')

test:
In [20]:
inc_test = ExprRange(i, IndexedVar(a, i), j, zero)

inc_test:
In [21]:
try:
ExprRange(i, IndexedVar(a, i), two, zero, order='increasing')
assert False, "Expecting a ValueError; should not get this far!"
except ValueError as _e:
print("Expected exception: ", _e)

Expected exception:  Invalid ExprRange endpoints: 2 to 0

In [22]:
ExprRange(i, IndexedVar(a, i), two, zero, order='decreasing')

In [23]:
test.lambda_map

In [24]:
(test.start_index, test.end_index, test.true_start_index, test.true_end_index)

In [25]:
(inc_test.start_index, inc_test.end_index,
inc_test.true_start_index, inc_test.true_end_index)

In [26]:
test.body

In [27]:
inc_test.body

In [28]:
test.first()

In [29]:
inc_test.first()

In [30]:
test.last()

In [31]:
inc_test.last()

In [32]:
empty_test_inc = ExprRange(i, IndexedVar(a, i), one, zero, order='increasing')

empty_test_inc:
In [ ]:


In [33]:
empty_test_inc.reduction()

In [34]:
empty_test_dec = ExprRange(i, IndexedVar(a, i), zero, one, order='decreasing')

empty_test_dec:
In [35]:
empty_test_dec.reduction()

In [ ]:


In [36]:
empty_test_dec.lambda_map

In [37]:
partition_test_inc = ExprRange(i, IndexedVar(a, i), zero, four, order='increasing')

partition_test_inc:
In [38]:
partition_test_inc.partition(two)

In [39]:
partition_test_dec = ExprRange(i, IndexedVar(a, i), four, zero, order='decreasing')

partition_test_dec:
In [40]:
partition_test_dec.start_index, partition_test_dec.true_start_index

In [41]:
partition_test_dec.partition(two)

In [ ]:


In [42]:
from proveit import fa
from proveit.numbers import Complex

In [43]:
assumptions = [InSet(Add(j, Neg(i), one), Natural),
InSet(i, Natural), InSet(j, Natural)]

assumptions:
In [44]:
f_i_to_j_dec = ExprRange(a, fa, i, j, order='decreasing')

f_i_to_j_dec:
In [ ]:


In [45]:
from proveit.core_expr_types.tuples import negated_shift_equivalence

In [46]:
negated_shift_equivalence

In [47]:
# negated_shift_equivalence.instantiate({i:Neg(i), j:Neg(j), k:subtract(i, one), a:Neg(one), l:subtract(j, one)}, assumptions=[InSet(subtract(subtract(Neg(j), one), Neg(i)),
# #                                                                  Natural), InSet(subtract(subtract(j, one), i),
#                                                                  Natural)])

In [48]:
# f_i_to_j_dec.shift_equivalence(new_shift=one, assumptions=[InSet(subtract(subtract(Neg(j), one), Neg(i)),
#                                                                  Natural)])

In [49]:
# f_i_to_j__shift__eq_dec = \
#     f_i_to_j_dec.shift_equivalence(new_shift=one, assumptions=[InSet(subtract(subtract(Neg(j), one), Neg(i)),
#                                                                  Natural)]).lhs.entries[0]

In [50]:
# assert False

In [51]:
Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, zero), one, n)).computation(assumptions=[InSet(n, NaturalPos)])

In [52]:
Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), two, n), one, zero)).computation(assumptions=[InSet(n, Natural)])

In [53]:
Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, n), one, n)).computation(assumptions=[InSet(n, Natural), InSet(n, NaturalPos)])

In [54]:
Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, zero), two, one)).computation(assumptions=[InSet(n, Natural)])


The following 5 cells have been commented out — they create and then depend on the one-element expr_range in the first cell, which returns an error

In [55]:
# expr_range = ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, one), one, one)

In [56]:
# lambda_map = Lambda((expr_range.parameter, expr_range.body.parameter), expr_range.body.body)

In [57]:
# singular_nested_range_reduction.instantiate({f:lambda_map, i:one, j:one, m:one})

In [58]:
# Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, one), one, one)).computation()

In [59]:
# Len(ExprRange(i, ExprRange(j, IndexedVar(a, [i, j]), one, two), one, one)).computation()

In [60]:
assumptions = [InSet(Add(j, Neg(i), one), Natural),
InSet(i, Natural), InSet(j, Natural)]

assumptions:
In [61]:
f_i_to_jp1

In [62]:
eq = f_i_to_jp1.partition(j, assumptions=assumptions)

eq:
In [63]:
eq.rhs.merger(assumptions=assumptions)

In [64]:
f_i_to_j__shift__eq = \
f_i_to_j.shift_equivalence(new_shift=one, assumptions=[InSet(subtract(Add(j, one), i),
Natural)])

f_i_to_j__shift__eq:
In [65]:
f_i_to_j__shift__eq.rhs

In [66]:
Add(subtract(i, one), one).simplification(assumptions=[InSet(i, Integer)])

In [67]:
Add(Add(i, Neg(two)), two).simplification(assumptions=[InSet(i, Integer)])

In [68]:
Add(subtract(j, one), one).simplification(assumptions=[InSet(j, Integer)])

In [69]:
Add(subtract(j, two), two).simplification(assumptions=[InSet(j, Integer)])

In [70]:
f_i_to_j__shift__eq.rhs.entries[0].shift_equivalence(
old_shift=one, new_shift=two,
assumptions=[InSet(j, Integer), InSet(i, Integer),
InSet(subtract(j, subtract(i, one)), Natural)])

, ,  ⊢
In [ ]:


In [ ]:


In [71]:
from proveit import fa
from proveit.numbers import Complex

In [72]:
f_i_to_j_dec = ExprRange(a, fa, i, j, order='decreasing')

f_i_to_j_dec:
In [73]:
assumptions = [InSet(Add(Neg(j), i, Neg(one)), Natural),
InSet(i, Natural), InSet(j, Natural)]

assumptions:
In [74]:
#InSet(Neg(Add(x, one)), Complex).prove(assumptions=[InSet(x, Complex)])

In [75]:
Neg(Add(Neg(Add(x, one)), one)).distribution(assumptions=[InSet(x, Complex)])

In [76]:
InSet(subtract(subtract(Neg(j), one), Neg(i)), Natural)

In [77]:
# f_i_to_j__shift__eq_dec = \
#     f_i_to_j_dec.shift_equivalence(new_shift=one, assumptions=[InSet(subtract(subtract(Neg(j), one), Neg(i)),
#                                                                  Natural)]).lhs.entries[0]

In [78]:
# lhs_done = f_i_to_j__shift__eq_dec.inner_expr().lhs[0].with_decreasing_order()

In [79]:
# lhs_done.inner_expr().rhs[0].with_decreasing_order()

In [80]:
# f_i_to_j__shift__eq_dec.rhs.entries[0].shift_equivalence(
#     old_shift=one, new_shift=two,
#     assumptions=[InSet(j, Integer), InSet(i, Integer),
#                  InSet(subtract(j, subtract(i, one)), Natural)])

In [81]:
tup=ExprTuple(a, b)

tup:
In [82]:
Len(a_i_to_j).computation(assumptions=[InSet(Add(j, Neg(i), one), Natural)])

In [83]:
tup_jdgmt = tup.prove(assumptions=[tup])

tup_jdgmt:

Not clear what the following cell is/was trying to accomplish:

In [84]:
# tup.prove(assumptions=[tup]).instantiate({a:a_i_to_j},
#                             assumptions=[InSet(Add(j, Neg(i), one), Natural)])

In [85]:
eq = f_i_to_jp1.partition(k, assumptions=[InSet(subtract(Add(k, one), i), Natural),
InSet(subtract(Add(j, one), k), Natural)])

eq: ,  ⊢
In [86]:
eq.rhs.merger(assumptions=[InSet(subtract(Add(k, one), i), Natural),
InSet(subtract(Add(j, one), k), Natural)])

In [87]:
eq = f_i_to_jp1.partition(i, assumptions=[InSet(subtract(Add(j, one), i), Natural)])

eq:
In [88]:
eq.rhs.merger(assumptions=[InSet(subtract(Add(j, one), i), Natural)])

In [89]:
eq = f_i_to_j.partition(subtract(j, one), assumptions=[InSet(subtract(j, i), Natural)])

eq:
In [90]:
Add(subtract(j, one), one).simplification(assumptions=[InSet(j, Natural)])

In [91]:
eq.rhs.merger(assumptions=[InSet(subtract(j, i), Natural), InSet(j, Natural)])

In [ ]:



### Testing the ExprTuple.range_expansion() method¶

For self an ExprTuple with a single entry that is an ExprRange of the form f(i),...,f(j), where 0 <= (j-i) <= 9 (i.e. the ExprRange represents 1 to 10 elements), derive and return an equality between self and an ExprTuple with explicit entries replacing the ExprRange. For example, if

self = ExprTuple$(f(3),...,f(6))$,

then self.range_expansion() would return:

$|- (f(3),...,f(6)) = (f(3), f(4), f(5), f(6))$

First not that we cannot create an ExprRange with only one element explicitly:

In [92]:
try:
ExprTuple(ExprRange(a, Function(g, a), two, two))
assert False, "Expecting a ValueError"
except ValueError as e:
print("Expected Error:", e)

Expected Error: Do not create an ExprRange with the same start and end index since it reduces to a single instance.  Note that nested_range/var_range automatically perform this reduction.


We can, however, create an ExprRange that doesn't obviously have one element but may turn out to have one element after a simplification or substitution.

In [93]:
expr_tuple_with_1_elem_range = ExprTuple(ExprRange(a, Function(g, a), two, Mult(one, two)))

expr_tuple_with_1_elem_range:
In [94]:
expr_tuple_with_1_elem_range.simplification()


ExprRange indices are already expected to be simplified w.r.t. quick_simplified_index from proveit.numbers, however, which deals with basic Add and Neg simplifications and combines all literal integers at the end of an Add.

In [95]:
try:
# A one-element ExprRange (hidden by choosing the start and end indices
# that are equal but appear different)
example_expr_range_2 = ExprRange(i, IndexedVar(x, i), one, Add(one, zero))
assert False, "Expecting ValueError"
except ValueError as e:
print("Expected Error:", e)

Expected Error: Start and end indices must be in the 'quick_simplified_index' canonical form: (1, 1 + 0) ≠ (1, 1)


range_expansion does the same thing as simplification in this case:

In [96]:
expr_tuple_with_1_elem_range.range_expansion()

In [97]:
# generate some example ExprTuples each containing a single ExprRange element
expr_tuple_with_2_elem_range, expr_tuple_with_2_elem_range_exp, expr_tuple_with_3_elem_range, expr_tuple_with_unknown_elem_range, expr_tuple_too_big = [
ExprTuple(ExprRange(a, Function(g, a), two, three)),
ExprTuple(ExprRange(a, Exp(two, Add(a, one)), two, three)),
ExprTuple(ExprRange(a, Exp(e_nat, Add(a, j)), two, four)),
ExprTuple(ExprRange(a, Exp(e_nat, Add(a, j)), i, k)),
ExprTuple(ExprRange(a, Function(g, a), two, num(20)))]

expr_tuple_with_2_elem_range:
expr_tuple_with_2_elem_range_exp:
expr_tuple_with_3_elem_range:
expr_tuple_with_unknown_elem_range:
expr_tuple_too_big:
In [98]:
# find equivalent explicitly 2-element ExprTuple
expr_tuple_with_2_elem_range.range_expansion()

In [99]:
# find equivalent explicitly 2-element ExprTuple
# notice the automatic simplification
expr_tuple_with_2_elem_range_exp.range_expansion()

In [100]:
# find equivalent explicitly 2-element ExprTuple
# notice the automatic simplification
expr_tuple_with_3_elem_range.range_expansion()

In [101]:
# When the number of elements represented by the ExprRange is not known,
# the range_expansion() method fails with an informative error message
try:
expr_tuple_with_unknown_elem_range.range_expansion()
assert False, "Expecting an EvaluationError; should not get this far!"
except EvaluationError as the_error:
print("EvaluationError: {}".format(the_error))

EvaluationError: Evaluation of k - i under assumptions {n in NaturalPos} is not known. The ExprRange e^{i + j}, e^{(i + 1) + j}, ..., e^{k + j} must represent a known, finite number of elements, but all we know is that it represents k - i elements.
EvaluationError: Evaluation of k - i under assumptions {n in NaturalPos} is not known

In [102]:
# but if we give the method enough information about the indexing
# we can generate the equivalent explicit ExprTuple
expr_tuple_with_unknown_elem_range.range_expansion(
assumptions=[Equals(k, Add(i, four)), Equals(subtract(k, i), four)])

In [103]:
# When the number of elements represented by the ExprRange is > 10,
# the range_expansion() method fails with an informative error message
try:
expr_tuple_too_big.range_expansion(assumptions=[Equals(subtract(num(20), two), num(18))])
assert False, "Expecting an EvaluationError; should not get this far!"
except ValueError as the_error:
print("ValueError: {}".format(the_error))

ValueError: ExprTuple.range_expansion() implemented only for ExprTuples with a single entry, with the single entry being an ExprRange representing a finite number of elements n with 1 <= n <= 9. Instead, the ExprTuple is g(2), g(3), ..., g(20) with number of elements equal to 19.

In [104]:
# a related issue to ask about
try:
Equals(subtract(num(20), two), num(18)).prove()
except ProofFailure as the_error:
print("ProofFailure: {}".format(the_error))

ProofFailure: Unable to prove (20 - 2) = 18 assuming {n in NaturalPos}:
'conclude' method not implemented for proof automation


A related example where the ExprRange and ExprTuple are being used as an argument for a TensorProd operator.

In [105]:
# create an example ExprRange
example_expr_range = ExprRange(i, IndexedVar(x, i), one, three)

example_expr_range:
In [106]:
# use the example ExprRange as the arg(s) for a TensorProd:
example_tensor_prod_over_range = TensorProd(example_expr_range)

example_tensor_prod_over_range:
In [107]:
# find the ExprTuple equivalent to the (ExprTuple-wrapped) ExprRange:
expr_range_eq_expr_tuple = ExprTuple(example_expr_range).range_expansion()

expr_range_eq_expr_tuple:
In [108]:
# find the equivalent explicit tensor prod
example_tensor_prod_over_range.inner_expr().operands.substitution(
expr_range_eq_expr_tuple)

In [109]:
%end demonstrations