logo

Expression of type Forall

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 ExprRange, IndexedVar, U, Variable, m, t
from proveit.linear_algebra import MatrixMult, ScalarMult, Unitary
from proveit.logic import Equals, Forall
from proveit.numbers import Exp, Mult, NaturalPos, e, i, one, pi, two
from proveit.physics.quantum import m_ket_domain, normalized_var_ket_u, var_ket_u, varphi
from proveit.physics.quantum.circuits import phase_kickback_on_register_circuit
from proveit.statistics import Prob
In [2]:
# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = IndexedVar(U, sub_expr1)
sub_expr3 = IndexedVar(varphi, sub_expr1)
expr = Forall(instance_param_or_params = [m, t], instance_expr = Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr2, one, t)], instance_expr = Forall(instance_param_or_params = [var_ket_u], instance_expr = Forall(instance_param_or_params = [ExprRange(sub_expr1, sub_expr3, one, t)], instance_expr = Equals(Prob(phase_kickback_on_register_circuit), one), condition = ExprRange(sub_expr1, Equals(MatrixMult(sub_expr2, var_ket_u), ScalarMult(Exp(e, Mult(two, pi, i, sub_expr3)), var_ket_u)), one, t)).with_wrapping(), domain = m_ket_domain, condition = normalized_var_ket_u).with_wrapping(), domain = Unitary(Exp(two, m))).with_wrapping(), domain = NaturalPos).with_wrapping()
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())
\begin{array}{l}\forall_{m, t \in \mathbb{N}^+}~\\
\left[\begin{array}{l}\forall_{U_{1}, U_{2}, \ldots, U_{t} \in \textrm{U}\left(2^{m}\right)}~\\
\left[\begin{array}{l}\forall_{\lvert u \rangle \in \mathbb{C}^{2^{m}}~|~\left \|\lvert u \rangle\right \| = 1}~\\
\left[\begin{array}{l}\forall_{\varphi_{1}, \varphi_{2}, \ldots, \varphi_{t}~|~\left(\left(U_{1} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert u \rangle\right)\right), \left(\left(U_{2} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert u \rangle\right)\right), \ldots, \left(\left(U_{t} \thinspace \lvert u \rangle\right) = \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{t}} \cdot \lvert u \rangle\right)\right)}~\\
\left(\textrm{Pr}\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{1}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{2}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot \varphi_{t}} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U_{1}} & \gate{U_{2}} & \gate{\cdots} & \gate{U_{t}} & \qout{\lvert u \rangle}
} \end{array}\right) = 1\right)\end{array}\right]\end{array}\right]\end{array}\right]\end{array}
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
with_wrappingIf 'True', wrap the Expression after the parametersNoneTrue('with_wrapping',)
condition_wrappingWrap 'before' or 'after' the condition (or None).NoneNone/False('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_paramsIf 'True', wraps every two parameters AND wraps the Expression after the parametersNoneNone/False('with_params',)
justificationjustify to the 'left', 'center', or 'right' in the array cellscentercenter('with_justification',)
In [6]:
# display the expression information
stored_expr.expr_info()
 core typesub-expressionsexpression
0Operationoperator: 30
operand: 2
1ExprTuple2
2Lambdaparameters: 3
body: 4
3ExprTuple159, 175
4Conditionalvalue: 5
condition: 6
5Operationoperator: 30
operand: 9
6Operationoperator: 52
operands: 8
7ExprTuple9
8ExprTuple10, 11
9Lambdaparameters: 12
body: 13
10Operationoperator: 40
operands: 14
11Operationoperator: 40
operands: 15
12ExprTuple16
13Conditionalvalue: 17
condition: 18
14ExprTuple159, 19
15ExprTuple175, 19
16ExprRangelambda_map: 20
start_index: 176
end_index: 175
17Operationoperator: 30
operand: 23
18Operationoperator: 52
operands: 22
19Literal
20Lambdaparameter: 185
body: 89
21ExprTuple23
22ExprTuple24
23Lambdaparameter: 123
body: 25
24ExprRangelambda_map: 26
start_index: 176
end_index: 175
25Conditionalvalue: 27
condition: 28
26Lambdaparameter: 185
body: 29
27Operationoperator: 30
operand: 34
28Operationoperator: 52
operands: 32
29Operationoperator: 40
operands: 33
30Literal
31ExprTuple34
32ExprTuple35, 36
33ExprTuple89, 37
34Lambdaparameters: 38
body: 39
35Operationoperator: 40
operands: 41
36Operationoperator: 136
operands: 42
37Operationoperator: 43
operand: 61
38ExprTuple45
39Conditionalvalue: 46
condition: 47
40Literal
41ExprTuple123, 48
42ExprTuple49, 176
43Literal
44ExprTuple61
45ExprRangelambda_map: 50
start_index: 176
end_index: 175
46Operationoperator: 136
operands: 51
47Operationoperator: 52
operands: 53
48Operationoperator: 54
operands: 55
49Operationoperator: 56
operand: 123
50Lambdaparameter: 185
body: 182
51ExprTuple58, 176
52Literal
53ExprTuple59
54Literal
55ExprTuple60, 61
56Literal
57ExprTuple123
58Operationoperator: 62
operand: 66
59ExprRangelambda_map: 64
start_index: 176
end_index: 175
60Literal
61Operationoperator: 167
operands: 65
62Literal
63ExprTuple66
64Lambdaparameter: 185
body: 67
65ExprTuple179, 159
66Operationoperator: 68
operands: 69
67Operationoperator: 136
operands: 70
68Literal
69ExprTuple71, 72, 73
70ExprTuple74, 75
71ExprTuple76, 77
72ExprRangelambda_map: 78
start_index: 176
end_index: 175
73ExprTuple79, 80
74Operationoperator: 81
operands: 82
75Operationoperator: 154
operands: 83
76ExprRangelambda_map: 84
start_index: 176
end_index: 175
77ExprRangelambda_map: 85
start_index: 176
end_index: 159
78Lambdaparameter: 158
body: 86
79ExprRangelambda_map: 87
start_index: 176
end_index: 175
80ExprRangelambda_map: 88
start_index: 176
end_index: 159
81Literal
82ExprTuple89, 123
83ExprTuple162, 123
84Lambdaparameter: 185
body: 90
85Lambdaparameter: 185
body: 91
86ExprTuple92, 93
87Lambdaparameter: 185
body: 94
88Lambdaparameter: 185
body: 95
89IndexedVarvariable: 149
index: 185
90Operationoperator: 109
operands: 96
91Operationoperator: 134
operands: 97
92ExprRangelambda_map: 98
start_index: 176
end_index: 175
93ExprRangelambda_map: 99
start_index: 176
end_index: 159
94Operationoperator: 114
operands: 100
95Operationoperator: 134
operands: 101
96NamedExprsstate: 102
97NamedExprselement: 103
targets: 120
98Lambdaparameter: 185
body: 104
99Lambdaparameter: 185
body: 105
100NamedExprsstate: 106
101NamedExprselement: 107
targets: 120
102Operationoperator: 169
operand: 116
103Operationoperator: 109
operands: 115
104Operationoperator: 110
operands: 111
105Operationoperator: 134
operands: 112
106Operationoperator: 154
operands: 113
107Operationoperator: 114
operands: 115
108ExprTuple116
109Literal
110Literal
111ExprTuple117, 118
112NamedExprselement: 119
targets: 120
113ExprTuple121, 122
114Literal
115NamedExprsstate: 123
part: 185
116Literal
117Conditionalvalue: 124
condition: 125
118Conditionalvalue: 126
condition: 127
119Operationoperator: 137
operands: 128
120Operationoperator: 129
operands: 130
121Operationoperator: 165
operands: 131
122Operationoperator: 132
operands: 133
123Variable
124Operationoperator: 134
operands: 135
125Operationoperator: 136
operands: 140
126Operationoperator: 137
operands: 138
127Operationoperator: 139
operands: 140
128NamedExprsoperation: 141
part: 185
129Literal
130ExprTuple164, 142
131ExprTuple176, 143
132Literal
133ExprTuple144, 145
134Literal
135NamedExprselement: 146
targets: 147
136Literal
137Literal
138NamedExprsoperation: 148
139Literal
140ExprTuple158, 185
141IndexedVarvariable: 149
index: 158
142Operationoperator: 171
operands: 151
143Operationoperator: 167
operands: 152
144Operationoperator: 169
operand: 161
145Operationoperator: 154
operands: 155
146Literal
147Operationoperator: 156
operand: 164
148Literal
149Variable
150ExprTuple158
151ExprTuple175, 159
152ExprTuple179, 160
153ExprTuple161
154Literal
155ExprTuple162, 163
156Literal
157ExprTuple164
158Variable
159Variable
160Operationoperator: 165
operands: 166
161Literal
162Operationoperator: 167
operands: 168
163Operationoperator: 169
operand: 176
164Operationoperator: 171
operands: 172
165Literal
166ExprTuple176, 179
167Literal
168ExprTuple173, 174
169Literal
170ExprTuple176
171Literal
172ExprTuple175, 176
173Literal
174Operationoperator: 177
operands: 178
175Variable
176Literal
177Literal
178ExprTuple179, 180, 181, 182
179Literal
180Literal
181Literal
182IndexedVarvariable: 183
index: 185
183Variable
184ExprTuple185
185Variable