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, U, Variable, VertExprArray, s, t
from proveit.linear_algebra import Unitary
from proveit.logic import Forall
from proveit.numbers import Add, Exp, Interval, one, two
from proveit.physics.quantum.QPE import QPE1, QPE1_U_t_circuit
from proveit.physics.quantum.circuits import Gate, MultiQubitElem, Qcircuit, QcircuitEquiv

# build up the expression from sub-expressions
sub_expr1 = Variable("_a", latex_format = r"{_{-}a}")
sub_expr2 = Add(t, s)
sub_expr3 = MultiQubitElem(element = Gate(operation = QPE1(U, t), part = sub_expr1), targets = Interval(one, sub_expr2))
expr = Forall(instance_param_or_params = [U], instance_expr = QcircuitEquiv(Qcircuit(vert_expr_array = VertExprArray([ExprRange(sub_expr1, sub_expr3, one, t), ExprRange(sub_expr1, sub_expr3, Add(t, one), sub_expr2)])), QPE1_U_t_circuit), domain = Unitary(Exp(two, s)))

# 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_{U \in \textrm{U}\left(2^{s}\right)}~\left(\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) \cong \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)\right)

stored_expr.style_options()

# display the expression information
stored_expr.expr_info()

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',)

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

Expression of type Forall¶

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

Expression of type Forall ¶

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