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