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, n, x, y
from proveit.linalg import SU, TensorExp
from proveit.linear_algebra import MatrixProd
from proveit.logic import Equals, Forall, Iff
from proveit.numbers import Exp, NaturalPos, two
from proveit.physics.quantum import Gate, Input, Output, QubitSpace
from proveit.physics.quantum.circuit import Circuit, MultiWire
In [2]:
# build up the expression from sub-expressions
expr = Forall([n], Forall([U], Forall([x, y], Iff(Circuit(ExprArray([Input(x), MultiWire(n), Gate(U), Output(y)])), Equals(y, MatrixProd(U, x))), 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, y \in \left(\mathbb{C}^{2}\right)^{\otimes n}}~\left(\hspace{2em} \Qcircuit@C=1em @R=.7em{
& \lstick{x} & { /^{n} } \qw & \gate{U} & \rstick{y} \qw 
} \hspace{2em} \Leftrightarrow \left(y = \left(U \thinspace x\right)\right)\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: 13
operand: 2
1ExprTuple2
2Lambdaparameter: 64
body: 3
3Conditionalvalue: 4
condition: 5
4Operationoperator: 13
operand: 8
5Operationoperator: 39
operands: 7
6ExprTuple8
7ExprTuple64, 9
8Lambdaparameter: 65
body: 10
9Literal
10Conditionalvalue: 11
condition: 12
11Operationoperator: 13
operand: 16
12Operationoperator: 39
operands: 15
13Literal
14ExprTuple16
15ExprTuple65, 17
16Lambdaparameters: 18
body: 19
17Operationoperator: 20
operand: 24
18ExprTuple63, 66
19Conditionalvalue: 22
condition: 23
20Literal
21ExprTuple24
22Operationoperator: 25
operands: 26
23Operationoperator: 27
operands: 28
24Operationoperator: 67
operands: 29
25Literal
26ExprTuple30, 31
27Literal
28ExprTuple32, 33
29ExprTuple70, 64
30Operationoperator: 34
operand: 41
31Operationoperator: 36
operands: 37
32Operationoperator: 39
operands: 38
33Operationoperator: 39
operands: 40
34Literal
35ExprTuple41None
36Literal
37ExprTuple66, 42
38ExprTuple63, 43
39Literal
40ExprTuple66, 43
41ExprTuple44None
42Operationoperator: 45
operands: 46
43Operationoperator: 47
operands: 48
44ExprTuple49, 50, 51, 52
45Literal
46ExprTuple65, 63
47Literal
48ExprTuple53, 64
49Operationoperator: 54
operand: 63
50Operationoperator: 56
operand: 64
51Operationoperator: 58
operand: 65
52Operationoperator: 60
operand: 66
53ExprTuple62
54Literal
55ExprTuple63
56Literal
57ExprTuple64
58Literal
59ExprTuple65
60Literal
61ExprTuple66
62Operationoperator: 67
operands: 68
63Variable
64Variable
65Variable
66Variable
67Literal
68ExprTuple69, 70
69Literal
70Literal