# Common expressions for the theory of proveit.core_expr_types¶

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 ExprTuple, IndexedVar, Function, ExprRange, var_range
from proveit import (a, b, c, d, e, f, g, i, j, k, l, m, n,
v, w, x, y, z, A, B, C, D, P, Q, R, S, U, V, W,
fa, fx, gx, Pk, alpha, lambda_)
from proveit.numbers import zero, one, two, Add, frac, Neg, subtract
from proveit.logic import Equals, Implies
from proveit.core_expr_types import Len

In [2]:
%begin common

Defining common sub-expressions for theory 'proveit.core_expr_types'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions

In [3]:
a_k = IndexedVar(a, k)

a_k:
In [4]:
a_1_to_i = var_range(a, one, i)

a_1_to_i:
In [5]:
a_1_to_ip1 = var_range(a, one, Add(i, one))

a_1_to_ip1:
In [6]:
a_1_to_j = var_range(a, one, j)

a_1_to_j:
In [7]:
a_1_to_k = var_range(a, one, k)

a_1_to_k:
In [8]:
a_1_to_m = var_range(a, one, m)

a_1_to_m:
In [9]:
a_1_to_n = var_range(a, one, n)

a_1_to_n:
In [10]:
a_i_to_j = var_range(a, i, j)

a_i_to_j:
In [11]:
a_1_to_0 = var_range(a, one, zero)

a_1_to_0:
In [12]:
a_i = IndexedVar(a, i)

a_i:
In [13]:
a_ip1 = IndexedVar(a, Add(i, one))

a_ip1:
In [14]:
alpha_k = IndexedVar(alpha, k)

alpha_k:
In [15]:
bj = IndexedVar(b, j)

bj:
In [16]:
b_i = IndexedVar(b, i)

b_i:
In [17]:
b_1_to_i = var_range(b, one, i)

b_1_to_i:
In [18]:
b_1_to_ip1 = var_range(b, one, Add(i, one))

b_1_to_ip1:
In [19]:
b_1_to_j = var_range(b, one, j)

b_1_to_j:
In [20]:
b_1_to_k = var_range(b, one, k)

b_1_to_k:
In [21]:
b_1_to_m = var_range(b, one, m)

b_1_to_m:
In [22]:
b_1_to_n = var_range(b, one, n)

b_1_to_n:
In [23]:
b_j_to_k = var_range(b, j, k)

b_j_to_k:
In [24]:
b_ip1 = IndexedVar(b, Add(i, one))

b_ip1:
In [25]:
b_kp1 = IndexedVar(b, Add(k, one))

b_kp1:
In [26]:
b_j_to_kp1 = var_range(b, j, Add(k, one))

b_j_to_kp1:
In [27]:
c_i = IndexedVar(c, i)

c_i:
In [28]:
c_1_to_i = var_range(c, one, i)

c_1_to_i:
In [29]:
c_1_to_j = var_range(c, one, j)

c_1_to_j:
In [30]:
c_1_to_k = var_range(c, one, k)

c_1_to_k:
In [31]:
c_1_to_n = var_range(c, one, n)

c_1_to_n:
In [32]:
d_1_to_i = var_range(d, one, i)

d_1_to_i:
In [33]:
d_1_to_j = var_range(d, one, j)

d_1_to_j:
In [34]:
d_1_to_k = var_range(d, one, k)

d_1_to_k:
In [35]:
e_1_to_i = var_range(e, one, i)

e_1_to_i:
In [36]:
e_1_to_j = var_range(e, one, j)

e_1_to_j:
In [37]:
e_1_to_k = var_range(e, one, k)

e_1_to_k:
In [38]:
f_1_to_k = var_range(f, one, k)

f_1_to_k:
In [39]:
f_k = IndexedVar(f, k)

f_k:
In [40]:
i_k = IndexedVar(i, k)

i_k:
In [41]:
j_k = IndexedVar(j, k)

j_k:
In [42]:
n_k = IndexedVar(n, k)

n_k:
In [43]:
i_1_to_m = var_range(i, one, m)

i_1_to_m:
In [44]:
i_1_to_n = var_range(i, one, n)

i_1_to_n:
In [45]:
j_1_to_m = var_range(j, one, m)

j_1_to_m:
In [46]:
j_1_to_n = var_range(j, one, n)

j_1_to_n:
In [47]:
k_1_to_m = var_range(k, one, m)

k_1_to_m:
In [48]:
n_1_to_m = var_range(n, one, m)

n_1_to_m:
In [49]:
v_i = IndexedVar(v, i)

v_i:
In [50]:
v_j = IndexedVar(v, j)

v_j:
In [51]:
w_i = IndexedVar(w, i)

w_i:
In [52]:
w_j = IndexedVar(w, j)

w_j:
In [53]:
V_i = IndexedVar(V, i)

V_i:
In [54]:
V_j = IndexedVar(V, j)

V_j:
In [55]:
v_1_to_m = var_range(v, one, m)

v_1_to_m:
In [56]:
v_1_to_n = var_range(v, one, n)

v_1_to_n:
In [57]:
W_i = IndexedVar(W, i)

W_i:
In [58]:
w_1_to_m = var_range(w, one, m)

w_1_to_m:
In [59]:
w_1_to_n = var_range(w, one, n)

w_1_to_n:
In [60]:
x_i = IndexedVar(x, i)

x_i:
In [61]:
x_j = IndexedVar(x, j)

x_j:
In [62]:
x_k = IndexedVar(x, k)

x_k:
In [63]:
A_k = IndexedVar(A, k)

A_k:
In [64]:
x_1_to_i = var_range(x, one, i)

x_1_to_i:
In [65]:
x_1_to_j = var_range(x, one, j)

x_1_to_j:
In [66]:
x_1_to_k = var_range(x, one, k)

x_1_to_k:
In [67]:
x_1_to_m = var_range(x, one, m)

x_1_to_m:
In [68]:
x_1_to_n = var_range(x, one, n)

x_1_to_n:
In [69]:
x_1_to_np1 = var_range(x, one, Add(n, one))

x_1_to_np1:
In [70]:
y_1_to_j = var_range(y, one, j)

y_1_to_j:
In [71]:
y_1_to_l = var_range(y, one, l)

y_1_to_l:
In [72]:
y_1_to_n = var_range(y, one, n)

y_1_to_n:
In [73]:
y_1_to_m = var_range(y, one, m)

y_1_to_m:
In [74]:
z_1_to_k = var_range(z, one, k)

z_1_to_k:
In [75]:
z_1_to_n = var_range(z, one, n)

z_1_to_n:
In [76]:
range_1_to_i = ExprRange(k, k, one, i)

range_1_to_i:
In [77]:
range_1_to_ip1 = ExprRange(k, k, one, Add(i, one))

range_1_to_ip1:
In [78]:
range_i_to_j = ExprRange(k, k, i, j)

range_i_to_j:
In [79]:
range_i_to_jp1 = ExprRange(k, k, i, Add(j, one))

range_i_to_jp1:
In [80]:
range_1_to_mp1 = ExprRange(k, k, one, Add(m, one))

range_1_to_mp1:
In [81]:
f__a_1_to_i = Function(f, a_1_to_i)

f__a_1_to_i:
In [82]:
g__a_1_to_i = Function(g, a_1_to_i)

g__a_1_to_i:
In [83]:
f__b_1_to_i = Function(f, b_1_to_i)

f__b_1_to_i:
In [84]:
f__b_1_to_j = Function(f, b_1_to_j)

f__b_1_to_j:
In [85]:
g__c_1_to_i = Function(g, c_1_to_i)

g__c_1_to_i:
In [86]:
f__x_1_to_n = Function(f, x_1_to_n)

f__x_1_to_n:
In [87]:
f__y_1_to_n = Function(f, y_1_to_n)

f__y_1_to_n:
In [88]:
g__x_1_to_n = Function(g, x_1_to_n)

g__x_1_to_n:
In [89]:
g__y_1_to_n = Function(g, y_1_to_n)

g__y_1_to_n:
In [90]:
A_i = IndexedVar(A, i)

A_i:
In [91]:
A_1_to_i = var_range(A, one, i)

A_1_to_i:
In [92]:
A_1_to_j = var_range(A, one, j)

A_1_to_j:
In [93]:
A_1_to_l = var_range(A, one, l)

A_1_to_l:
In [94]:
A_i_to_j = var_range(A, i, j)

A_i_to_j:
In [95]:
A_1_to_k = var_range(A, one, k)

A_1_to_k:
In [96]:
A_1_to_l = var_range(A, one, l)

A_1_to_l:
In [97]:
A_1_to_m = var_range(A, one, m)

A_1_to_m:
In [98]:
A_1_to_n = var_range(A, one, n)

A_1_to_n:
In [99]:
B_1_to_i = var_range(B, one, i)

B_1_to_i:
In [100]:
B_1_to_j = var_range(B, one, j)

B_1_to_j:
In [101]:
B_1_to_k = var_range(B, one, k)

B_1_to_k:
In [102]:
B_1_to_m = var_range(B, one, m)

B_1_to_m:
In [103]:
B_1_to_n = var_range(B, one, n)

B_1_to_n:
In [104]:
C_1_to_k = var_range(C, one, k)

C_1_to_k:
In [105]:
C_1_to_l = var_range(C, one, l)

C_1_to_l:
In [106]:
C_1_to_m = var_range(C, one, m)

C_1_to_m:
In [107]:
C_1_to_n = var_range(C, one, n)

C_1_to_n:
In [108]:
D_1_to_m = var_range(D, one, m)

D_1_to_m:
In [109]:
D_1_to_n = var_range(D, one, n)

D_1_to_n:
In [110]:
Q_1_to_m = var_range(Q, one, m)

Q_1_to_m:
In [111]:
R_1_to_n = var_range(R, one, n)

R_1_to_n:
In [112]:
S_1_to_n = var_range(S, one, n)

S_1_to_n:
In [113]:
U_1_to_i = var_range(U, one, i)

U_1_to_i:
In [114]:
U_1_to_m = var_range(U, one, m)

U_1_to_m:
In [115]:
V_1_to_i = var_range(V, one, i)

V_1_to_i:
In [116]:
V_1_to_j = var_range(V, one, j)

V_1_to_j:
In [117]:
V_1_to_n = var_range(V, one, n)

V_1_to_n:
In [118]:
W_1_to_k = var_range(W, one, k)

W_1_to_k:
In [119]:
W_1_to_n = var_range(W, one, n)

W_1_to_n:
In [120]:
lambda_i = IndexedVar(lambda_, i)

lambda_i:
In [121]:
P__x_1_to_n = Function(P, x_1_to_n)

P__x_1_to_n:
In [122]:
P__y_1_to_n = Function(P, y_1_to_n)

P__y_1_to_n:
In [123]:
P__x_1_to_m_y_1_to_n = Function(P, [x_1_to_m, y_1_to_n])

P__x_1_to_m_y_1_to_n:
In [124]:
P__x_1_to_np1 = Function(P, x_1_to_np1)

P__x_1_to_np1:
In [125]:
Q__x_1_to_n = Function(Q, x_1_to_n)

Q__x_1_to_n:
In [126]:
Q__x_1_to_m = Function(Q, x_1_to_m)

Q__x_1_to_m:
In [127]:
Q__y_1_to_n = Function(Q, y_1_to_n)

Q__y_1_to_n:
In [128]:
Q__z_1_to_n = Function(Q, z_1_to_n)

Q__z_1_to_n:
In [129]:
Q__a_1_to_i = Function(Q, a_1_to_i)

Q__a_1_to_i:
In [130]:
Q__b_1_to_i = Function(Q, b_1_to_i)

Q__b_1_to_i:
In [131]:
Q__c_1_to_i = Function(Q, c_1_to_i)

Q__c_1_to_i:
In [132]:
R__x_1_to_n = Function(R, x_1_to_n)

R__x_1_to_n:
In [133]:
R__y_1_to_n = Function(R, y_1_to_n)

R__y_1_to_n:
In [134]:
R__y_1_to_m = Function(R, y_1_to_m)

R__y_1_to_m:
In [135]:
R__x_1_to_m_y_1_to_n = Function(R, [x_1_to_m, y_1_to_n])

R__x_1_to_m_y_1_to_n:
In [136]:
R__z_1_to_n = Function(R, z_1_to_n)

R__z_1_to_n:
In [137]:
fi = Function(f, i)

fi:
In [138]:
fj = Function(f, j)

fj:
In [139]:
fk = Function(f, k)

fk:
In [140]:
f_jp1 = Function(f, Add(j, one))

f_jp1:
In [141]:
f_1_to_n = var_range(f, one, n)

f_1_to_n:
In [142]:
f_m_to_n = var_range(f, m, n)

f_m_to_n:
In [143]:
f_1_to_i = ExprRange(a, fa, one, i)

f_1_to_i:
In [144]:
f_1_to_j = ExprRange(a, fa, one, j)

f_1_to_j:
In [145]:
f_i_to_j = ExprRange(a, fa, i, j)

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

f_i_to_j_dec:
In [147]:
f_i_to_jp1 = ExprRange(a, fa, i, Add(j, one))

f_i_to_jp1:
In [148]:
f_i_to_jm1 = ExprRange(a, fa, i, subtract(j, one))

f_i_to_jm1:
In [149]:
f_i_to_k = ExprRange(a, fa, i, k)

f_i_to_k:
In [150]:
f_i_to_l = ExprRange(a, fa, i, l)

f_i_to_l:
In [151]:
f_j_to_k = ExprRange(a, fa, j, k)

f_j_to_k:
In [152]:
f_k_to_l = ExprRange(a, fa, k, l)

f_k_to_l:
In [153]:
f_ip1_to_j = ExprRange(a, fa, Add(i, one), j)

f_ip1_to_j:
In [154]:
f_jp1_to_k = ExprRange(a, fa, Add(j, one), k)

f_jp1_to_k:
In [155]:
gi = Function(g, i)

gi:
In [156]:
gk = Function(g, k)

gk:
In [157]:
gj = Function(g, j)

gj:
In [158]:
g_i_to_j = ExprRange(x, gx, i, j)

g_i_to_j:
In [159]:
g_k_to_l = ExprRange(x, gx, k, l)

g_k_to_l:
In [160]:
Q__b_1_to_j = Function(Q, b_1_to_j)

Q__b_1_to_j:
In [161]:
Pk_1_to_n = ExprRange(k, Pk, one, n)

Pk_1_to_n:
In [162]:
Pk_a1_to_an = ExprRange(k, Function(P, IndexedVar(a, k)), one, n)

Pk_a1_to_an:
In [163]:
Qk_a1_to_an = ExprRange(k, Function(Q, IndexedVar(a, k)), one, n)

Qk_a1_to_an:
In [164]:
Qk_implies_Pk_a1_to_an = ExprRange(k, Implies( Function(Q, IndexedVar(a, k)), Function(P, IndexedVar(a, k))), one, n)

Qk_implies_Pk_a1_to_an:
In [165]:
xk_over_y_1_to_n = ExprRange(k, frac(IndexedVar(x, k), y), one, n)

xk_over_y_1_to_n:
In [166]:
i_to_j_len = Add(j, Neg(i), one)

i_to_j_len:
In [167]:
j_to_k_len = Add(k, Neg(j), one)

j_to_k_len:
In [168]:
k_to_l_len = Add(l, Neg(k), one)

k_to_l_len:
In [169]:
tuple_len_incr_equiv = Equals(Len([a_1_to_i, b]),
.with_wrap_after_operator()

tuple_len_incr_equiv:
In [170]:
concat_len_equiv = Equals(Len([a_1_to_i, f_j_to_k]),
.with_wrap_after_operator()

concat_len_equiv:
In [171]:
concat_len_simple_equiv = Equals(Len([a_1_to_i, f_1_to_j]),
.with_wrap_after_operator()

concat_len_simple_equiv:
In [172]:
iter_ext_equiv = Equals(ExprTuple(f_i_to_jp1),
ExprTuple(f_i_to_j, f_jp1))\
.with_wrap_after_operator()

iter_ext_equiv:
In [173]:
partition_equiv = Equals(ExprTuple(f_i_to_k),
ExprTuple(f_i_to_j, f_jp1_to_k))\
.with_wrap_after_operator()

partition_equiv:
In [174]:
merge_equiv = Equals(ExprTuple(f_i_to_j, f_k_to_l),
ExprTuple(f_i_to_l))\
.with_wrap_after_operator()

merge_equiv:
In [175]:
partition_front_equiv = Equals(ExprTuple(f_i_to_j),
ExprTuple(fi, f_ip1_to_j))\
.with_wrap_after_operator()

partition_front_equiv:
In [176]:
merge_front_equiv = Equals(ExprTuple(fi, f_j_to_k),
ExprTuple(f_i_to_k))\
.with_wrap_after_operator()

merge_front_equiv:
In [177]:
partition_back_equiv = Equals(ExprTuple(f_i_to_j),
ExprTuple(f_i_to_jm1, fj))\
.with_wrap_after_operator()

partition_back_equiv:
In [178]:
merge_back_equiv = Equals(ExprTuple(f_i_to_j, fk),
ExprTuple(f_i_to_k))\
.with_wrap_after_operator()

merge_back_equiv:
In [179]:
x_0_to_jmi = ExprRange(i, IndexedVar(x, i), zero, subtract(j, i))

x_0_to_jmi:
In [180]:
merge_series_conditions = \
ExprRange(k, Equals(IndexedVar(x, k), Function(f, Add(i, k))),
zero, subtract(j, i))

merge_series_conditions:
In [181]:
merge_series_equiv = Equals(ExprTuple(x_0_to_jmi),
ExprTuple(f_i_to_j))\
.with_wrap_after_operator()

merge_series_equiv:
In [182]:
x_eq_y__1_to_n = ExprRange(k, Equals(IndexedVar(x, k), IndexedVar(y, k)), one, n)

x_eq_y__1_to_n:
In [183]:
%end common

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