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 A, ExprRange, IndexedVar, N, Variable, VertExprArray, m, n
from proveit.core_expr_types import A_1_to_m, n_1_to_m
from proveit.linear_algebra import TensorProd
from proveit.logic import CartExp, Forall
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}")
expr = Forall(instance_param_or_params = [m], instance_expr = Forall(instance_param_or_params = [n_1_to_m], instance_expr = 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, IndexedVar(n, sub_expr2))), one, m)]).with_wrapping(), domain = NaturalPos).with_wrapping(), domain = NaturalPos)
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())
\forall_{m \in \mathbb{N}^+}~\left[\begin{array}{l}\forall_{n_{1}, n_{2}, \ldots, n_{m} \in \mathbb{N}^+}~\\
\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}\right]\end{array}\right]
In [5]:
stored_expr.style_options()
namedescriptiondefaultcurrent valuerelated methods
with_wrappingIf 'True', wrap the Expression after the parametersNoneNone/False('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: 24
operand: 2
1ExprTuple2
2Lambdaparameter: 134
body: 3
3Conditionalvalue: 4
condition: 5
4Operationoperator: 24
operand: 8
5Operationoperator: 65
operands: 7
6ExprTuple8
7ExprTuple134, 30
8Lambdaparameters: 9
body: 10
9ExprTuple11
10Conditionalvalue: 12
condition: 13
11ExprRangelambda_map: 14
start_index: 146
end_index: 134
12Operationoperator: 24
operand: 17
13Operationoperator: 52
operands: 16
14Lambdaparameter: 143
body: 100
15ExprTuple17
16ExprTuple18
17Lambdaparameters: 126
body: 19
18ExprRangelambda_map: 20
start_index: 146
end_index: 134
19Conditionalvalue: 21
condition: 22
20Lambdaparameter: 143
body: 23
21Operationoperator: 24
operand: 28
22Operationoperator: 52
operands: 26
23Operationoperator: 65
operands: 27
24Literal
25ExprTuple28
26ExprTuple29
27ExprTuple100, 30
28Lambdaparameters: 31
body: 32
29ExprRangelambda_map: 33
start_index: 146
end_index: 134
30Literal
31ExprTuple34
32Conditionalvalue: 35
condition: 36
33Lambdaparameter: 143
body: 37
34ExprRangelambda_map: 38
start_index: 87
end_index: 134
35Operationoperator: 39
operands: 40
36Operationoperator: 52
operands: 41
37Operationoperator: 65
operands: 42
38Lambdaparameter: 143
body: 88
39Literal
40ExprTuple43, 44
41ExprTuple45, 46
42ExprTuple136, 47
43Operationoperator: 49
operand: 56
44Operationoperator: 49
operand: 57
45ExprRangelambda_map: 51
start_index: 87
end_index: 134
46Operationoperator: 52
operands: 53
47Operationoperator: 54
operands: 55
48ExprTuple56
49Literal
50ExprTuple57
51Lambdaparameter: 143
body: 58
52Literal
53ExprTuple59, 60
54Literal
55ExprTuple61, 62
56ExprTuple63
57ExprTuple64
58Operationoperator: 65
operands: 66
59Operationoperator: 80
operands: 67
60ExprRangelambda_map: 68
start_index: 146
end_index: 134
61Literal
62Operationoperator: 69
operands: 70
63ExprRangelambda_map: 71
start_index: 146
end_index: 134
64ExprRangelambda_map: 72
start_index: 146
end_index: 134
65Literal
66ExprTuple88, 73
67ExprTuple74, 87
68Lambdaparameter: 143
body: 75
69Literal
70ExprTuple76, 100
71Lambdaparameter: 141
body: 77
72Lambdaparameter: 128
body: 78
73Literal
74IndexedVarvariable: 131
index: 87
75Operationoperator: 80
operands: 81
76Literal
77ExprRangelambda_map: 82
start_index: 146
end_index: 83
78ExprRangelambda_map: 84
start_index: 85
end_index: 86
79ExprTuple87
80Literal
81ExprTuple88, 89
82Lambdaparameter: 143
body: 90
83IndexedVarvariable: 107
index: 141
84Lambdaparameter: 141
body: 91
85Operationoperator: 137
operands: 92
86IndexedVarvariable: 131
index: 128
87Literal
88IndexedVarvariable: 131
index: 143
89Operationoperator: 137
operands: 94
90Operationoperator: 96
operands: 95
91Operationoperator: 96
operands: 97
92ExprTuple98, 146
93ExprTuple128
94ExprTuple99, 100
95NamedExprselement: 101
targets: 102
96Literal
97NamedExprselement: 103
targets: 104
98IndexedVarvariable: 131
index: 114
99IndexedVarvariable: 131
index: 115
100IndexedVarvariable: 107
index: 143
101Operationoperator: 110
operands: 108
102Operationoperator: 112
operands: 109
103Operationoperator: 110
operands: 111
104Operationoperator: 112
operands: 113
105ExprTuple114
106ExprTuple115
107Variable
108NamedExprsstate: 116
part: 143
109ExprTuple117, 118
110Literal
111NamedExprsstate: 119
part: 141
112Literal
113ExprTuple146, 120
114Operationoperator: 137
operands: 121
115Operationoperator: 137
operands: 122
116IndexedVarvariable: 139
index: 141
117Operationoperator: 137
operands: 123
118IndexedVarvariable: 131
index: 141
119Operationoperator: 125
operands: 126
120IndexedVarvariable: 131
index: 134
121ExprTuple128, 142
122ExprTuple143, 142
123ExprTuple129, 146
124ExprTuple141
125Literal
126ExprTuple130
127ExprTuple134
128Variable
129IndexedVarvariable: 131
index: 135
130ExprRangelambda_map: 133
start_index: 146
end_index: 134
131Variable
132ExprTuple135
133Lambdaparameter: 143
body: 136
134Variable
135Operationoperator: 137
operands: 138
136IndexedVarvariable: 139
index: 143
137Literal
138ExprTuple141, 142
139Variable
140ExprTuple143
141Variable
142Operationoperator: 144
operand: 146
143Variable
144Literal
145ExprTuple146
146Literal