Demonstrations for the theory of proveit.linear_algebra.addition ¶

import proveit
from proveit import k, t, v, vi, vk, N, 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)
%begin demonstrations

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)), vk), domain=Interval(zero, N)),
    VecSum(k, v, domain=Interval(one, eight)))

`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.

vec_sum_01

vec_sum_01.shallow_simplification()

`VecSum.shifting()`¶

vec_sum_02.shifting(one)

vec_sum_02.shifting(two)

vec_sum_02.shifting(Neg(one))

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

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

`VecSum.partitioning()`¶

vec_sum_02.partitioning(split_index=num(5), side='after')

vec_sum_02.partitioning(split_index=num(5), side='before')

`VecSum.partitioning_last()`¶

vec_sum_02.partitioning_last()

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

`VecSum.partitioning_first()`¶

vec_sum_02.partitioning_first()

from proveit.logic import Forall, CartExp
from proveit.numbers import Complex, Natural, NaturalPos
from proveit import defaults, n
Cn = CartExp(Complex, n)
defaults.assumptions = [InSet(n, NaturalPos), InSet(N, NaturalPos), Forall(k, InSet(vk, Cn), domain=Natural)]

defaults.assumptions + vec_sum_04.domain_conditions()

defaults.assumptions[-1].instantiate({k:zero}, assumptions=defaults.assumptions)

vec_sum_04.partitioning_first()

Testing re: `VecAdd.factorization()`¶

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.

R3 = CartExp(Real, three)

C3 = CartExp(Complex, three)

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

Mult(alpha, beta, gamma, delta).factorization(Mult(beta, gamma))

vec_add_01 = VecAdd(ScalarMult(a, x), ScalarMult(Mult(beta, a), y))

vec_add_02 = VecAdd(TensorProd(x, y), TensorProd(z, y))

vec_add_03 = VecAdd(TensorProd(x, y, z), TensorProd(x, y, w), TensorProd(x, y, v))

vec_add_01_factored = vec_add_01.factorization(a, pull='left')

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

supposed_vec_space_membership = TensorProd(x, y).deduce_in_vec_space(field=Real)

supposed_vec_space = supposed_vec_space_membership.domain

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

vec_add_02_factored = vec_add_02.factorization(y, pull='right', field=Real)

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

# reminder of assumptions:
defaults.assumptions

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

InSet(temp_factored_tensor_prod_01, TensorProd(R3, R3, R3)).conclude()

temp_factored_tensor_prod_02 = TensorProd(x, VecAdd(TensorProd(y, z), TensorProd(y, w), TensorProd(y, v)))

deduction_as_vec_space = TensorProd(R3, R3, R3).deduce_as_vec_space()

deduced_field = deduction_as_vec_space.domain.field

temp_factored_tensor_prod_02.deduce_in_vec_space(field=None)

temp_factored_tensor_prod_02.deduce_in_vec_space(field=deduced_field)

# interestingly, we also can already do this:
VecSpaces.known_vec_space(x, field=Real)

R3.deduce_as_vec_space()

TensorProd(x, TensorProd(y, z)).simplification()

from proveit.logic import Equals
Equals(TensorProd(R3, TensorProd(R3, R3)), TensorProd(R3, R3, R3)).prove()

vec_add_03_factored_02 = vec_add_03.factorization(x, pull='left', field=Real)

TensorProd(x, TensorProd(y, z)).shallow_simplification()

# 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: factorization() missing 1 required keyword-only argument: 'pull'

Automatically proving conjunctions are equal via permutation¶

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

Equals(VecAdd(w, x, y, z), VecAdd(z, y, w, x)).prove()

Equals(VecAdd(y, z, x, w), VecAdd(x, w, y, z)).prove()

%end demonstrations

Demonstrations for the theory of proveit.linear_algebra.addition¶

VecSum.shallow_simplification()¶

VecSum.shifting()¶

VecSum.partitioning()¶

VecSum.partitioning_last()¶

VecSum.partitioning_first()¶

Testing re: VecAdd.factorization()¶