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, NaturalPos, 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}")
sub_expr4 = IndexedVar(n, sub_expr2)
expr = Conditional(Forall(instance_param_or_params = [A_1_to_m], instance_expr = 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(), domains = [ExprRange(sub_expr2, CartExp(Complex, Exp(two, sub_expr4)), one, m)]).with_wrapping(), And(ExprRange(sub_expr2, InSet(sub_expr4, NaturalPos), 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_{\left(A_{1} \in \mathbb{C}^{2^{n_{1}}}\right), \left(A_{2} \in \mathbb{C}^{2^{n_{2}}}\right), \ldots, \left(A_{m} \in \mathbb{C}^{2^{n_{m}}}\right)}~\\
\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}\right]\end{array} \textrm{ if } \left(n_{1} \in \mathbb{N}^+\right) \land  \left(n_{2} \in \mathbb{N}^+\right) \land  \ldots \land  \left(n_{m} \in \mathbb{N}^+\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: 12
operand: 5
2Operationoperator: 40
operands: 4
3ExprTuple5
4ExprTuple6
5Lambdaparameters: 114
body: 7
6ExprRangelambda_map: 8
start_index: 134
end_index: 122
7Conditionalvalue: 9
condition: 10
8Lambdaparameter: 131
body: 11
9Operationoperator: 12
operand: 16
10Operationoperator: 40
operands: 14
11Operationoperator: 53
operands: 15
12Literal
13ExprTuple16
14ExprTuple17
15ExprTuple88, 18
16Lambdaparameters: 19
body: 20
17ExprRangelambda_map: 21
start_index: 134
end_index: 122
18Literal
19ExprTuple22
20Conditionalvalue: 23
condition: 24
21Lambdaparameter: 131
body: 25
22ExprRangelambda_map: 26
start_index: 75
end_index: 122
23Operationoperator: 27
operands: 28
24Operationoperator: 40
operands: 29
25Operationoperator: 53
operands: 30
26Lambdaparameter: 131
body: 76
27Literal
28ExprTuple31, 32
29ExprTuple33, 34
30ExprTuple124, 35
31Operationoperator: 37
operand: 44
32Operationoperator: 37
operand: 45
33ExprRangelambda_map: 39
start_index: 75
end_index: 122
34Operationoperator: 40
operands: 41
35Operationoperator: 42
operands: 43
36ExprTuple44
37Literal
38ExprTuple45
39Lambdaparameter: 131
body: 46
40Literal
41ExprTuple47, 48
42Literal
43ExprTuple49, 50
44ExprTuple51
45ExprTuple52
46Operationoperator: 53
operands: 54
47Operationoperator: 68
operands: 55
48ExprRangelambda_map: 56
start_index: 134
end_index: 122
49Literal
50Operationoperator: 57
operands: 58
51ExprRangelambda_map: 59
start_index: 134
end_index: 122
52ExprRangelambda_map: 60
start_index: 134
end_index: 122
53Literal
54ExprTuple76, 61
55ExprTuple62, 75
56Lambdaparameter: 131
body: 63
57Literal
58ExprTuple64, 88
59Lambdaparameter: 129
body: 65
60Lambdaparameter: 116
body: 66
61Literal
62IndexedVarvariable: 119
index: 75
63Operationoperator: 68
operands: 69
64Literal
65ExprRangelambda_map: 70
start_index: 134
end_index: 71
66ExprRangelambda_map: 72
start_index: 73
end_index: 74
67ExprTuple75
68Literal
69ExprTuple76, 77
70Lambdaparameter: 131
body: 78
71IndexedVarvariable: 95
index: 129
72Lambdaparameter: 129
body: 79
73Operationoperator: 125
operands: 80
74IndexedVarvariable: 119
index: 116
75Literal
76IndexedVarvariable: 119
index: 131
77Operationoperator: 125
operands: 82
78Operationoperator: 84
operands: 83
79Operationoperator: 84
operands: 85
80ExprTuple86, 134
81ExprTuple116
82ExprTuple87, 88
83NamedExprselement: 89
targets: 90
84Literal
85NamedExprselement: 91
targets: 92
86IndexedVarvariable: 119
index: 102
87IndexedVarvariable: 119
index: 103
88IndexedVarvariable: 95
index: 131
89Operationoperator: 98
operands: 96
90Operationoperator: 100
operands: 97
91Operationoperator: 98
operands: 99
92Operationoperator: 100
operands: 101
93ExprTuple102
94ExprTuple103
95Variable
96NamedExprsstate: 104
part: 131
97ExprTuple105, 106
98Literal
99NamedExprsstate: 107
part: 129
100Literal
101ExprTuple134, 108
102Operationoperator: 125
operands: 109
103Operationoperator: 125
operands: 110
104IndexedVarvariable: 127
index: 129
105Operationoperator: 125
operands: 111
106IndexedVarvariable: 119
index: 129
107Operationoperator: 113
operands: 114
108IndexedVarvariable: 119
index: 122
109ExprTuple116, 130
110ExprTuple131, 130
111ExprTuple117, 134
112ExprTuple129
113Literal
114ExprTuple118
115ExprTuple122
116Variable
117IndexedVarvariable: 119
index: 123
118ExprRangelambda_map: 121
start_index: 134
end_index: 122
119Variable
120ExprTuple123
121Lambdaparameter: 131
body: 124
122Variable
123Operationoperator: 125
operands: 126
124IndexedVarvariable: 127
index: 131
125Literal
126ExprTuple129, 130
127Variable
128ExprTuple131
129Variable
130Operationoperator: 132
operand: 134
131Variable
132Literal
133ExprTuple134
134Literal