Expression of type Conditional

from the theory of proveit.physics.quantum.circuits

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, n_1_to_m
from proveit.linear_algebra import TensorProd
from proveit.logic import CartExp, Forall, InSet
from proveit.numbers import Add, Complex, Exp, Interval, Natural, NaturalPos, one, subtract, two
from proveit.physics.quantum.circuits import Input, MultiQubitElem, N_0_to_m, N_m, Qcircuit, QcircuitEquiv, each_Nk_is_partial_sum

# 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_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 = Input(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 = Input(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(), InSet(m, NaturalPos))

expr:

# 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

# Show the LaTeX representation of the expression for convenience if you need it.
print(stored_expr.latex())

\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{
\qin{A_{1}~\mbox{part}~1~\mbox{on}~\{N_{1 - 1} + 1~\ldotp \ldotp~N_{1}\}} & \qw \\
\qin{A_{1}~\mbox{part}~2~\mbox{on}~\{N_{1 - 1} + 1~\ldotp \ldotp~N_{1}\}} & \qw \\
\qin{\vdots} & \qw \\
\qin{A_{1}~\mbox{part}~n_{1}~\mbox{on}~\{N_{1 - 1} + 1~\ldotp \ldotp~N_{1}\}} & \qw \\
\qin{A_{2}~\mbox{part}~1~\mbox{on}~\{N_{2 - 1} + 1~\ldotp \ldotp~N_{2}\}} & \qw \\
\qin{A_{2}~\mbox{part}~2~\mbox{on}~\{N_{2 - 1} + 1~\ldotp \ldotp~N_{2}\}} & \qw \\
\qin{\vdots} & \qw \\
\qin{A_{2}~\mbox{part}~n_{2}~\mbox{on}~\{N_{2 - 1} + 1~\ldotp \ldotp~N_{2}\}} & \qw \\
\qin{\begin{array}{c}\vdots\\ \vdots\end{array}} & \qw \\
\qin{A_{m}~\mbox{part}~1~\mbox{on}~\{N_{m - 1} + 1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{A_{m}~\mbox{part}~2~\mbox{on}~\{N_{m - 1} + 1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{\vdots} & \qw \\
\qin{A_{m}~\mbox{part}~n_{m}~\mbox{on}~\{N_{m - 1} + 1~\ldotp \ldotp~N_{m}\}} & \qw
} \end{array}\right) \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{1 - 1} + 1~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{1 - 1} + 2~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{\vdots} & \qw \\
\qin{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{1}~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{2 - 1} + 1~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{2 - 1} + 2~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{\vdots} & \qw \\
\qin{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{2}~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{\begin{array}{c}\vdots\\ \vdots\end{array}} & \qw \\
\qin{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{m - 1} + 1~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{m - 1} + 2~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} & \qw \\
\qin{\vdots} & \qw \\
\qin{A_{1} {\otimes}  A_{2} {\otimes}  \ldots {\otimes}  A_{m}~\mbox{part}~N_{m}~\mbox{on}~\{1~\ldotp \ldotp~N_{m}\}} & \qw
} \end{array}\right)\right)\end{array}\right]\end{array}\right]\end{array} \textrm{ if } m \in \mathbb{N}^+\right..

stored_expr.style_options()

name	description	default	current value	related methods
condition_delimiter	'comma' or 'and'	comma	comma	('with_comma_delimiter', 'with_conjunction_delimiter')

# display the expression information
stored_expr.expr_info()

	core type	sub-expressions	expression
0	Conditional	value: 1 condition: 2
1	Operation	operator: 21 operand: 5
2	Operation	operator: 62 operands: 4
3	ExprTuple	5
4	ExprTuple	131, 27
5	Lambda	parameters: 6 body: 7
6	ExprTuple	8
7	Conditional	value: 9 condition: 10
8	ExprRange	lambda_map: 11 start_index: 143 end_index: 131
9	Operation	operator: 21 operand: 14
10	Operation	operator: 49 operands: 13
11	Lambda	parameter: 140 body: 97
12	ExprTuple	14
13	ExprTuple	15
14	Lambda	parameters: 123 body: 16
15	ExprRange	lambda_map: 17 start_index: 143 end_index: 131
16	Conditional	value: 18 condition: 19
17	Lambda	parameter: 140 body: 20
18	Operation	operator: 21 operand: 25
19	Operation	operator: 49 operands: 23
20	Operation	operator: 62 operands: 24
21	Literal
22	ExprTuple	25
23	ExprTuple	26
24	ExprTuple	97, 27
25	Lambda	parameters: 28 body: 29
26	ExprRange	lambda_map: 30 start_index: 143 end_index: 131
27	Literal
28	ExprTuple	31
29	Conditional	value: 32 condition: 33
30	Lambda	parameter: 140 body: 34
31	ExprRange	lambda_map: 35 start_index: 84 end_index: 131
32	Operation	operator: 36 operands: 37
33	Operation	operator: 49 operands: 38
34	Operation	operator: 62 operands: 39
35	Lambda	parameter: 140 body: 85
36	Literal
37	ExprTuple	40, 41
38	ExprTuple	42, 43
39	ExprTuple	133, 44
40	Operation	operator: 46 operand: 53
41	Operation	operator: 46 operand: 54
42	ExprRange	lambda_map: 48 start_index: 84 end_index: 131
43	Operation	operator: 49 operands: 50
44	Operation	operator: 51 operands: 52
45	ExprTuple	53
46	Literal
47	ExprTuple	54
48	Lambda	parameter: 140 body: 55
49	Literal
50	ExprTuple	56, 57
51	Literal
52	ExprTuple	58, 59
53	ExprTuple	60
54	ExprTuple	61
55	Operation	operator: 62 operands: 63
56	Operation	operator: 77 operands: 64
57	ExprRange	lambda_map: 65 start_index: 143 end_index: 131
58	Literal
59	Operation	operator: 66 operands: 67
60	ExprRange	lambda_map: 68 start_index: 143 end_index: 131
61	ExprRange	lambda_map: 69 start_index: 143 end_index: 131
62	Literal
63	ExprTuple	85, 70
64	ExprTuple	71, 84
65	Lambda	parameter: 140 body: 72
66	Literal
67	ExprTuple	73, 97
68	Lambda	parameter: 138 body: 74
69	Lambda	parameter: 125 body: 75
70	Literal
71	IndexedVar	variable: 128 index: 84
72	Operation	operator: 77 operands: 78
73	Literal
74	ExprRange	lambda_map: 79 start_index: 143 end_index: 80
75	ExprRange	lambda_map: 81 start_index: 82 end_index: 83
76	ExprTuple	84
77	Literal
78	ExprTuple	85, 86
79	Lambda	parameter: 140 body: 87
80	IndexedVar	variable: 104 index: 138
81	Lambda	parameter: 138 body: 88
82	Operation	operator: 134 operands: 89
83	IndexedVar	variable: 128 index: 125
84	Literal
85	IndexedVar	variable: 128 index: 140
86	Operation	operator: 134 operands: 91
87	Operation	operator: 93 operands: 92
88	Operation	operator: 93 operands: 94
89	ExprTuple	95, 143
90	ExprTuple	125
91	ExprTuple	96, 97
92	NamedExprs	element: 98 targets: 99
93	Literal
94	NamedExprs	element: 100 targets: 101
95	IndexedVar	variable: 128 index: 111
96	IndexedVar	variable: 128 index: 112
97	IndexedVar	variable: 104 index: 140
98	Operation	operator: 107 operands: 105
99	Operation	operator: 109 operands: 106
100	Operation	operator: 107 operands: 108
101	Operation	operator: 109 operands: 110
102	ExprTuple	111
103	ExprTuple	112
104	Variable
105	NamedExprs	state: 113 part: 140
106	ExprTuple	114, 115
107	Literal
108	NamedExprs	state: 116 part: 138
109	Literal
110	ExprTuple	143, 117
111	Operation	operator: 134 operands: 118
112	Operation	operator: 134 operands: 119
113	IndexedVar	variable: 136 index: 138
114	Operation	operator: 134 operands: 120
115	IndexedVar	variable: 128 index: 138
116	Operation	operator: 122 operands: 123
117	IndexedVar	variable: 128 index: 131
118	ExprTuple	125, 139
119	ExprTuple	140, 139
120	ExprTuple	126, 143
121	ExprTuple	138
122	Literal
123	ExprTuple	127
124	ExprTuple	131
125	Variable
126	IndexedVar	variable: 128 index: 132
127	ExprRange	lambda_map: 130 start_index: 143 end_index: 131
128	Variable
129	ExprTuple	132
130	Lambda	parameter: 140 body: 133
131	Variable
132	Operation	operator: 134 operands: 135
133	IndexedVar	variable: 136 index: 140
134	Literal
135	ExprTuple	138, 139
136	Variable
137	ExprTuple	140
138	Variable
139	Operation	operator: 141 operand: 143
140	Variable
141	Literal
142	ExprTuple	143
143	Literal