Expression of type ExprTuple ¶

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, ExprTuple, Lambda, Variable, VertExprArray, l
from proveit.logic import Bijections
from proveit.numbers import Add, Interval, one
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import ModAdd, QPE, _Omega, _U, _b_floor, _full_domain, _ket_u, _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(sub_expr2, sub_expr3)
sub_expr5 = MultiQubitElem(element = Gate(operation = QPE(_U, _t), part = sub_expr1), targets = Interval(one, sub_expr3))
expr = ExprTuple(Lambda(l, 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)]))), Bijections(_full_domain, _Omega))

# 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(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}\right), \left[\{-2^{t - 1} + 1~\ldotp \ldotp~2^{t - 1}\} \xrightarrow[\text{onto}]{\text{1-to-1}} \Omega\right]\right)

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

name	description	default	current value	related methods
wrap_positions	position(s) at which wrapping is to occur; 'n' is after the nth comma.	()	()	('with_wrapping_at',)
justification	if any wrap positions are set, justify to the 'left', 'center', or 'right'	left	left	('with_justification',)

	core type	sub-expressions
0	ExprTuple	1, 2
1	Lambda	parameter: 104 body: 4
2	Operation	operator: 5 operands: 6
3	ExprTuple	104
4	Operation	operator: 7 operands: 8
5	Literal
6	ExprTuple	9, 10
7	Literal
8	ExprTuple	11, 12, 13, 14
9	Operation	operator: 73 operands: 15
10	Literal
11	ExprTuple	16, 17
12	ExprTuple	18, 19
13	ExprTuple	20, 21
14	ExprTuple	22, 23
15	ExprTuple	24, 62
16	ExprRange	lambda_map: 25 start_index: 105 end_index: 97
17	ExprRange	lambda_map: 26 start_index: 105 end_index: 96
18	ExprRange	lambda_map: 27 start_index: 105 end_index: 97
19	ExprRange	lambda_map: 27 start_index: 82 end_index: 83
20	ExprRange	lambda_map: 28 start_index: 105 end_index: 97
21	ExprRange	lambda_map: 29 start_index: 105 end_index: 96
22	ExprRange	lambda_map: 30 start_index: 105 end_index: 97
23	ExprRange	lambda_map: 31 start_index: 105 end_index: 96
24	Operation	operator: 92 operands: 32
25	Lambda	parameter: 81 body: 33
26	Lambda	parameter: 81 body: 34
27	Lambda	parameter: 81 body: 35
28	Lambda	parameter: 81 body: 36
29	Lambda	parameter: 81 body: 37
30	Lambda	parameter: 81 body: 38
31	Lambda	parameter: 81 body: 40
32	ExprTuple	41, 105
33	Operation	operator: 65 operands: 42
34	Operation	operator: 49 operands: 43
35	Operation	operator: 49 operands: 44
36	Operation	operator: 45 operands: 46
37	Operation	operator: 66 operands: 47
38	Operation	operator: 49 operands: 48
39	ExprTuple	81
40	Operation	operator: 49 operands: 50
41	Operation	operator: 101 operand: 62
42	NamedExprs	state: 52
43	NamedExprs	element: 53 targets: 61
44	NamedExprs	element: 54 targets: 55
45	Literal
46	NamedExprs	basis: 56
47	NamedExprs	operation: 57
48	NamedExprs	element: 58 targets: 59
49	Literal
50	NamedExprs	element: 60 targets: 61
51	ExprTuple	62
52	Operation	operator: 63 operand: 77
53	Operation	operator: 65 operands: 72
54	Operation	operator: 66 operands: 67
55	Operation	operator: 73 operands: 68
56	Literal
57	Literal
58	Operation	operator: 71 operands: 69
59	Operation	operator: 73 operands: 70
60	Operation	operator: 71 operands: 72
61	Operation	operator: 73 operands: 74
62	Operation	operator: 75 operands: 76
63	Literal
64	ExprTuple	77
65	Literal
66	Literal
67	NamedExprs	operation: 78 part: 81
68	ExprTuple	105, 83
69	NamedExprs	state: 79 part: 81
70	ExprTuple	105, 97
71	Literal
72	NamedExprs	state: 80 part: 81
73	Literal
74	ExprTuple	82, 83
75	Literal
76	ExprTuple	84, 85
77	Literal
78	Operation	operator: 86 operands: 87
79	Operation	operator: 88 operands: 89
80	Literal
81	Variable
82	Operation	operator: 92 operands: 90
83	Operation	operator: 92 operands: 91
84	Literal
85	Operation	operator: 92 operands: 93
86	Literal
87	ExprTuple	94, 97
88	Literal
89	ExprTuple	95, 97
90	ExprTuple	97, 105
91	ExprTuple	97, 96
92	Literal
93	ExprTuple	97, 98
94	Literal
95	Operation	operator: 99 operands: 100
96	Literal
97	Literal
98	Operation	operator: 101 operand: 105
99	Literal
100	ExprTuple	103, 104
101	Literal
102	ExprTuple	105
103	Literal
104	Variable
105	Literal

Expression of type ExprTuple¶

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

Expression of type ExprTuple ¶

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