logo

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