logo

Demonstrations for the theory of proveit.core_expr_types.expr_arrays

In [1]:
import proveit
from proveit import defaults
from proveit import ExprRange, ExprTuple, IndexedVar, var_range, ExprArray, VertExprArray
from proveit import i, j, k, m, n, p, q, A, B, C, D, E, F, G, H, I, X
from proveit.logic import InSet
from proveit.numbers import one, Natural, NaturalPos, subtract
%begin demonstrations
In [2]:
# defaults.assumptions = [InSet(i, Natural), InSet(j, Natural), InSet(k, Natural),
#                         InSet(subtract(j, i), Natural), 
#                         InSet(n, Natural), InSet(m, NaturalPos)]
In [3]:
A_i_to_j = var_range(A, i, j)
A_i_to_j:
In [4]:
B_i_to_j = var_range(B, i, j)
B_i_to_j:
In [5]:
C_i_to_j = var_range(C, i, j)
C_i_to_j:
In [6]:
D_i_to_j = var_range(D, i, j)
D_i_to_j:
In [7]:
Aij = IndexedVar(A,(i,j))
Aij:
In [8]:
Bij = IndexedVar(B,(i,j))
Bij:
In [9]:
Cij = IndexedVar(C,(i,j))
Cij:
In [10]:
Dij = IndexedVar(D,(i,j))
Dij:
In [11]:
Eij = IndexedVar(E, (i,j))
Eij:
In [12]:
Fij = IndexedVar(F, (i,j))
Fij:
In [13]:
ExprRange(j, Aij, one, n).with_styles(parameterization='explicit').body
In [14]:
ExprRange(i, ExprTuple(ExprRange(j, Aij, one, n), ExprRange(j, Bij, one, k)),one,m)
In [15]:
ExprTuple(ExprRange(i, ExprTuple(ExprRange(j, Aij, one, n), ExprRange(j, Bij, one, k)),
                    one,m))
In [16]:
ExprArray(ExprTuple(A, B), ExprTuple(C, D))
In [17]:
ExprArray(ExprTuple(A, B, C, A, B, C, A), 
          ExprTuple(D, E, F, D, E, F, D), 
          ExprTuple(G, H, I, G, H, I, G))
In [18]:
ExprArray(ExprTuple(A_i_to_j, A, B, C), 
          ExprTuple(C_i_to_j, D, E, F))
In [19]:
ExprArray(ExprTuple(A_i_to_j.with_front_expansion(3), A, B, C), 
          ExprTuple(C_i_to_j.with_front_expansion(3), D, E, F))
In [20]:
# Unable to format this in an array form.
ExprArray(ExprTuple(A_i_to_j.with_front_expansion(2), A, B, C), 
          ExprTuple(C_i_to_j.with_front_expansion(3), D, E, F))
In [21]:
ExprArray(ExprTuple(A_i_to_j.with_back_expansion(3), A, B, C), 
          ExprTuple(C_i_to_j.with_back_expansion(3), D, E, F))
In [22]:
# Unable to format this in an array form.
ExprArray(ExprTuple(A_i_to_j.with_front_expansion(3), A, B, C), 
          ExprTuple(C_i_to_j.with_back_expansion(3), D, E, F))
In [23]:
ExprArray(ExprTuple(A_i_to_j.with_explicit_parameterization(), A, B, C), 
          ExprTuple(C_i_to_j, D, E, F))
In [24]:
ExprArray(ExprTuple(A_i_to_j, B_i_to_j.with_explicit_parameterization()), 
          ExprTuple(C_i_to_j.with_explicit_parameterization(), D_i_to_j))
In [25]:
ExprArray(ExprRange(i, ExprTuple(Aij, Bij, Cij, Dij),one,m))
In [26]:
ExprArray(ExprRange(i, ExprTuple(Aij, Bij, Cij, Dij),one,m)
          .with_explicit_parameterization())
In [27]:
ExprArray(ExprRange(i, ExprTuple(Aij, Bij, Cij, Dij),one,m)
          .with_explicit_parameterization())
In [28]:
ExprArray(ExprRange(i, ExprTuple(Aij, Bij, Cij, Dij),one,m)
          .with_explicit_parameterization(),
          ExprTuple(D, C, B, A))
In [29]:
ExprArray(ExprRange(i, ExprTuple(Aij, Bij, Cij, Dij),one,m)
          .with_explicit_parameterization(),
          X, [D, C, B, A])
In [30]:
VertExprArray(ExprRange(i, ExprTuple(Aij, Bij, Cij, Dij),one,m)
              .with_explicit_parameterization(),
              X, [D, C, B, A])
In [31]:
ExprArray(ExprTuple(A,B,C,D),
          ExprRange(i, ExprTuple(Aij, Bij, Cij, Dij),one,m), 
          ExprTuple(A,B,C,D))
In [32]:
ExprArray(ExprRange(i, ExprTuple(ExprRange(j, Aij, one, n), 
                                 ExprRange(j, Bij, one, k)),one,m))
In [33]:
ExprArray(ExprRange(i, ExprTuple(ExprRange(j, Aij, one, n), 
                                 ExprRange(j, Bij, one, k)),one,m)
          .with_explicit_parameterization())
In [34]:
ExprArray(ExprRange(i, ExprTuple(ExprRange(j, Aij, one, n)
                                 .with_explicit_parameterization(), 
                                 ExprRange(j, Bij, one, k)),one,m))
In [35]:
ExprArray(ExprRange(i, ExprTuple(ExprRange(j, Aij, one, n)
                                 .with_explicit_parameterization(), 
                                 ExprRange(j, Bij, one, k)),one,m)
          .with_explicit_parameterization())
In [36]:
ExprArray(ExprRange(i, ExprTuple(ExprRange(j, Aij, one, n)
                                 .with_explicit_parameterization(), 
                                 ExprRange(j, Bij, one, k)),one,m)
          .with_explicit_parameterization())
In [37]:
VertExprArray(ExprRange(i, ExprTuple(ExprRange(j, Aij, one, n)
                                 .with_explicit_parameterization(), 
                                 ExprRange(j, Bij, one, k)),one,m)
          .with_explicit_parameterization())
In [38]:
ExprArray(ExprRange(i, ExprTuple(A, A, ExprRange(j, Aij, one, n), A, A), one, m))
In [39]:
ExprArray(ExprRange(i, ExprRange(j, Aij, 
                                 one, n), 
                    one, m))
In [40]:
ExprArray(ExprRange(i, ExprRange(j, ExprTuple(Aij, Bij), 
                                 one, n), 
                    one, m))
In [41]:
ExprArray(ExprRange(i, ExprTuple(A, A, ExprRange(j, Aij, one, n), A, A), one, m))
In [42]:
ExprArray(ExprRange(i, ExprTuple(A, A, ExprRange(j, Aij, one, n).with_explicit_parameterization(), A, A), one, m)
          .with_explicit_parameterization())
In [43]:
ExprArray(ExprRange(i, ExprTuple(A, A, ExprRange(j, Aij, one, n), A, A), one, m)
          .with_explicit_parameterization())
In [44]:
Apj = IndexedVar(A,(p,j))
Apj:
In [45]:
Bpj = IndexedVar(B,(p,j))
Bpj:
In [46]:
Cjk = IndexedVar(C,(j,k))
Cjk:
In [47]:
Dki = IndexedVar(D,(k,i))
Dki:
In [48]:
C_i_to_k = var_range(C, i, k)
C_i_to_k:
In [49]:
D_j_to_i = var_range(B, j, i)
D_j_to_i:
In [50]:
# Unable to format this in an array form.
ExprArray(ExprTuple(A, B, C, A, B, A), 
          ExprTuple(D, E, F, D, E, F, D), 
          ExprTuple(G, H, I, G, H, I, G))
In [51]:
ExprArray(ExprTuple(B_i_to_j, A, B, C), 
          ExprTuple(D, E, F, D_i_to_j))
In [52]:
ExprArray(ExprTuple(A, B, C, B_i_to_j), 
          ExprTuple(D_i_to_j, D, E, F))
In [53]:
ExprArray(ExprTuple(C_i_to_j, D_j_to_i), 
          ExprTuple(A_i_to_j, B_i_to_j))
In [54]:
ExprArray(ExprRange(i, ExprTuple(Apj, Bij, Cjk, Dki),one,m))
In [55]:
ExprArray(ExprTuple(ExprRange(i, ExprRange(j, Aij, one, n), one, m)),
          ExprTuple(ExprRange(i, ExprRange(j, Bij, one, n), one, m)))
In [56]:
ExprArray(ExprRange(i, IndexedVar(A, i), one, n))
In [57]:
ExprArray(ExprRange(i, ExprTuple(IndexedVar(A, i), IndexedVar(B, i)), one, n))#.get_format_cell_entries()
In [58]:
ExprArray(ExprRange(i, IndexedVar(A, i), one, n)).get_format_cell_entries()

[(A_{1}, 0), (A_{2}, 1), (A_{1}, A_{2}, ..., A_{n}, 'implicit'), (A_{n}, -1)]
In [59]:
ExprArray(ExprRange(i, ExprRange(j, Aij, one, n), one, m))
In [60]:
VertExprArray(ExprRange(i, ExprRange(j, Aij, one, n), one, m))
In [61]:
VertExprArray(ExprRange(i, ExprRange(j, Aij, one, n), one, m).with_explicit_parameterization())
In [62]:
ExprTuple(ExprRange(i, ExprRange(j, Aij, one, n), one, m).with_explicit_parameterization())
In [63]:
ExprArray(ExprRange(i, ExprRange(j, ExprTuple(Aij, Bij), one, n), one, m))
In [64]:
ExprArray(ExprRange(i, ExprRange(j, ExprTuple(Aij, Bij), one, n), one, m)
          .with_explicit_parameterization())
In [65]:
VertExprArray(ExprRange(i, ExprRange(j, ExprTuple(Aij, Bij), one, n), one, m).with_explicit_parameterization())
In [66]:
VertExprArray(ExprRange(i, ExprRange(j, ExprTuple(Aij, Bij), one, n).with_explicit_parameterization(), 
                        one, m).with_explicit_parameterization())
In [67]:
VertExprArray(ExprRange(i, ExprRange(j, Aij, one, n), one, m))
In [68]:
ExprArray(ExprRange(i, ExprRange(j, Aij, one, n), one, m))
In [69]:
# Unable to format this in an array form.
ExprArray(ExprTuple(A,B,C,D),
          ExprRange(i, ExprTuple(ExprTuple(Apj, Bij), 
                                 ExprTuple(Cjk, Dki)),one,m), 
          ExprTuple(A,B,C,D))
In [70]:
ExprArray(E, F, ExprTuple(A,B), C, D)
In [71]:
%end demonstrations