Demonstrations for the theory of proveit.physics.quantum.algebra ¶

import proveit
from proveit import defaults
from proveit import alpha, beta, gamma, delta, j, m, n, b, c, A, B, C, D
from proveit.core_expr_types import b_1_to_j, f__b_1_to_j, Q__b_1_to_j
from proveit.logic import Forall, InSet, CartExp, InClass
from proveit.numbers import Complex, NaturalPos
from proveit.linear_algebra import VecAdd, MatrixSpace
from proveit.linear_algebra.addition import vec_summation_b1toj_fQ
from proveit.physics.quantum import Qmult, Bra, Ket
from proveit.physics.quantum import (
    psi, bra_psi, ket_psi, varphi, bra_varphi, ket_varphi)
from proveit.physics.quantum.algebra import QmultCodomain
%begin demonstrations

Make some assumptions from proving that the Qmult examples are well-formed¶

all_instances_in_C_nxm = Forall(
    b_1_to_j, InSet(f__b_1_to_j, MatrixSpace(Complex, n, m)),
           condition=Q__b_1_to_j)

defaults.assumptions = [
    InSet(alpha, Complex), InSet(beta, Complex),
    InSet(gamma, Complex), InSet(delta, Complex),
    InSet(j, NaturalPos),
    InSet(m, NaturalPos), InSet(n, NaturalPos),
    InSet(ket_psi, CartExp(Complex, m)),
    InSet(A, MatrixSpace(Complex, n, m)),
    InSet(B, MatrixSpace(Complex, n, m)),
    InSet(C, MatrixSpace(Complex, n, m)),
    InSet(D, MatrixSpace(Complex, m, n)),
    InSet(ket_varphi, CartExp(Complex, n)),
    all_instances_in_C_nxm,
    Q__b_1_to_j.basic_replaced({b:c})
    ]

all_instances_in_C_nxm.instantiate({b:c})

Build some Qmult examples, well-formed and not¶

Well-formed:

qmult1 = Qmult(alpha, A, beta, ket_psi, gamma)

qmult2 = Qmult(bra_varphi, alpha, A, beta, 
               ket_psi, gamma, bra_varphi, delta)

qmult3 = Qmult(bra_varphi, alpha, VecAdd(A, B, C), beta, 
               ket_psi, gamma, bra_varphi, delta)

qmult4 = Qmult(bra_varphi, alpha, vec_summation_b1toj_fQ, beta, 
               ket_psi, gamma, bra_varphi, delta).basic_replaced(
    {b:c}, allow_relabeling=True)

qmult5 = Qmult(alpha, A, beta, VecAdd(ket_psi, Qmult(D, ket_varphi)))

qmult6 = Qmult(alpha, D, beta, VecAdd(Qmult(B, ket_psi), ket_varphi))

Not well-formed (matrix-vector incompatible):

qmult_bad = Qmult(alpha, D, beta, ket_psi, 
                  gamma, Bra(varphi), delta)

Let's disable some simplification directives during initial testing¶

print(Qmult.simplification_directive_keys())

['ungroup', 'factor_scalars', 'use_scalar_mult']

Qmult.change_simplification_directives(
    ungroup=False, factor_scalars=False, use_scalar_mult=False)

Proving membership in the QmultCodomain class¶

InClass(alpha, QmultCodomain).prove()

InClass(ket_psi, QmultCodomain).prove()

InClass(Bra(varphi), QmultCodomain).prove()

InClass(Qmult(alpha), QmultCodomain).prove()

InClass(Qmult(ket_psi), QmultCodomain).prove()

InClass(Qmult(A), QmultCodomain).prove()

InClass(Qmult(bra_varphi), QmultCodomain).prove()

InClass(Qmult(ket_varphi, bra_psi), QmultCodomain).prove()

InClass(Qmult(D, ket_varphi), QmultCodomain).prove()

InClass(Qmult(bra_psi, ket_psi), QmultCodomain).prove()

InClass(Qmult(alpha, A), QmultCodomain).prove()

InClass(Qmult(bra_varphi, ket_varphi, gamma), QmultCodomain).prove()

qmult1

InClass(qmult1, QmultCodomain).prove()

qmult5

InClass(qmult5, QmultCodomain).prove()

Association/dissociation of a Qmult¶

help(Qmult.association)

Help on function association in module proveit.physics.quantum.algebra.qmult:

association(self, start_idx, length, **defaults_config)
    Given a valid Qmult operation (valid sequence of bras, kets,
    and/or quantum operations), deduce that this expression is equal 
    to a form in which operands in the
    range [start_idx, start_idx+length) are grouped together.
    For example, (A B ... Y Z) = (A B ... (L ... M) ... Y Z).
    
    Keyword arguments are accepted for temporarily changing any
    of the attributes of proveit.defaults.
    
    'associated' returns the right-hand side of 'association'.
    'associate', called on an InnerExpr of a Judgment,
    substitutes the right-hand side of 'association' for
    the inner expression.

help(Qmult.disassociation)

Help on function disassociation in module proveit.physics.quantum.algebra.qmult:

disassociation(self, idx, **defaults_config)
    Given a valid Qmult operation (valid sequence of bras, kets,
    and/or quantum operations), deduce that this expression is equal 
    to a form in which the operand
    at index idx is no longer grouped together.
    For example, (A B ... (L ... M) ... Y Z) = (A B ... Y Z).
    
    Keyword arguments are accepted for temporarily changing any
    of the attributes of proveit.defaults.
    
    'disassociated' returns the right-hand side of 'disassociation'.
    'disassociate', called on an InnerExpr of a Judgment,
    substitutes the right-hand side of 'disassociation' for
    the inner expression.

qmult1

qmult1_association = qmult1.association(1, 2)

qmult1_associated = qmult1_association.rhs

qmult1_associated.disassociation(1)

qmult2

qmult2.association(5, 3)

If the Qmult is not well-formed, we expect an error:

qmult_bad

from proveit import UnsatisfiedPrerequisites try: qmult_bad.association(2, 3) assert False # expecting an error except UnsatisfiedPrerequisites as e: print("Expected error: %s"%e)

Factor out scalar factors¶

Scalars are pulled to the front automatically with the default simplification directives. This directive is currently disabled, however. Here, we demonstrate doing this manually.

help(Qmult.factorization_of_scalars)

Help on function factorization_of_scalars in module proveit.physics.quantum.algebra.qmult:

factorization_of_scalars(self, **defaults_config)
    Prove equality with a Qmult in which the complex
    numbers are pulled to the front andassociated together via Mult.
    For example,
        (a A b B c C d D e) = ((a*b*c*d*e) A B C D)
    where a, b, c, d, and e are complex numbers, '*' denotes
    number multiplication, and spaces, here, denote the Qmult
    operation.
    
    Also see scalar_mult_factorization.
    
    Keyword arguments are accepted for temporarily changing any
    of the attributes of proveit.defaults.
    
    'scalars_factored' returns the right-hand side of 'factorization_of_scalars'.
    'factor_scalars', called on an InnerExpr of a Judgment,
    substitutes the right-hand side of 'factorization_of_scalars' for
    the inner expression.

qmult1.factorization_of_scalars()

qmult2

qmult2.factorization_of_scalars()

Distribution over summations¶

help(Qmult.distribution)

Help on function distribution in module proveit.physics.quantum.algebra.qmult:

distribution(self, idx, *, field=None, **defaults_config)
    Given a Qmult operand at the (0-based) index location
    'idx' that is a vector sum or summation, prove the distribution 
    over that Qmult factor and return an equality to the original
    Qmult. For example, we could take the Qmult
        qmult = Qmult(A, B+C, D)
    and call qmult.distribution(1) to obtain:
        |- Qmult(A, B+C, D) =
           Qmult(A, B, D) + Qmult(A, C. D)
    
    Keyword arguments are accepted for temporarily changing any
    of the attributes of proveit.defaults.
    
    'distributed' returns the right-hand side of 'distribution'.
    'distribute', called on an InnerExpr of a Judgment,
    substitutes the right-hand side of 'distribution' for
    the inner expression.

qmult3

QmultCodomain.membership_object(qmult3).expr

InClass(qmult3, QmultCodomain).prove()

qmult3.distribution(2)

qmult4

qmult4.distribution(2)

qmult5

qmult5.distribution(3)

qmult6

qmult6.distribution(3)

Simplification¶

help(Qmult.simplification)

Help on function simplification in module proveit._core_.expression.operation.operation:

simplification(self, **defaults_config)
    If possible, return a Judgment of this expression equal to a
    simplified form (according to strategies specified in 
    proveit.defaults). 
    
    This Operation.simplification version tries calling
    simplifies the operands and then calls 'shallow_simplification'.
    
    Keyword arguments are accepted for temporarily changing any
    of the attributes of proveit.defaults.
    
    'simplified' returns the right-hand side of 'simplification'.
    'simplify', called on an InnerExpr of a Judgment,
    substitutes the right-hand side of 'simplification' for
    the inner expression.

help(Qmult.shallow_simplification)

Help on function shallow_simplification in module proveit.physics.quantum.algebra.qmult:

shallow_simplification(self, *, must_evaluate=False, **defaults_config)
    Returns a proven simplification equation for this Qmult
    expression assuming the operands have been simplified.
    
    Currently deals only with:
    (1) simplify unary case
    (2) Ungrouping nested tensor products.
    (3) Factoring out scalars.
    
    Keyword arguments are accepted for temporarily changing any
    of the attributes of proveit.defaults.
    
    'shallow_simplified' returns the right-hand side of 'shallow_simplification'.
    'shallow_simplify', called on an InnerExpr of a Judgment,
    substitutes the right-hand side of 'shallow_simplification' for
    the inner expression.

Qmult.change_simplification_directives(ungroup=True, 
                                       factor_scalars=True,
                                       use_scalar_mult=True)

qmult1.simplification()

qmult1_associated

qmult1_associated.simplification()

qmult4

qmult4.simplification()

%end demonstrations

Demonstrations for the theory of proveit.physics.quantum.algebra¶