Axioms for the theory of proveit.physics.quantum.circuits

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 k, l, A, B, S
from proveit.logic import Forall, Equals
from proveit.numbers import one, NaturalPos
from proveit.core_expr_types.expr_arrays import (
    A11_to_Akl, B11_to_Bkl, A11_to_Akl_varray, B11_to_Bkl_varray)
from proveit.physics.quantum.circuits import (
    Input, Output, Measure, Gate, MultiQubitElem)
from proveit.physics.quantum.circuits import circuit_Akl, circuit_Bkl 

%begin axioms

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

Quantum circuits of the same dimension are equal if and only if their contents are equal.

qcircuit_eq_def = Forall(
    (k, l), Forall(
        (A11_to_Akl, B11_to_Bkl),
        Equals(Equals(circuit_Akl, circuit_Bkl),
               Equals(A11_to_Akl_varray, B11_to_Bkl_varray))
        .with_wrap_after_operator()).with_wrapping(),
    domain=NaturalPos)

qcircuit_eq_def:

Quantum circuit inputs/outputs are equal only when their output states are equal

qcircuit_input_eq_def = Forall(
    (A, B), Equals(Equals(Input(A), Input(B)),
                   Equals(A, B)))

qcircuit_input_eq_def:

qcircuit_output_eq_def = Forall(
    (A, B), Equals(Equals(Output(A), Output(B)),
                   Equals(A, B)))

qcircuit_output_eq_def:

qcircuit_input_part_eq_def = Forall(
    k, Forall(
        (A, B, S), Equals(Equals(MultiQubitElem(Input(A, part=k),
                                                targets=S),
                                 MultiQubitElem(Input(B, part=k),
                                                targets=S)),
                          Equals(A, B))),
    domain=NaturalPos)

qcircuit_input_part_eq_def:

qcircuit_output_part_eq_def = Forall(
    k, Forall(
        (A, B, S), Equals(Equals(MultiQubitElem(Output(A, part=k),
                                                targets=S),
                                 MultiQubitElem(Output(B, part=k),
                                                targets=S)),
                          Equals(A, B))),
    domain=NaturalPos)

qcircuit_output_part_eq_def:

%end axioms

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