logo

Expression of type Conditional

from the theory of proveit.physics.quantum.circuits

In [1]:
import proveit
# Automation is not needed when building an expression:
proveit.defaults.automation = False # This will speed things up.
proveit.defaults.inline_pngs = False # Makes files smaller.
%load_expr # Load the stored expression as 'stored_expr'
# import Expression classes needed to build the expression
from proveit import A, Conditional, ExprRange, IndexedVar, N, Variable, VertExprArray, m, n
from proveit.core_expr_types import A_1_to_m
from proveit.linear_algebra import TensorProd
from proveit.logic import And, CartExp, Forall, InSet
from proveit.numbers import Add, Complex, Exp, Interval, Natural, one, subtract, two
from proveit.physics.quantum.circuits import MultiQubitElem, N_0_to_m, N_m, Output, Qcircuit, QcircuitEquiv, each_Nk_is_partial_sum
In [2]:
# build up the expression from sub-expressions
sub_expr1 = Variable("_b", latex_format = r"{_{-}b}")
sub_expr2 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr3 = Variable("_c", latex_format = r"{_{-}c}")
expr = Conditional(Forall(instance_param_or_params = [N_0_to_m], instance_expr = QcircuitEquiv(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, ExprRange(sub_expr2, MultiQubitElem(element = Output(state = IndexedVar(A, sub_expr1), part = sub_expr2), targets = Interval(Add(IndexedVar(N, subtract(sub_expr1, one)), one), IndexedVar(N, sub_expr1))), one, IndexedVar(n, sub_expr1)).with_wrapping_at(2,6), one, m)])), Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr3, ExprRange(sub_expr1, MultiQubitElem(element = Output(state = TensorProd(A_1_to_m), part = sub_expr1), targets = Interval(one, N_m)), Add(IndexedVar(N, subtract(sub_expr3, one)), one), IndexedVar(N, sub_expr3)).with_wrapping_at(2,6), one, m)]))), domain = Natural, condition = each_Nk_is_partial_sum).with_wrapping(), And(ExprRange(sub_expr2, InSet(IndexedVar(A, sub_expr2), CartExp(Complex, Exp(two, IndexedVar(n, sub_expr2)))), one, m)))
expr:
In [3]:
# check that the built expression is the same as the stored expression
assert expr == stored_expr
assert expr._style_id == stored_expr._style_id
print("Passed sanity check: expr matches stored_expr")
Passed sanity check: expr matches stored_expr
In [4]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())
\left\{\begin{array}{l}\forall_{N_{0}, N_{1}, \ldots, N_{m} \in \mathbb{N}~|~\left(N_{0} = 0\right)\land \left(N_{1} = \left(N_{1 - 1} + n_{1}\right)\right) \land  \left(N_{2} = \left(N_{2 - 1} + n_{2}\right)\right) \land  \ldots \land  \left(N_{m} = \left(N_{m - 1} + n_{m}\right)\right)}~\\
\left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \qout{A_{1}~\mbox{part}~1~\mbox{on}~\{N_{1 - 1} + 1~\ldotp \ldotp~N_{1}\}} \\
& \qout{A_{1}~\mbox{part}~2~\mbox{on}~\{N_{1 - 1} + 1~\ldotp \ldotp~N_{1}\}} \\
& \qout{\vdots} \\
& \qout{A_{1}~\mbox{part}~n_{1}~\mbox{on}~\{N_{1 - 1} + 1~\ldotp \ldotp~N_{1}\}} \\
& \qout{A_{2}~\mbox{part}~1~\mbox{on}~\{N_{2 - 1} + 1~\ldotp \ldotp~N_{2}\}} \\
& \qout{A_{2}~\mbox{part}~2~\mbox{on}~\{N_{2 - 1} + 1~\ldotp \ldotp~N_{2}\}} \\
& \qout{\vdots} \\
& \qout{A_{2}~\mbox{part}~n_{2}~\mbox{on}~\{N_{2 - 1} + 1~\ldotp \ldotp~N_{2}\}} \\
& \qout{\begin{array}{c}\vdots\\ \vdots\end{array}} \\
& \qout{A_{m}~\mbox{part}~1~\mbox{on}~\{N_{m - 1} + 1~\ldotp \ldotp~N_{m}\}} \\
& \qout{A_{m}~\mbox{part}~2~\mbox{on}~\{N_{m - 1} + 1~\ldotp \ldotp~N_{m}\}} \\
& \qout{\vdots} \\
& \qout{A_{m}~\mbox{part}~n_{m}~\mbox{on}~\{N_{m - 1} + 1~\ldotp \ldotp~N_{m}\}}
} \end{array}\right) \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \qout{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{1 - 1} + 1~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\
& \qout{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{1 - 1} + 2~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\
& \qout{\vdots} \\
& \qout{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{1}~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\
& \qout{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{2 - 1} + 1~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\
& \qout{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{2 - 1} + 2~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\
& \qout{\vdots} \\
& \qout{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{2}~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\
& \qout{\begin{array}{c}\vdots\\ \vdots\end{array}} \\
& \qout{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{m - 1} + 1~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\
& \qout{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{m - 1} + 2~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} \\
& \qout{\vdots} \\
& \qout{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{m}~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}}
} \end{array}\right)\right)\end{array} \textrm{ if } \left(A_{1} \in \mathbb{C}^{2^{n_{1}}}\right) \land  \left(A_{2} \in \mathbb{C}^{2^{n_{2}}}\right) \land  \ldots \land  \left(A_{m} \in \mathbb{C}^{2^{n_{m}}}\right)\right..
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
condition_delimiter'comma' or 'and'commacomma('with_comma_delimiter', 'with_conjunction_delimiter')
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Conditionalvalue: 1
condition: 2
1Operationoperator: 3
operand: 6
2Operationoperator: 29
operands: 5
3Literal
4ExprTuple6
5ExprTuple7
6Lambdaparameters: 8
body: 9
7ExprRangelambda_map: 10
start_index: 123
end_index: 111
8ExprTuple11
9Conditionalvalue: 12
condition: 13
10Lambdaparameter: 120
body: 14
11ExprRangelambda_map: 15
start_index: 64
end_index: 111
12Operationoperator: 16
operands: 17
13Operationoperator: 29
operands: 18
14Operationoperator: 42
operands: 19
15Lambdaparameter: 120
body: 65
16Literal
17ExprTuple20, 21
18ExprTuple22, 23
19ExprTuple113, 24
20Operationoperator: 26
operand: 33
21Operationoperator: 26
operand: 34
22ExprRangelambda_map: 28
start_index: 64
end_index: 111
23Operationoperator: 29
operands: 30
24Operationoperator: 31
operands: 32
25ExprTuple33
26Literal
27ExprTuple34
28Lambdaparameter: 120
body: 35
29Literal
30ExprTuple36, 37
31Literal
32ExprTuple38, 39
33ExprTuple40
34ExprTuple41
35Operationoperator: 42
operands: 43
36Operationoperator: 57
operands: 44
37ExprRangelambda_map: 45
start_index: 123
end_index: 111
38Literal
39Operationoperator: 46
operands: 47
40ExprRangelambda_map: 48
start_index: 123
end_index: 111
41ExprRangelambda_map: 49
start_index: 123
end_index: 111
42Literal
43ExprTuple65, 50
44ExprTuple51, 64
45Lambdaparameter: 120
body: 52
46Literal
47ExprTuple53, 77
48Lambdaparameter: 118
body: 54
49Lambdaparameter: 105
body: 55
50Literal
51IndexedVarvariable: 108
index: 64
52Operationoperator: 57
operands: 58
53Literal
54ExprRangelambda_map: 59
start_index: 123
end_index: 60
55ExprRangelambda_map: 61
start_index: 62
end_index: 63
56ExprTuple64
57Literal
58ExprTuple65, 66
59Lambdaparameter: 120
body: 67
60IndexedVarvariable: 84
index: 118
61Lambdaparameter: 118
body: 68
62Operationoperator: 114
operands: 69
63IndexedVarvariable: 108
index: 105
64Literal
65IndexedVarvariable: 108
index: 120
66Operationoperator: 114
operands: 71
67Operationoperator: 73
operands: 72
68Operationoperator: 73
operands: 74
69ExprTuple75, 123
70ExprTuple105
71ExprTuple76, 77
72NamedExprselement: 78
targets: 79
73Literal
74NamedExprselement: 80
targets: 81
75IndexedVarvariable: 108
index: 91
76IndexedVarvariable: 108
index: 92
77IndexedVarvariable: 84
index: 120
78Operationoperator: 87
operands: 85
79Operationoperator: 89
operands: 86
80Operationoperator: 87
operands: 88
81Operationoperator: 89
operands: 90
82ExprTuple91
83ExprTuple92
84Variable
85NamedExprsstate: 93
part: 120
86ExprTuple94, 95
87Literal
88NamedExprsstate: 96
part: 118
89Literal
90ExprTuple123, 97
91Operationoperator: 114
operands: 98
92Operationoperator: 114
operands: 99
93IndexedVarvariable: 116
index: 118
94Operationoperator: 114
operands: 100
95IndexedVarvariable: 108
index: 118
96Operationoperator: 102
operands: 103
97IndexedVarvariable: 108
index: 111
98ExprTuple105, 119
99ExprTuple120, 119
100ExprTuple106, 123
101ExprTuple118
102Literal
103ExprTuple107
104ExprTuple111
105Variable
106IndexedVarvariable: 108
index: 112
107ExprRangelambda_map: 110
start_index: 123
end_index: 111
108Variable
109ExprTuple112
110Lambdaparameter: 120
body: 113
111Variable
112Operationoperator: 114
operands: 115
113IndexedVarvariable: 116
index: 120
114Literal
115ExprTuple118, 119
116Variable
117ExprTuple120
118Variable
119Operationoperator: 121
operand: 123
120Variable
121Literal
122ExprTuple123
123Literal