Expression of type Implies

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 Conditional, ExprRange, Lambda, Variable, VertExprArray, e, l
from proveit.logic import And, Equals, Forall, Implies, InSet, Union
from proveit.numbers import Add, Interval, ModAbs, greater, one
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import ModAdd, QPE, _U, _b_floor, _full_domain, _ket_u, _neg_domain, _pos_domain, _s, _s_wire, _t, _two_pow_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(sub_expr2, sub_expr3)
sub_expr5 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr3))
sub_expr6 = greater(ModAbs(l, _two_pow_t), e)
sub_expr7 = Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, Input(state = ket_plus), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr1), targets = sub_expr4), one, _s)], [ExprRange(sub_expr1, sub_expr5, one, _t), ExprRange(sub_expr1, sub_expr5, sub_expr2, sub_expr3)], [ExprRange(sub_expr1, Measure(basis = Z), one, _t), _s_wire], [ExprRange(sub_expr1, MultiQubitElem(element = Output(state = NumKet(ModAdd(_b_floor, l), _t), part = sub_expr1), targets = Interval(one, _t)), one, _t), ExprRange(sub_expr1, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr1), targets = sub_expr4), one, _s)]))
sub_expr8 = Conditional(sub_expr7, And(InSet(l, _full_domain), sub_expr6))
sub_expr9 = Conditional(sub_expr7, And(InSet(l, Union(_neg_domain, _pos_domain)), sub_expr6))
expr = Implies(Forall(instance_param_or_params = [l], instance_expr = Equals(sub_expr9, sub_expr8)), Equals(Lambda(l, sub_expr9), Lambda(l, sub_expr8)).with_wrapping_at(2)).with_wrapping_at(2)

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())

\begin{array}{c} \begin{array}{l} \left[\forall_{l}~\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 b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \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_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array} \textrm{ if } l \in \left(\{-2^{t - 1} + 1~\ldotp \ldotp~-\left(e + 1\right)\} \cup \{e + 1~\ldotp \ldotp~2^{t - 1}\}\right) ,  \left|l\right|_{\textup{mod}\thinspace 2^{t}} > e\right.. = \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_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \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_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array} \textrm{ if } l \in \{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\} ,  \left|l\right|_{\textup{mod}\thinspace 2^{t}} > e\right..\right)\right] \Rightarrow  \\ \left(\begin{array}{c} \begin{array}{l} \left[l \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 b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \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_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array} \textrm{ if } l \in \left(\{-2^{t - 1} + 1~\ldotp \ldotp~-\left(e + 1\right)\} \cup \{e + 1~\ldotp \ldotp~2^{t - 1}\}\right) ,  \left|l\right|_{\textup{mod}\thinspace 2^{t}} > e\right..\right] =  \\ \left[l \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 b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \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_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & \meter & \ghostqout{\lvert b_{\textit{f}} \oplus l \rangle_{t}} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}\left(U, t\right)} & { /^{s} } \qw & \qout{\lvert u \rangle}
} \end{array} \textrm{ if } l \in \{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\} ,  \left|l\right|_{\textup{mod}\thinspace 2^{t}} > e\right..\right] \end{array} \end{array}\right) \end{array} \end{array}

stored_expr.style_options()

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.	()	(2)	('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',)
direction	Direction of the relation (normal or reversed)	normal	normal	('with_direction_reversed', 'is_reversed')

# display the expression information
stored_expr.expr_info()

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