# Common expressions for the theory of proveit.physics.quantum.circuits¶

In [1]:
import proveit
# Prepare this notebook for defining the common expressions of a theory:
%common_expressions_notebook # Keep this at the top following 'import proveit'.

from proveit import (Function, Variable, IndexedVar, Conditional, ConditionalSet,
ExprRange, ExprTuple, VertExprArray, var_range)
from proveit import a, b, i, j, k, l, m, n, p, t, A, B, C, D, N, P, Q, R, S, U, pi
from proveit.core_expr_types import (
a_i, b_i, c_i, i_k, j_k, n_k, n_1_to_m, A_k, A_1_to_m,
U_1_to_m, U_1_to_i, V_1_to_j)
from proveit.core_expr_types.expr_arrays import (
Aij, Bij, Cij, Dij, Eij, Pij, Qij, Rij, Sij, Tij, Uij, Vij,
A11_to_Akl, A11_to_Akl_varray, B11_to_Bmn, B11_to_Bkl_varray,
D11_to_Dmn, S11_to_Smn)
from proveit.logic import (And, Equals, NotEquals, Set, InSet, CartExp, Disjoint,
InvImage)
from proveit.numbers import NaturalPos, Complex, Interval, zero, one, two, three
from proveit.numbers import Add, Neg, subtract, frac, sqrt, Exp, exp2pi_i, greater
from proveit.linear_algebra import VecAdd, ScalarMult, TensorProd
from proveit.physics.quantum import (
I, X, Y, Z, H, Ket, varphi, ket_plus, ket0, ket1, var_ket_u, var_ket_v, m_ket_domain,
var_ket_psi, NumKet, Qmult)
from proveit.physics.quantum.circuits import (
Qcircuit, Gate, Input, Output, Measure, MultiQubitElem,
control_elem, multi_wire, multi_gate_entries,
multi_input_entries, multi_output_entries, multi_measure_entries)

In [2]:
%begin common

Defining common sub-expressions for theory 'proveit.physics.quantum.circuits'
Subsequent end-of-cell assignments will define common sub-expressions
%end_common will finalize the definitions

In [3]:
Igate, Xgate, Ygate, Zgate, Hgate = Gate(I), Gate(X), Gate(Y), Gate(Z), Gate(H)

Igate:
Xgate:
Ygate:
Zgate:
Hgate:
In [4]:
target = Gate(X).with_implicit_representation()

target:
In [5]:
unitary_gate_op = Qcircuit(
VertExprArray([*multi_input_entries(var_ket_psi, one, m, (one, m))],
[*multi_gate_entries(U, one, m, (one, m))],
[*multi_output_entries(Qmult(U, var_ket_psi), one, m, (one, m))]))

unitary_gate_op:
In [6]:
qubit_meas = Qcircuit(VertExprArray([Input(var_ket_psi)], [Measure(Z)], [Output(Ket(b))]))

qubit_meas:
In [7]:
register_meas = Qcircuit(VertExprArray(
[*multi_input_entries(var_ket_psi, one, m, (one, m))],
[ExprRange(k, Measure(Z), one, m)],
[*multi_output_entries(NumKet(n, m), one, m, (one, m))]))

register_meas:
In [8]:
circuit_Am = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(A, i), one, m)))

circuit_Am:
In [9]:
circuit_Bn = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(B, i), one, n)))

circuit_Bn:
In [10]:
circuit_Bk = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(B, i), one, k)))

circuit_Bk:
In [11]:
circuit_Dm = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(D, i), one, m)))

circuit_Dm:
In [12]:
circuit_AjBkCl = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(A, i), one, j),
ExprRange(i, IndexedVar(B, i), one, k),
ExprRange(i, IndexedVar(C, i), one, l)))

circuit_AjBkCl:
In [13]:
circuit_AjDmCl = Qcircuit(VertExprArray(
ExprRange(i, IndexedVar(A, i), one, j),
ExprRange(i, IndexedVar(D, i), one, m),
ExprRange(i, IndexedVar(C, i), one, l)))

circuit_AjDmCl:
In [14]:
circuit_aUb = Qcircuit(VertExprArray(
[*multi_input_entries(a, one, k, (one, k))],
U_1_to_m,
[*multi_output_entries(b, one, k, (one, k))]))

circuit_aUb:
In [15]:
circuit_aU = Qcircuit(VertExprArray(
[*multi_input_entries(a, one, k, (one, k))],
U_1_to_m))

circuit_aU:
In [16]:
circuit_Ua = Qcircuit(VertExprArray(
U_1_to_m,
[*multi_output_entries(a, one, k, (one, k))]))

circuit_Ua:
In [17]:
circuit_Ub = Qcircuit(VertExprArray(
U_1_to_m,
[*multi_output_entries(b, one, k, (one, k))]))

circuit_Ub:
In [18]:
circuit_b = Qcircuit(VertExprArray(
[*multi_input_entries(b, one, k, (one, k))]))

circuit_b:
In [19]:
circuit_Akm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Aij, Rij), one, k)], one, m)))

circuit_Akm:
In [20]:
circuit_Bkm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Bij, Sij), one, k)], one, m)))

circuit_Bkm:
In [21]:
circuit_Bkn = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Bij, Sij), one, k)], one, n)))

circuit_Bkn:
In [22]:
circuit_Ckm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Cij, Tij), one, k)], one, m)))

circuit_Ckm:
In [23]:
circuit_Dkn = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Dij, Uij), one, k)], one, n)))

circuit_Dkn:
In [24]:
circuit_AkClm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Aij, Rij), one, k),
ExprRange(j, MultiQubitElem(Cij, Tij), one, l)],
one, m)))

circuit_AkClm:
In [25]:
circuit_BkClm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j, MultiQubitElem(Bij, Sij), one, k),
ExprRange(j, MultiQubitElem(Cij, Tij), one, l)],
one, m)))

circuit_BkClm:
In [26]:
no_1tok_in_Ts = ExprRange(i, ExprRange(j, Disjoint(Tij, Interval(one, k)), one, m), one, l)

no_1tok_in_Ts:
In [27]:
no_1tok_in_Ts.body

In [28]:
no_1tok_in_Ts = (ExprRange(i, ExprRange(j, Disjoint(Tij, Interval(one, k)), one, m), one, l)
.with_wrapping_at(8, 16))

no_1tok_in_Ts:
In [29]:
circuit_permuted_Akm = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j,
MultiQubitElem(IndexedVar(A, [pi, j]),
Function(InvImage(p), IndexedVar(R, [pi, j]))),
one, k)],
one, m)))

circuit_permuted_Akm:
In [30]:
circuit_permuted_Bkn = Qcircuit(VertExprArray(
ExprRange(i, [ExprRange(j,
MultiQubitElem(IndexedVar(B, [pi, j]),
Function(InvImage(p), IndexedVar(S, [pi, j]))),
one, k)],
one, n)))

circuit_permuted_Bkn:
In [31]:
circuit_compressed_inputAm = Qcircuit(
VertExprArray([*multi_input_entries(A, one, m, (one, m))]))

circuit_compressed_inputAm:
In [32]:
circuit_compressed_outputAm = Qcircuit(
VertExprArray([*multi_output_entries(A, one, m, (one, m))]))

circuit_compressed_outputAm:
In [33]:
circuit_expanded_inputBm = Qcircuit(
VertExprArray([ExprRange(k, Input(IndexedVar(B, k)), one, m)]))

circuit_expanded_inputBm:
In [34]:
circuit_expanded_outputBm = Qcircuit(
VertExprArray([ExprRange(k, Output(IndexedVar(B, k)), one, m)]))

circuit_expanded_outputBm:
In [35]:
N_0_to_m = var_range(N, zero, m)

N_0_to_m:
In [36]:
N_0 = IndexedVar(N, zero)

N_0:
In [37]:
N_m = IndexedVar(N, m)

N_m:
In [38]:
N_km1 = IndexedVar(N, subtract(k, one))

N_km1:
In [39]:
kth_start = Add(N_km1, one)

kth_start:
In [40]:
N_k = IndexedVar(N, k)

N_k:
In [41]:
each_Nk_is_partial_sum = And(Equals(N_0, zero),
ExprRange(k, Equals(N_k, Add(N_km1, n_k)), one, m))

each_Nk_is_partial_sum:
In [42]:
input_Ak_nk = (list(multi_input_entries(A_k, kth_start, N_k, (one, n_k),
check_part_index_span=True))[0]
.with_wrapping_at(2, 6))

input_Ak_nk:
In [43]:
output_Ak_nk = (list(multi_output_entries(A_k, kth_start, N_k, (one, n_k),
check_part_index_span=True))[0]
.with_wrapping_at(2, 6))

output_Ak_nk:
In [44]:
consolidated_input_A_1_to_m = ExprRange(
i, MultiQubitElem(Input(TensorProd(A_1_to_m), part=i),
targets=Interval(one, N_m)), kth_start, N_k).with_wrapping_at(2, 6)

consolidated_input_A_1_to_m:
In [45]:
consolidated_output_A_1_to_m = ExprRange(
i, MultiQubitElem(Output(TensorProd(A_1_to_m), part=i),
targets=Interval(one, N_m)), kth_start, N_k).with_wrapping_at(2, 6)

consolidated_output_A_1_to_m:
In [46]:
circuit_Ui_psi_m = Qcircuit(
VertExprArray(U_1_to_i.with_front_expansion(1),
[*multi_output_entries(var_ket_psi, one, m, (one, m))]))

circuit_Ui_psi_m:
In [47]:
circuit_psi_m_Vj = Qcircuit(
VertExprArray([*multi_input_entries(var_ket_psi, one, m, (one, m))],
V_1_to_j.with_front_expansion(1)))

circuit_psi_m_Vj:
In [48]:
circuit_Ui_Vj = Qcircuit(VertExprArray(U_1_to_i, V_1_to_j))

circuit_Ui_Vj:
In [49]:
circuit_Akl = Qcircuit(A11_to_Akl_varray)

circuit_Akl:
In [50]:
circuit_Bkl = Qcircuit(B11_to_Bkl_varray)

circuit_Bkl:
In [51]:
circuit__u_Akl_v = Qcircuit(VertExprArray(
[*multi_input_entries(var_ket_u, one, l, (one, l))],
ExprRange(i, ExprTuple(ExprRange(j, Aij, one, l)),
one, k),
[*multi_output_entries(var_ket_v, one, l, (one, l))]))

circuit__u_Akl_v:
In [52]:
m_wire = multi_wire(m)

m_wire:
In [53]:
n_wire = multi_wire(n)

n_wire:
In [54]:
circuit__psi_m__u_Akl_v = Qcircuit(VertExprArray(
[*multi_input_entries(var_ket_psi, one, m, (one, m)),
ExprRange(i, ExprTuple(multi_wire(m),
ExprRange(j, Aij, one, l)),
one, k),
[*multi_output_entries(var_ket_psi, one, m, (one, m)),

circuit__psi_m__u_Akl_v:
In [55]:
circuit__u_Akl_v__psi_m = Qcircuit(VertExprArray(
[*multi_input_entries(var_ket_u, one, l, (one, l)),
ExprRange(i, ExprTuple(ExprRange(j, Aij, one, l),
multi_wire(m)),
one, k),
[*multi_output_entries(var_ket_v, one, l, (one, l)),

circuit__u_Akl_v__psi_m:
In [56]:
phase_kickback_circuit = Qcircuit(VertExprArray(

phase_kickback_circuit:
In [57]:
phase_kickback_on_register_circuit = Qcircuit(VertExprArray(
[ExprRange(i, Input(ket_plus), one, t),
ExprRange(i,
[ExprRange(j, ConditionalSet(
Equals(i, j)),
Conditional(Gate(I), NotEquals(i, j))),
one, t).with_case_simplification(),

%end common

phase_kickback_on_register_circuit expression notebook is being updated