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, ConditionalSet, ExprRange, Variable, VertExprArray, t
from proveit.linear_algebra import MatrixExp, ScalarMult, VecAdd
from proveit.logic import Equals, Implies, NotEquals, Set
from proveit.numbers import Add, Exp, Interval, Mult, Neg, e, frac, i, one, pi, sqrt, two, zero
from proveit.physics.quantum import CONTROL, ket0, ket1, ket_plus
from proveit.physics.quantum.QPE import QPE1, _U, _ket_u, _phase, _s
from proveit.physics.quantum.circuits import Gate, Igate, Input, MultiQubitElem, Output, Qcircuit, QcircuitEquiv

# 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 = Add(t, one)
sub_expr4 = Add(sub_expr1, t)
sub_expr5 = Add(t, _s)
sub_expr6 = Interval(sub_expr3, sub_expr5)
sub_expr7 = Add(Neg(t), one)
sub_expr8 = MultiQubitElem(element = Gate(operation = QPE1(_U, t), part = sub_expr2), targets = Interval(one, sub_expr5))
sub_expr9 = [ExprRange(sub_expr2, sub_expr8, one, t), ExprRange(sub_expr2, sub_expr8, sub_expr3, sub_expr5)]
sub_expr10 = [ExprRange(sub_expr2, Input(state = ket_plus), one, t), ExprRange(sub_expr2, MultiQubitElem(element = Input(state = _ket_u, part = sub_expr2), targets = sub_expr6), one, _s)]
sub_expr11 = ExprRange(sub_expr1, [ExprRange(sub_expr2, ConditionalSet(Conditional(MultiQubitElem(element = CONTROL, targets = Set(sub_expr3)), Equals(sub_expr4, sub_expr2)), Conditional(Igate, NotEquals(sub_expr4, sub_expr2))), one, t).with_case_simplification(), ExprRange(sub_expr2, MultiQubitElem(element = Gate(operation = MatrixExp(_U, Exp(two, Neg(sub_expr1))), part = sub_expr2), targets = sub_expr6), one, _s)], sub_expr7, zero).with_decreasing_order()
sub_expr12 = [ExprRange(sub_expr2, Output(state = ScalarMult(frac(one, sqrt(two)), VecAdd(ket0, ScalarMult(Exp(e, Mult(two, pi, i, Exp(two, Neg(sub_expr2)), _phase)), ket1)))), sub_expr7, zero).with_decreasing_order(), ExprRange(sub_expr2, MultiQubitElem(element = Output(state = _ket_u, part = sub_expr2), targets = sub_expr6), one, _s)]
expr = Implies(QcircuitEquiv(Qcircuit(vert_expr_array = VertExprArray(sub_expr11)), Qcircuit(vert_expr_array = VertExprArray(sub_expr9))), QcircuitEquiv(Qcircuit(vert_expr_array = VertExprArray(sub_expr10, sub_expr11, sub_expr12)), Qcircuit(vert_expr_array = VertExprArray(sub_expr10, sub_expr9, sub_expr12))).with_wrapping_at(1)).with_wrapping_at(2)

# 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(\left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qw \\
& \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qw \\
& \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qw \\
& \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qw \\
& \gate{U^{2^{t - 1}}} & \gate{U^{2^{t - 2}}} & \gate{\cdots} & \gate{U^{2^{0}}} & { /^{s} } \qw
} \end{array}\right) \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
& \multigate{1}{\textrm{QPE}_1\left(U, t\right)} & { /^{t} } \qw \\
& \ghost{\textrm{QPE}_1\left(U, t\right)} & { /^{s} } \qw
} \end{array}\right)\right) \Rightarrow  \\ \left(\begin{array}{c} \begin{array}{l} \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \control{} \qw \qwx[1] & \qw & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 1} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \control{} \qw \qwx[1] & \gate{\cdots} \qwx[1] & \qw & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 2} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \gate{\vdots} \qwx[1] & \gate{\vdots} \qwx[1] & \gate{\ddots} \qwx[1] & \gate{\vdots} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \qw \qwx[1] & \qw \qwx[1] & \gate{\cdots} \qwx[1] & \control{} \qw \qwx[1] & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{0} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \gate{U^{2^{t - 1}}} & \gate{U^{2^{t - 2}}} & \gate{\cdots} & \gate{U^{2^{0}}} & \qout{\lvert u \rangle}
} \end{array}\right) \\  \cong \left(\begin{array}{c} \Qcircuit@C=1em @R=.7em{
\qin{\lvert + \rangle} & \multigate{4}{\textrm{QPE}_1\left(U, t\right)} & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 1} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{t - 2} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\begin{array}{c}:\\ \left(t - 3\right) \times \\:\end{array}} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \qout{\vdots} \\
\qin{\lvert + \rangle} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \qout{\frac{1}{\sqrt{2}} \cdot \left(\lvert 0 \rangle + \left(\mathsf{e}^{2 \cdot \pi \cdot \mathsf{i} \cdot 2^{0} \cdot \varphi} \cdot \lvert 1 \rangle\right)\right)} \\
\qin{\lvert u \rangle} & \ghost{\textrm{QPE}_1\left(U, t\right)} & \qout{\lvert u \rangle}
} \end{array}\right) \end{array} \end{array}\right) \end{array} \end{array}

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

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

Expression of type Implies¶

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

Expression of type Implies ¶

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