# 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)))

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

In [4]:
vec_sum_01.shallow_simplification()


#### VecSum.shifting()¶

In [5]:
vec_sum_02.shifting(one)

In [6]:
vec_sum_02.shifting(two)

In [7]:
vec_sum_02.shifting(Neg(one))

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)

In [9]:
# Then we allow auto_simplify to proceed as usual
vec_sum_03.shifting(Neg(one), assumptions=[InSet(Exp(two, t), Integer)])


#### VecSum.partitioning()¶

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

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


#### VecSum.partitioning_last()¶

In [12]:
vec_sum_02.partitioning_last()

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


#### VecSum.partitioning_first()¶

In [14]:
vec_sum_02.partitioning_first()

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


#### 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)

R3:
In [18]:
C3 = CartExp(Complex, three)

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)]

defaults.assumptions:
In [20]:
Mult(alpha, beta, gamma, delta).factorization(Mult(beta, gamma))

, , ,  ⊢
In [21]:
vec_add_01 = VecAdd(ScalarMult(a, x), ScalarMult(ScalarMult(beta, a), y))

In [22]:
vec_add_02 = VecAdd(TensorProd(x, y), TensorProd(z, y))

In [23]:
vec_add_03 = VecAdd(TensorProd(x, y, z), TensorProd(x, y, w), TensorProd(x, y, v))

In [24]:
vec_add_01_factored = vec_add_01.factorization(a)


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)

supposed_vec_space_membership: ,  ⊢
In [26]:
supposed_vec_space = supposed_vec_space_membership.domain

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)

In [28]:
vec_add_02_factored = vec_add_02.factorization(y, pull='right', field=Real)

In [29]:
vec_add_03


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

In [31]:
# this one will work OK (see next cell)
temp_factored_tensor_prod_01 = TensorProd(TensorProd(x, y), VecAdd(z, w, v))

temp_factored_tensor_prod_01:
In [32]:
InSet(temp_factored_tensor_prod_01, TensorProd(R3, R3, R3)).conclude()

, , , ,  ⊢
In [33]:
temp_factored_tensor_prod_02 = TensorProd(x, VecAdd(TensorProd(y, z), TensorProd(y, w), TensorProd(y, v)))

temp_factored_tensor_prod_02:
In [34]:
deduction_as_vec_space = TensorProd(R3, R3, R3).deduce_as_vec_space()

deduction_as_vec_space:
In [35]:
deduced_field = deduction_as_vec_space.domain.field

deduced_field:
In [36]:
temp_factored_tensor_prod_02.deduce_in_vec_space(field=None)

, , , ,  ⊢
In [37]:
temp_factored_tensor_prod_02.deduce_in_vec_space(field=deduced_field)

, , , ,  ⊢
In [38]:
# interestingly, we also can already do this:
VecSpaces.known_vec_space(x, field=Real)

In [39]:
R3.deduce_as_vec_space()

In [40]:
TensorProd(x, TensorProd(y, z)).simplification()

, ,  ⊢
In [41]:
from proveit.logic import Equals
Equals(TensorProd(R3, TensorProd(R3, R3)), TensorProd(R3, R3, R3)).prove()

In [42]:
vec_add_03_factored_02 = vec_add_03.factorization(x, pull='left', field=Real)

vec_add_03_factored_02: , , , ,  ⊢
In [43]:
TensorProd(x, TensorProd(y, z)).shallow_simplification()

, ,  ⊢
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:
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)!


### Automatically proving conjunctions are equal via permutation¶

In [45]:
defaults.assumptions = [InSet(w, R3), InSet(x, R3), InSet(y, R3), InSet(z, R3)]

defaults.assumptions:
In [46]:
Equals(VecAdd(w, x, y, z), VecAdd(z, y, w, x)).prove()

, , ,  ⊢
In [47]:
Equals(VecAdd(y, z, x, w), VecAdd(x, w, y, z)).prove()

, , ,  ⊢
In [48]:
%end demonstrations