# 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.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]:

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