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 MatrixProd, 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, ket1
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, ket1)
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(MatrixProd(U, 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 1 \rangle} & \qw & \control \qw \qwx[1] & \rstick{\alpha \thinspace \lvert 1 \rangle} \qw   \\ 
  & \lstick{x} & { /^{n} } \qw & \gate{U} & \rstick{U \thinspace 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: 66
body: 3
3Conditionalvalue: 4
condition: 5
4Operationoperator: 23
operand: 8
5Operationoperator: 37
operands: 7
6ExprTuple8
7ExprTuple66, 9
8Lambdaparameter: 78
body: 10
9Literal
10Conditionalvalue: 11
condition: 12
11Operationoperator: 23
operand: 15
12Operationoperator: 37
operands: 14
13ExprTuple15
14ExprTuple78, 16
15Lambdaparameter: 79
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
25ExprTuple79, 28
26ExprTuple77, 66
27Lambdaparameter: 75
body: 29
28Operationoperator: 30
operands: 31
29Conditionalvalue: 32
condition: 33
30Literal
31ExprTuple34, 66
32Operationoperator: 35
operand: 40
33Operationoperator: 37
operands: 38
34ExprTuple39
35Literal
36ExprTuple40None
37Literal
38ExprTuple75, 45
39Operationoperator: 41
operands: 42
40ExprTuple43, 44None
41Literal
42ExprTuple45, 77
43ExprTuple46, 47, 48, 49
44ExprTuple50, 51, 52, 53
45Literal
46Operationoperator: 56
operand: 65
47Literal
48Operationoperator: 60
operands: 54
49Operationoperator: 62
operand: 65
50Operationoperator: 56
operand: 79
51Operationoperator: 58
operand: 66
52Operationoperator: 60
operands: 61
53Operationoperator: 62
operand: 68
54ExprTuple64, 67
55ExprTuple65
56Literal
57ExprTuple79
58Literal
59ExprTuple66
60Literal
61ExprTuple78, 67
62Literal
63ExprTuple68
64Literal
65Operationoperator: 69
operands: 70
66Variable
67Operationoperator: 71
operands: 72
68Operationoperator: 73
operands: 74
69Literal
70ExprTuple75, 76
71Literal
72ExprTuple82, 77
73Literal
74ExprTuple78, 79
75Variable
76Operationoperator: 80
operand: 82
77Literal
78Variable
79Variable
80Literal
81ExprTuple82
82Literal