logo

Expression of type Forall

from the theory of proveit.physics.quantum

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, U, alpha, n, x
from proveit.linalg import TensorExp
from proveit.linear_algebra import SU, ScalarProd
from proveit.logic import Forall, Set
from proveit.numbers import Complex, Exp, NaturalPos, one, two
from proveit.physics.quantum import CONTROL, I, Input, Output, QubitSpace, ket0
from proveit.physics.quantum.circuit import Circuit, MultiQubitGate, MultiWire
In [2]:
# build up the expression from sub-expressions
sub_expr1 = Set(one, two)
sub_expr2 = ScalarProd(alpha, ket0)
expr = Forall([n], Forall([U], Forall([x], Forall([alpha], Circuit(ExprArray([Input(sub_expr2), I, MultiQubitGate(CONTROL, sub_expr1), Output(sub_expr2)], [Input(x), MultiWire(n), MultiQubitGate(U, sub_expr1), Output(x)])), domain = Complex), domain = TensorExp([QubitSpace], n)), domain = SU(Exp(two, n))), 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_{n \in \mathbb{N}^+}~\left[\forall_{U \in SU(2^{n})}~\left[\forall_{x \in \left(\mathbb{C}^{2}\right)^{\otimes n}}~\left[\forall_{\alpha \in \mathbb{C}}~\hspace{2em} \Qcircuit@C=1em @R=.7em{
& \lstick{\alpha \thinspace \lvert 0 \rangle} & \qw & \control \qw \qwx[1] & \rstick{\alpha \thinspace \lvert 0 \rangle} \qw   \\ 
  & \lstick{x} & { /^{n} } \qw & \gate{U} & \rstick{x} \qw 
} \hspace{2em}\right]\right]\right]
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: 23
operand: 2
1ExprTuple2
2Lambdaparameter: 65
body: 3
3Conditionalvalue: 4
condition: 5
4Operationoperator: 23
operand: 8
5Operationoperator: 37
operands: 7
6ExprTuple8
7ExprTuple65, 9
8Lambdaparameter: 66
body: 10
9Literal
10Conditionalvalue: 11
condition: 12
11Operationoperator: 23
operand: 15
12Operationoperator: 37
operands: 14
13ExprTuple15
14ExprTuple66, 16
15Lambdaparameter: 68
body: 17
16Operationoperator: 18
operand: 22
17Conditionalvalue: 20
condition: 21
18Literal
19ExprTuple22
20Operationoperator: 23
operand: 27
21Operationoperator: 37
operands: 25
22Operationoperator: 41
operands: 26
23Literal
24ExprTuple27
25ExprTuple68, 28
26ExprTuple76, 65
27Lambdaparameter: 73
body: 29
28Operationoperator: 30
operands: 31
29Conditionalvalue: 32
condition: 33
30Literal
31ExprTuple34, 65
32Operationoperator: 35
operand: 40
33Operationoperator: 37
operands: 38
34ExprTuple39
35Literal
36ExprTuple40None
37Literal
38ExprTuple73, 45
39Operationoperator: 41
operands: 42
40ExprTuple43, 44None
41Literal
42ExprTuple45, 76
43ExprTuple46, 47, 48, 49
44ExprTuple50, 51, 52, 53
45Literal
46Operationoperator: 56
operand: 64
47Literal
48Operationoperator: 59
operands: 54
49Operationoperator: 61
operand: 64
50Operationoperator: 56
operand: 68
51Operationoperator: 57
operand: 65
52Operationoperator: 59
operands: 60
53Operationoperator: 61
operand: 68
54ExprTuple63, 67
55ExprTuple64
56Literal
57Literal
58ExprTuple65
59Literal
60ExprTuple66, 67
61Literal
62ExprTuple68
63Literal
64Operationoperator: 69
operands: 70
65Variable
66Variable
67Operationoperator: 71
operands: 72
68Variable
69Literal
70ExprTuple73, 74
71Literal
72ExprTuple75, 76
73Variable
74Operationoperator: 77
operand: 79
75Literal
76Literal
77Literal
78ExprTuple79
79Literal