Expression of type And ¶

from the theory of proveit.physics.quantum.QPE ¶

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, Lambda, Variable, VertExprArray, a, b, m
from proveit.logic import And, Forall, Functions, InSet, NotEquals
from proveit.numbers import Add, Interval, one
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import QPE, _Omega, _U, _ket_u, _m_domain, _phase_est_circuit, _s, _s_wire, _t
from proveit.physics.quantum.circuits import Gate, Input, Measure, MultiQubitElem, Output, Qcircuit

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(_t, one)
sub_expr3 = Add(_t, _s)
sub_expr4 = Interval(one, _t)
sub_expr5 = Interval(sub_expr2, sub_expr3)
sub_expr6 = [ExprRange(sub_expr1, Measure(basis = Z), one, _t), _s_wire]
sub_expr7 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr3))
sub_expr8 = ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)
sub_expr9 = [ExprRange(sub_expr1, Input(state = ket_plus), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr5), one, _s)]
sub_expr10 = [ExprRange(sub_expr1, sub_expr7, one, _t), ExprRange(sub_expr1, sub_expr7, sub_expr2, sub_expr3)]
expr = And(InSet(Lambda(m, _phase_est_circuit), Functions(_m_domain, _Omega)), Forall(instance_param_or_params = [a, b], instance_expr = NotEquals(Qcircuit(vert_expr_array = VertExprArray(sub_expr9, sub_expr10, sub_expr6, [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(a, _t), part = sub_expr1), targets = sub_expr4), one, _t), sub_expr8])), Qcircuit(vert_expr_array = VertExprArray(sub_expr9, sub_expr10, sub_expr6, [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(b, _t), part = sub_expr1), targets = sub_expr4), one, _t), sub_expr8]))), domain = _m_domain, condition = NotEquals(a, b)))

# 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(\left[m \mapsto \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}\left(U, t\right)} & \measure{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert m \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right)\right] \in \left[\{0~\ldotp \ldotp~2^{t} - 1\} \rightarrow \Omega\right]\right) \land \left[\forall_{a, b \in \{0~\ldotp \ldotp~2^{t} - 1\}~|~a \neq b}~\left(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert a \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert a \rangle_{t}} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}\left(U, t\right)} & \measure{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert a \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert a \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right) \neq \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}\left(U, t\right)} & \meter & \multiqout{3}{\lvert b \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b \rangle_{t}} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}\left(U, t\right)} & \measure{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} \qw & \ghostqout{\lvert b \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array}\right)\right)\right]

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
operation	'infix' or 'function' style formatting	infix	infix
wrap_positions	position(s) at which wrapping is to occur; '2 n - 1' is after the nth operand, '2 n' is after the nth operation.	()	()	('with_wrapping_at', 'with_wrap_before_operator', 'with_wrap_after_operator', 'without_wrapping', 'wrap_positions')
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	center	center	('with_justification',)

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

Expression of type And¶

from the theory of proveit.physics.quantum.QPE¶

Expression of type And ¶

from the theory of proveit.physics.quantum.QPE ¶