This type lists the allowed alternatives for “reversible gate”; its constructors are the cases that downstream code must handle.
inductive ReversibleGate (qubits : Nat) where
| x (target : Fin qubits)
| cx (control target : Fin qubits) (distinct : control ≠ target)
| ccx (control0 control1 target : Fin qubits)
(c0_ne_c1 : control0 ≠ control1)
(c0_ne_target : control0 ≠ target)
(c1_ne_target : control1 ≠ target)
commit-pinned source · Verso Blueprint panel
This abbreviation gives a shorter name to the type or expression used for “reversible program”.
abbrev ReversibleProgram (qubits : Nat) := List (ReversibleGate qubits)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “ccx basis action”.
def ccxBasisAction {qubits : Nat} (control0 control1 target : Fin qubits)
(state : PrimitiveBasis qubits) : PrimitiveBasis qubits :=
if state control0 = 1 ∧ state control1 = 1 then
xBasisAction target state
else state
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “ccx basis action involutive”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem ccxBasisAction_involutive {qubits : Nat}
(control0 control1 target : Fin qubits)
(c0_ne_target : control0 ≠ target)
(c1_ne_target : control1 ≠ target) :
Function.Involutive (ccxBasisAction control0 control1 target) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “ccx basis equiv”.
def ccxBasisEquiv {qubits : Nat} (control0 control1 target : Fin qubits)
(c0_ne_target : control0 ≠ target)
(c1_ne_target : control1 ≠ target) :
PrimitiveBasis qubits ≃ PrimitiveBasis qubits where
toFun := ccxBasisAction control0 control1 target
invFun := ccxBasisAction control0 control1 target
left_inv := ccxBasisAction_involutive control0 control1 target
c0_ne_target c1_ne_target
right_inv := ccxBasisAction_involutive control0 control1 target
c0_ne_target c1_ne_target
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “eval reversible gate”.
def evalReversibleGate {qubits : Nat} : ReversibleGate qubits →
PrimitiveBasis qubits ≃ PrimitiveBasis qubits
| .x target => xBasisEquiv target
| .cx control target distinct => cxBasisEquiv control target distinct
| .ccx control0 control1 target _ c0_ne_target c1_ne_target =>
ccxBasisEquiv control0 control1 target c0_ne_target c1_ne_target
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “eval reversible program”.
def evalReversibleProgram {qubits : Nat} : ReversibleProgram qubits →
PrimitiveBasis qubits ≃ PrimitiveBasis qubits
| [] => Equiv.refl _
| gate :: rest => (evalReversibleGate gate).trans (evalReversibleProgram rest)
commit-pinned source · Verso Blueprint panel