Axioms for the theory of proveit.physics.quantum

import proveit
# Prepare this notebook for defining the axioms of a theory:
%axioms_notebook # Keep this at the top following 'import proveit'.
from proveit import (Operation, Function, Lambda, Conditional,
                     ExprArray, ExprTuple, Composition)
from proveit import (a, b, c, f, k, m, n, v, x, y, alpha, 
                     A, B, M, U, V, W, X, Y, Z, fx, fy)
from proveit.core_expr_types import A_1_to_m, B_1_to_m
from proveit.linear_algebra import (
    LinMap, VecSpaces, MatrixSpace, MatrixMult, TensorProd, ScalarMult)
from proveit.logic import (Iff, And, Or, Forall, Exists, Equals, 
                           InSet, Set, Union, SetOfAll, InClass)
from proveit.numbers import zero, one, two, frac, Integer, Natural, NaturalPos, Complex, Exp
from proveit.numbers import Add, Exp, Mult, sqrt, subtract, greater
from proveit.numbers.number_sets import Interval
from proveit.physics.quantum import (
    Ket, NumKet)
from proveit.physics.quantum.circuits import (Gate, QcircuitEquiv, Qcircuit,
                                              Input, Output)
# from proveit.physics.quantum import Bra, Ket, RegisterBra, Meas, MultiWire, Circuit
from proveit.physics.quantum import ket0, ket1, ket_plus, H, QubitSpace, RegisterSU, I, CONTROL
# from proveit.physics.quantum import I, X, Y, Z, RegisterSU
from proveit.physics.quantum import QubitRegisterSpace

%begin axioms

Defining axioms for theory 'proveit.physics.quantum'
Subsequent end-of-cell assignments will define axioms
%end_axioms will finalize the definitions

# scalar_id_for_ket = Forall(k,
#                            Equals(Mult(one, Ket(k)), Ket(k)),
#                            domain=Natural)

hadamard_on_zero = Equals(MatrixMult(H, ket0), ket_plus)

hadamard_on_zero:

substitution = Forall((f, x, y), QcircuitEquiv(fx, fy), conditions=QcircuitEquiv(x, y))

substitution:

And then we have several axioms involving the Circuit class, which class itself still needs updating
(in particular, the Circuit class needs an appropriate substitute for the ExpressionTensor class -- perhaps ExprArray).

# circuit_gate_application = Forall(
#     U, 
#     Forall((x, y),
#            Iff(Circuit(ExprArray(ExprTuple(Input(x), Gate(U), Output(y)))),
#                Equals(y, MatrixMult(U, x))),
#            domain=QubitSpace),
#     domain=SU(two))

# circuit_multi_gate_application = Forall(
#     n,
#     Forall(U,
#            Forall((x, y),
#                   Iff(Circuit(ExprArray(ExprTuple(Input(x), MultiWire(n), Gate(U), Output(y)))),
#                       Equals(y, MatrixMult(U, x))),
#                   domain=QubitRegisterSpace(n)),
#            domain=RegisterSU(n)),
#     domain=NaturalPos)

# zero_controlled_ngate = Forall(
#     n,
#     Forall(U,
#            Forall(x,
#                   Forall(alpha,
#                          Circuit(ExprArray(ExprTuple(Input(ScalarMult(alpha, ket0)),
#                                    I,
#                                    MultiQubitGate(CONTROL, Set(one, two)),
#                                    Output(ScalarMult(alpha, ket0))),
#                                   ExprTuple(Input(x), MultiWire(n), MultiQubitGate(U, Set(one, two)), Output(x)))),
#                          domain=Complex),
#                   domain=QubitRegisterSpace(n)),
#            domain=SU(Exp(two, n))),
#     domain=NaturalPos)

# one_controlled_ngate = Forall(
#     n,
#     Forall(U,
#            Forall(x,
#                   Forall(alpha,
#                          Circuit(ExprArray(ExprTuple(Input(ScalarMult(alpha, ket1)),
#                                    I,
#                                    MultiQubitGate(CONTROL, Set(one, two)),
#                                    Output(ScalarMult(alpha, ket1))),
#                                   ExprTuple(Input(x), MultiWire(n), MultiQubitGate(U, Set(one, two)), Output(MatrixMult(U, x))))),
#                          domain=Complex),
#                   domain=QubitRegisterSpace(n)),
#            domain=SU(Exp(two, n))),
#     domain=NaturalPos)

%end axioms

These axioms may now be imported from the theory package: proveit.physics.quantum