logo

Demonstrations for the theory of proveit.linear_algebra.addition

In [1]:
import proveit
from proveit import k, t, v, vi, vk, Variable
from proveit.logic import InSet
from proveit.linear_algebra import ScalarMult, VecAdd, VecSpaces, VecSum
from proveit.numbers import (zero, one, two, eight, i, e, pi, Exp, Integer,
                             Interval, Less, Mult, Neg, num)
from proveit.physics.quantum import Ket
%begin demonstrations
In [2]:
i_var = Variable('i') # to distinguish from imaginary number i
vec_sum_01, vec_sum_02, vec_sum_03, vec_sum_04, vec_sum_05 = (
    VecSum(i_var, vi, domain=Interval(two, two)),
    VecSum(i_var, vi, domain=Interval(one, eight)),
    VecSum(k, vk, domain=Interval(zero, Exp(two, t))),
    VecSum(k, ScalarMult(Exp(e, Mult(two, pi, i, k)), Ket(k)), domain=Interval(zero, Exp(two, t))),
    VecSum(k, v, domain=Interval(one, eight)))
Out[2]:
vec_sum_01:
vec_sum_02:
vec_sum_03:
vec_sum_04:
vec_sum_05:

VecSum.shallow_simplification()

VecSum.shallow_simplification() will take a single-item vector summation and return the equality of that sum with the vector evaluated at the single index value.

In [3]:
vec_sum_01
Out[3]:
In [4]:
vec_sum_01.shallow_simplification()
Out[4]:

VecSum.shifting()

In [5]:
vec_sum_02.shifting(one)
Out[5]:
In [6]:
vec_sum_02.shifting(two)
Out[6]:
In [7]:
vec_sum_02.shifting(Neg(one))
Out[7]:
In [8]:
# Here we temporarily set auto_simplify=False to see the underlying shift
vec_sum_03.shifting(Neg(one), assumptions=[InSet(Exp(two, t), Integer)], auto_simplify=False)
Out[8]:
In [9]:
# Then we allow auto_simplify to proceed as usual
vec_sum_03.shifting(Neg(one), assumptions=[InSet(Exp(two, t), Integer)])
Out[9]:

VecSum.partitioning()

In [10]:
vec_sum_02.partitioning(split_index=num(5), side='after')
Out[10]:
In [11]:
vec_sum_02.partitioning(split_index=num(5), side='before')
Out[11]:

VecSum.partitioning_last()

In [12]:
vec_sum_02.partitioning_last()
Out[12]:
In [13]:
vec_sum_03.partitioning_last(
        assumptions=[InSet(Exp(two, t), Integer), Less(zero, Exp(two, t))])
Out[13]:

VecSum.partitioning_first()

In [14]:
vec_sum_02.partitioning_first()
Out[14]:
In [15]:
vec_sum_04.partitioning_first(
        assumptions=[InSet(Exp(two, t), Integer), Less(zero, Exp(two, t))])
Out[15]:

Testing re: VecAdd.factorization()

In [16]:
from proveit import defaults
from proveit import a, b, c, i, u, v, w, x, y, z, alpha, beta, gamma, delta, fi
from proveit.linear_algebra import TensorProd, VecZero
from proveit.logic import CartExp, Forall, InSet, NotEquals
from proveit.numbers import three, Complex, Natural, Real

Let's set some defaults for convienience in our testing below.

In [17]:
R3 = CartExp(Real, three)
Out[17]:
R3:
In [18]:
C3 = CartExp(Complex, three)
Out[18]:
C3:
In [19]:
defaults.assumptions = [
    InSet(u, R3), InSet(v, R3), InSet(w, R3), 
    InSet(x, R3), InSet(y, R3), InSet(z, R3),
    NotEquals(x, VecZero(R3)), NotEquals(z, VecZero(R3)),
    InSet(a, Real), InSet(alpha, Complex), InSet(beta, Real),
    InSet(gamma, Real), InSet (delta, Real),
    Forall(i, InSet(fi, R3), domain=Natural)]
Out[19]:
defaults.assumptions:
In [20]:
Mult(alpha, beta, gamma, delta).factorization(Mult(beta, gamma))
Out[20]:
, , ,  ⊢  
In [21]:
vec_add_01 = VecAdd(ScalarMult(a, x), ScalarMult(ScalarMult(beta, a), y))
Out[21]:
vec_add_01:
In [22]:
vec_add_02 = VecAdd(TensorProd(x, y), TensorProd(z, y))
Out[22]:
vec_add_02:
In [23]:
vec_add_03 = VecAdd(TensorProd(x, y, z), TensorProd(x, y, w), TensorProd(x, y, v))
Out[23]:
vec_add_03:
In [24]:
vec_add_01_factored = vec_add_01.factorization(a)
Out[24]:
vec_add_01_factored: , , ,  ⊢  

Testing Begin Here! (Needs to be cleaned up and reorganized later.)

In [25]:
supposed_vec_space_membership = TensorProd(x, y).deduce_in_vec_space(field=Real)
Out[25]:
supposed_vec_space_membership: ,  ⊢  
In [26]:
supposed_vec_space = supposed_vec_space_membership.domain
Out[26]:
supposed_vec_space:
In [27]:
# perhaps this will help the experiment further below?
from proveit.linear_algebra.vector_spaces import containing_vec_space
containing_vec_space(TensorProd(y, z), field=Real)
Out[27]:
In [28]:
vec_add_02_factored = vec_add_02.factorization(y, pull='right', field=Real)
Out[28]:
vec_add_02_factored: , ,  ⊢  
In [29]:
vec_add_03
Out[29]:

Investigating error when Prove-It is trying to perform the following:

return tensor_prod_is_in_tensor_prod_space.instantiate( {a: _a_sub, i: _i_sub, K: _K_sub, V: vec_spaces})

in tensor_prod_membership.py for the case of $x\otimes((y\otimes z) + (y\otimes w) + (y\otimes v))$

In [30]:
# reminder of assumptions:
defaults.assumptions
Out[30]:
In [31]:
# this one will work OK (see next cell)
temp_factored_tensor_prod_01 = TensorProd(TensorProd(x, y), VecAdd(z, w, v))
Out[31]:
temp_factored_tensor_prod_01:
In [32]:
InSet(temp_factored_tensor_prod_01, TensorProd(R3, R3, R3)).conclude()
Out[32]:
, , , ,  ⊢  
In [33]:
temp_factored_tensor_prod_02 = TensorProd(x, VecAdd(TensorProd(y, z), TensorProd(y, w), TensorProd(y, v)))
Out[33]:
temp_factored_tensor_prod_02:
In [34]:
deduction_as_vec_space = TensorProd(R3, R3, R3).deduce_as_vec_space()
Out[34]:
deduction_as_vec_space:  ⊢  
In [35]:
deduced_field = deduction_as_vec_space.domain.field
Out[35]:
deduced_field:
In [36]:
temp_factored_tensor_prod_02.deduce_in_vec_space(field=None)
Out[36]:
, , , ,  ⊢  
In [37]:
temp_factored_tensor_prod_02.deduce_in_vec_space(field=deduced_field)
Out[37]:
, , , ,  ⊢  
In [38]:
# interestingly, we also can already do this:
VecSpaces.known_vec_space(x, field=Real)
Out[38]:
In [39]:
R3.deduce_as_vec_space()
Out[39]:
In [40]:
TensorProd(x, TensorProd(y, z)).simplification()
Out[40]:
, ,  ⊢  
In [41]:
from proveit.logic import Equals
Equals(TensorProd(R3, TensorProd(R3, R3)), TensorProd(R3, R3, R3)).prove()
Out[41]:
In [42]:
vec_add_03_factored_02 = vec_add_03.factorization(x, pull='left', field=Real)
Out[42]:
vec_add_03_factored_02: , , , ,  ⊢  
In [43]:
TensorProd(x, TensorProd(y, z)).shallow_simplification()
Out[43]:
, ,  ⊢  
In [44]:
# This will not yet work, since the factor is a vector and
# appears in the scaled portion of each ScalarMult but is not a TensorProd factor
try:
    VecAdd(ScalarMult(two, x), ScalarMult(three, x)).factorization(x)
except Exception as the_exception:
    print("Exception: {}".format(the_exception))
Exception: Factor, x, is not present in the term at index 0 of (2 * x) + (3 * x)!

Testing Ends Here!

In [45]:
%end demonstrations