logo

Common expressions for the theory of proveit.core_expr_types.tuples

In [1]:
import proveit
# Prepare this notebook for defining the common expressions of a theory:
%common_expressions_notebook # Keep this at the top following 'import proveit'.
from proveit import Function, ExprRange, IndexedVar, ExprTuple
from proveit.logic import Equals, InSet
from proveit import a, b, f, k, i, j, k, l, m, n, x
from proveit.core_expr_types import (
    f_k, i_k, j_k, f_1_to_n, f_i_to_j, f_i_to_j_dec, i_1_to_n, j_1_to_n)
from proveit.numbers import Natural, one, Add, Neg
In [2]:
%begin common

Defining common sub-expressions for theory 'proveit.core_expr_types.tuples'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions
In [3]:
fk_ik_to_jk = ExprRange(x, Function(f_k, x), i_k, j_k)
fk_ik_to_jk:
In [4]:
f_ik_to_jk__1_to_n = ExprRange(k, fk_ik_to_jk, one, n)
f_ik_to_jk__1_to_n:
In [5]:
fk_i_to_j = ExprRange(x, Function(f_k, x), i, j)
fk_i_to_j:
In [6]:
f_i_to_j__1_to_n = ExprRange(k, fk_i_to_j, one, n)
f_i_to_j__1_to_n:
In [7]:
fk_1_to_i = ExprRange(x, Function(f_k, x), one, i)
fk_1_to_i:
In [8]:
f_1_to_i__1_to_n = ExprRange(k, fk_1_to_i, one, n)
f_1_to_i__1_to_n:
In [9]:
f_i_to_j__m_to_n = ExprRange(k, fk_i_to_j, m, n)
f_i_to_j__m_to_n:
In [10]:
general_range_of_ranges = ExprTuple(ExprRange(k, ExprRange(l, Function(f, (k, l)),
                                                           Function(i, k), Function(j, k)), m, n))
general_range_of_ranges:
In [11]:
range_len_conditions = ExprRange(k, InSet(Add(j_k, Neg(i_k), one), Natural), one, n)
range_len_conditions:
In [12]:
range_len_sum = Add(ExprRange(k, Add(j_k, Neg(i_k), one), one, n))
range_len_sum:
In [13]:
shift_equiv = Equals([f_i_to_j], 
                     [ExprRange(i, Function(f, Add(i, a)), k, l)])
shift_equiv:
In [14]:
f_i_to_j_dec.first()
In [15]:
f_i_to_j_dec.start_index
In [16]:
f_i_to_j_dec.get_styles()

{'order': 'decreasing',
 'front_expansion': '2',
 'back_expansion': '1',
 'wrap_positions': '()',
 'case_simplify': 'False'}
In [17]:
f_i_to_j_dec
In [18]:
neg_shift_equiv = Equals([f_i_to_j_dec], 
                     [ExprRange(i, Function(f, Add(i, a)), k, l, order='decreasing')])
neg_shift_equiv:
In [19]:
shift_equiv_both = Equals([ExprRange(k, Function(f, Add(k, a)), i, j)], 
                          [ExprRange(i, Function(f, Add(i, b)), k, l)])
shift_equiv_both:
In [20]:
neg_shift_equiv_both = Equals([ExprRange(k, Function(f, Add(k, a)), i, j, order='decreasing')], 
                          [ExprRange(i, Function(f, Add(i, b)), k, l, order='decreasing')])
neg_shift_equiv_both:
In [21]:
%end common

These common expressions may now be imported from the theory package: proveit.core_expr_types.tuples