logo

Expression of type Forall

from the theory of proveit.physics.quantum.QPE

In [1]:
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 ExprArray, k
from proveit.logic import Forall, Set
from proveit.numbers import NaturalPos, one, three, two
from proveit.physics.quantum import CONTROL, Hgate, Input, Ket, Output, SPACE, ket0
from proveit.physics.quantum.QPE import U_pow_two_pow_k, psi_k, psi_next, u_
from proveit.physics.quantum.circuit import Circuit, IdentityOp, MultiQubitGate
In [2]:
# build up the expression from sub-expressions
sub_expr1 = Set(two, three)
sub_expr2 = Ket(u_)
sub_expr3 = MultiQubitGate(IdentityOp(), Set(one, two))
expr = Forall([k], Circuit(ExprArray([Input(Ket(psi_k)), IdentityOp(), IdentityOp(), sub_expr3, SPACE, SPACE], [Input(ket0), Hgate, MultiQubitGate(CONTROL, sub_expr1), sub_expr3, IdentityOp(), Output(Ket(psi_next))], [Input(sub_expr2), IdentityOp(), MultiQubitGate(U_pow_two_pow_k, sub_expr1), Output(sub_expr2), SPACE, SPACE])), domain = NaturalPos)
Out[2]:
expr:
In [3]:
# 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
In [4]:
# Show the LaTeX representation of the expression for convenience if you need it.
print(expr.latex())
\forall_{k \in \mathbb{N}^+}~\hspace{2em} \Qcircuit@C=1em @R=.7em{
& \lstick{\lvert \psi_{k} \rangle} & \qw & \qw & \qw \qwx[1]   \\ 
  & \lstick{\lvert 0 \rangle} & \gate{H} & \control \qw \qwx[1] & \qw & \qw & \rstick{\lvert \psi_{k + 1} \rangle} \qw   \\ 
  & \lstick{\lvert u \rangle} & \qw & \gate{U^{2^{k}}} & \rstick{\lvert u \rangle} \qw 
} \hspace{2em}
In [5]:
expr.style_options()
Out[5]:
namedescriptiondefaultcurrent valuerelated methods
with_wrappingIf 'True', wrap the Expression after the parametersNoneNone/False('with_wrapping',)
wrap_paramsIf 'True', wraps every two parameters AND wraps the Expression after the parametersNoneNone/False('with_params',)
justificationjustify to the 'left', 'center', or 'right' in the array cellscentercenter('with_justification',)
In [6]:
# display the expression information
expr.expr_info()
Out[6]:
 core typesub-expressionsexpression
0Operationoperator: 1
operand: 3
1Literal
2ExprTuple3
3Lambdaparameter: 74
body: 4
4Conditionalvalue: 5
condition: 6
5Operationoperator: 7
operand: 11
6Operationoperator: 9
operands: 10
7Literal
8ExprTuple11None
9Literal
10ExprTuple74, 12
11ExprTuple13, 14, 15None
12Literal
13ExprTuple16, 42, 42, 20, 25, 25
14ExprTuple17, 18, 19, 20, 42, 21
15ExprTuple22, 42, 23, 24, 25, 25
16Operationoperator: 33
operand: 38
17Operationoperator: 33
operand: 39
18Operationoperator: 28
operand: 40
19Operationoperator: 34
operands: 30
20Operationoperator: 34
operands: 31
21Operationoperator: 36
operand: 44
22Operationoperator: 33
operand: 47
23Operationoperator: 34
operands: 35
24Operationoperator: 36
operand: 47
25Literal
26ExprTuple38
27ExprTuple39
28Literal
29ExprTuple40
30ExprTuple41, 46
31ExprTuple42, 43
32ExprTuple44
33Literal
34Literal
35ExprTuple45, 46
36Literal
37ExprTuple47
38Operationoperator: 55
operand: 57
39Operationoperator: 55
operand: 58
40Literal
41Literal
42Literal
43Operationoperator: 53
operands: 50
44Operationoperator: 55
operand: 59
45Operationoperator: 67
operands: 52
46Operationoperator: 53
operands: 54
47Operationoperator: 55
operand: 63
48ExprTuple57
49ExprTuple58
50ExprTuple75, 71
51ExprTuple59
52ExprTuple60, 61
53Literal
54ExprTuple71, 62
55Literal
56ExprTuple63
57Operationoperator: 65
operands: 64
58Literal
59Operationoperator: 65
operands: 66
60Literal
61Operationoperator: 67
operands: 68
62Literal
63Literal
64ExprTuple69, 74
65Literal
66ExprTuple69, 70
67Literal
68ExprTuple71, 74
69Literal
70Operationoperator: 72
operands: 73
71Literal
72Literal
73ExprTuple74, 75
74Variable
75Literal