Expression of type Forall

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, Variable, VertExprArray, a, b
from proveit.logic import Forall, NotEquals
from proveit.numbers import Add, Interval, one
from proveit.physics.quantum import NumKet, Z, ket_plus
from proveit.physics.quantum.QPE import QPE, _U, _ket_u, _m_domain, _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 = 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))

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

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

stored_expr.style_options()

name	description	default	current value	related methods
with_wrapping	If 'True', wrap the Expression after the parameters	None	None/False	('with_wrapping',)
condition_wrapping	Wrap 'before' or 'after' the condition (or None).	None	None/False	('with_wrap_after_condition', 'with_wrap_before_condition')
wrap_params	If 'True', wraps every two parameters AND wraps the Expression after the parameters	None	None/False	('with_params',)
justification	justify to the 'left', 'center', or 'right' in the array cells	center	center	('with_justification',)

# display the expression information
stored_expr.expr_info()

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