logo

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

In [1]:
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

In [2]:
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)
Out[2]:
all_instances_in_C_nxm:
In [3]:
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})
    ]
Out[3]:
defaults.assumptions:
In [4]:
all_instances_in_C_nxm.instantiate({b:c})
Out[4]:

Build some Qmult examples, well-formed and not

Well-formed:

In [5]:
qmult1 = Qmult(alpha, A, beta, ket_psi, gamma)
Out[5]:
qmult1:
In [6]:
qmult2 = Qmult(bra_varphi, alpha, A, beta, 
               ket_psi, gamma, bra_varphi, delta)
Out[6]:
qmult2:
In [7]:
qmult3 = Qmult(bra_varphi, alpha, VecAdd(A, B, C), beta, 
               ket_psi, gamma, bra_varphi, delta)
Out[7]:
qmult3:
In [8]:
qmult4 = Qmult(bra_varphi, alpha, vec_summation_b1toj_fQ, beta, 
               ket_psi, gamma, bra_varphi, delta).basic_replaced(
    {b:c}, allow_relabeling=True)
Out[8]:
qmult4:
In [9]:
qmult5 = Qmult(alpha, A, beta, VecAdd(ket_psi, Qmult(D, ket_varphi)))
Out[9]:
qmult5:
In [10]:
qmult6 = Qmult(alpha, D, beta, VecAdd(Qmult(B, ket_psi), ket_varphi))
Out[10]:
qmult6:

Not well-formed (matrix-vector incompatible):

In [11]:
qmult_bad = Qmult(alpha, D, beta, ket_psi, 
                  gamma, Bra(varphi), delta)
Out[11]:
qmult_bad:

Let's disable some simplification directives during initial testing

In [12]:
print(Qmult.simplification_directive_keys())
['ungroup', 'factor_scalars', 'use_scalar_mult']
In [13]:
Qmult.change_simplification_directives(
    ungroup=False, factor_scalars=False, use_scalar_mult=False)

Proving membership in the QmultCodomain class

In [14]:
InClass(alpha, QmultCodomain).prove()
Out[14]:
In [15]:
InClass(ket_psi, QmultCodomain).prove()
Out[15]:
In [16]:
InClass(Bra(varphi), QmultCodomain).prove()
Out[16]:
In [17]:
InClass(Qmult(alpha), QmultCodomain).prove()
Out[17]:
In [18]:
InClass(Qmult(ket_psi), QmultCodomain).prove()
Out[18]:
In [19]:
InClass(Qmult(A), QmultCodomain).prove()
Out[19]:
, ,  ⊢  
In [20]:
InClass(Qmult(bra_varphi), QmultCodomain).prove()
Out[20]:
In [21]:
InClass(Qmult(ket_varphi, bra_psi), QmultCodomain).prove()
Out[21]:
In [22]:
InClass(Qmult(D, ket_varphi), QmultCodomain).prove()
Out[22]:
, , ,  ⊢  
In [23]:
InClass(Qmult(bra_psi, ket_psi), QmultCodomain).prove()
Out[23]:
In [24]:
InClass(Qmult(alpha, A), QmultCodomain).prove()
Out[24]:
, , ,  ⊢  
In [25]:
InClass(Qmult(bra_varphi, ket_varphi, gamma), QmultCodomain).prove()
Out[25]:
, ,  ⊢  
In [26]:
qmult1
Out[26]:
In [27]:
InClass(qmult1, QmultCodomain).prove()
Out[27]:
, , , , , ,  ⊢  
In [28]:
qmult5
Out[28]:
In [29]:
InClass(qmult5, QmultCodomain).prove()
Out[29]:
, , , , , , ,  ⊢  

Association/dissociation of a Qmult

In [30]:
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.

In [31]:
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.

In [32]:
qmult1
Out[32]:
In [33]:
qmult1_association = qmult1.association(1, 2)
Out[33]:
qmult1_association: , , , , , ,  ⊢  
In [34]:
qmult1_associated = qmult1_association.rhs
Out[34]:
qmult1_associated:
In [35]:
qmult1_associated.disassociation(1)
Out[35]:
, , , , , ,  ⊢  
In [36]:
qmult2
Out[36]:
In [37]:
qmult2.association(5, 3)
Out[37]:
, , , , , , , ,  ⊢  

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

In [38]:
qmult_bad
Out[38]:

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.

In [39]:
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.

In [40]:
qmult1.factorization_of_scalars()
Out[40]:
, , , , , ,  ⊢  
In [41]:
qmult2
Out[41]:
In [42]:
qmult2.factorization_of_scalars()
Out[42]:
, , , , , , , ,  ⊢  

Distribution over summations

In [43]:
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.

In [44]:
qmult3
Out[44]:
In [45]:
QmultCodomain.membership_object(qmult3).expr
Out[45]:
In [46]:
InClass(qmult3, QmultCodomain).prove()
Out[46]:
, , , , , , , , , ,  ⊢  
In [47]:
qmult3.distribution(2)
Out[47]:
, , , , , , , , , ,  ⊢  
In [48]:
qmult4
Out[48]:
In [49]:
qmult4.distribution(2)
Out[49]:
, , , , , , , , ,  ⊢  
In [50]:
qmult5
Out[50]:
In [51]:
qmult5.distribution(3)
Out[51]:
, , , , , , ,  ⊢  
In [52]:
qmult6
Out[52]:
In [53]:
qmult6.distribution(3)
Out[53]:
, , , , , , ,  ⊢  

Simplification

In [54]:
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.

In [55]:
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.

In [56]:
Qmult.change_simplification_directives(ungroup=True, 
                                       factor_scalars=True,
                                       use_scalar_mult=True)
In [57]:
qmult1.simplification()
Out[57]:
, , , , , ,  ⊢  
In [58]:
qmult1_associated
Out[58]:
In [59]:
qmult1_associated.simplification()
Out[59]:
, , , , , ,  ⊢  
In [60]:
qmult4
Out[60]:
In [61]:
qmult4.simplification()
Out[61]:
, , , , , , , , ,  ⊢  
In [62]:
%end demonstrations