This type lists the allowed alternatives for “exact angle”; its constructors are the cases that downstream code must handle.
inductive ExactAngle where
| rational (value : Rat)
| piRational (value : Rat)
| twiceArccosRational (value : Rat)
(bounded : |(value : Real)| ≤ 1)
| twiceArccosSqrtRational (value : Rat)
(bounded : 0 ≤ (value : Real) ∧ (value : Real) ≤ 1)
/-- An exact real angle in the mathematical circuit. This constructor does
not promise a computable decimal export; exporters must supply and audit
their own numerical evaluation of the defining real expression. -/
| real (value : Real)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “eval”.
noncomputable def eval : ExactAngle → Real
| .rational value => (value : Real)
| .piRational value => Real.pi * (value : Real)
| .twiceArccosRational value _ => 2 * Real.arccos (value : Real)
| .twiceArccosSqrtRational value _ =>
2 * Real.arccos (Real.sqrt (value : Real))
| .real value => value
| .add left right => left.eval + right.eval
| .neg value => -value.eval
| .scale factor value => (factor : Real) * value.eval
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval add”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem eval_add (left right : ExactAngle) :
(add left right).eval = left.eval + right.eval := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval neg”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem eval_neg (value : ExactAngle) :
(neg value).eval = -value.eval := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval scale”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem eval_scale (factor : Rat) (value : ExactAngle) :
(scale factor value).eval = (factor : Real) * value.eval := rfl
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “sub”.
def sub (left right : ExactAngle) : ExactAngle :=
add left (neg right)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “half add”.
def halfAdd (left right : ExactAngle) : ExactAngle :=
scale (1 / 2) (add left right)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “half sub”.
def halfSub (left right : ExactAngle) : ExactAngle :=
scale (1 / 2) (sub left right)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval sub”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem eval_sub (left right : ExactAngle) :
(sub left right).eval = left.eval - right.eval := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval half add”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem eval_half_add (left right : ExactAngle) :
(halfAdd left right).eval = (left.eval + right.eval) / 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval half sub”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem eval_half_sub (left right : ExactAngle) :
(halfSub left right).eval = (left.eval - right.eval) / 2 := by
commit-pinned source · Verso Blueprint panel
This type lists the allowed alternatives for “primitive gate”; its constructors are the cases that downstream code must handle.
inductive PrimitiveGate (qubits : Nat) where
| x (target : Fin qubits)
| ry (target : Fin qubits) (angle : ExactAngle)
| rz (target : Fin qubits) (angle : ExactAngle)
| cx (control target : Fin qubits) (distinct : control ≠ target)
commit-pinned source · Verso Blueprint panel
This abbreviation gives a shorter name to the type or expression used for “primitive circuit”.
abbrev PrimitiveCircuit (qubits : Nat) := List (PrimitiveGate qubits)
/-- A primitive circuit together with an exact global phase. -/
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “primitive program”. A proposition-valued field is a requirement until a constructor supplies it. A primitive circuit together with an exact global phase.
structure PrimitiveProgram (qubits : Nat) where
circuit : PrimitiveCircuit qubits
globalPhase : ExactAngle
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “dagger”.
def dagger {qubits : Nat} : PrimitiveGate qubits → PrimitiveGate qubits
| .x target => .x target
| .ry target angle => .ry target (.neg angle)
| .rz target angle => .rz target (.neg angle)
| .cx control target distinct => .cx control target distinct
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “touched”.
def touched {qubits : Nat} : PrimitiveGate qubits → Finset (Fin qubits)
| .x target | .ry target _ | .rz target _ => {target}
| .cx control target _ => {control, target}
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “one qubit count”.
def oneQubitCount {qubits : Nat} : PrimitiveGate qubits → Nat
| .x _ | .ry _ _ | .rz _ _ => 1
| .cx _ _ _ => 0
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “two qubit count”.
def twoQubitCount {qubits : Nat} : PrimitiveGate qubits → Nat
| .cx _ _ _ => 1
| _ => 0
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “gate count”.
def gateCount {qubits : Nat} (circuit : PrimitiveCircuit qubits) : Nat :=
circuit.length
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “one qubit count”.
def oneQubitCount {qubits : Nat} (circuit : PrimitiveCircuit qubits) : Nat :=
circuit.foldl (fun total gate => total + gate.oneQubitCount) 0
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “two qubit count”.
def twoQubitCount {qubits : Nat} (circuit : PrimitiveCircuit qubits) : Nat :=
circuit.foldl (fun total gate => total + gate.twoQubitCount) 0
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “ry count”.
def ryCount {qubits : Nat} (circuit : PrimitiveCircuit qubits) : Nat :=
circuit.countP fun gate => match gate with
| .ry _ _ => true
| _ => false
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “cx count”.
def cxCount {qubits : Nat} (circuit : PrimitiveCircuit qubits) : Nat :=
circuit.countP fun gate => match gate with
| .cx _ _ _ => true
| _ => false
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “ry count append”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem ryCount_append {qubits : Nat}
(left right : PrimitiveCircuit qubits) :
(left ++ right).ryCount = left.ryCount + right.ryCount := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “cx count append”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem cxCount_append {qubits : Nat}
(left right : PrimitiveCircuit qubits) :
(left ++ right).cxCount = left.cxCount + right.cxCount := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “ry count singleton ry”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem ryCount_singleton_ry {qubits : Nat}
(target : Fin qubits) (angle : ExactAngle) :
ryCount ([PrimitiveGate.ry target angle] : PrimitiveCircuit qubits) = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “ry count singleton cx”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem ryCount_singleton_cx {qubits : Nat}
(control target : Fin qubits) (distinct : control ≠ target) :
ryCount ([PrimitiveGate.cx control target distinct] : PrimitiveCircuit qubits) = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “cx count singleton ry”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem cxCount_singleton_ry {qubits : Nat}
(target : Fin qubits) (angle : ExactAngle) :
cxCount ([PrimitiveGate.ry target angle] : PrimitiveCircuit qubits) = 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “cx count singleton cx”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem cxCount_singleton_cx {qubits : Nat}
(control target : Fin qubits) (distinct : control ≠ target) :
cxCount ([PrimitiveGate.cx control target distinct] : PrimitiveCircuit qubits) = 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “next wire depth”.
def nextWireDepth {qubits : Nat} (depth : Fin qubits → Nat)
(gate : PrimitiveGate qubits) : Fin qubits → Nat :=
let layer := gate.touched.sup depth
fun wire => if wire ∈ gate.touched then layer + 1 else depth wire
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “wire depths”.
def wireDepths {qubits : Nat} (circuit : PrimitiveCircuit qubits) :
Fin qubits → Nat :=
circuit.foldl nextWireDepth (fun _ => 0)
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “depth”.
def depth {qubits : Nat} (circuit : PrimitiveCircuit qubits) : Nat :=
Finset.univ.sup circuit.wireDepths
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “resource”.
def resource {qubits : Nat} (circuit : PrimitiveCircuit qubits) : Resource :=
Resource.ofCountsWithDepth circuit.oneQubitCount circuit.twoQubitCount
0 0 circuit.depth
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “gate count eq length”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem gateCount_eq_length {qubits : Nat}
(circuit : PrimitiveCircuit qubits) :
circuit.gateCount = circuit.length := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “resource oracle calls eq zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem resource_oracleCalls_eq_zero {qubits : Nat}
(circuit : PrimitiveCircuit qubits) :
circuit.resource.oracleCalls = 0 := rfl
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “identity”.
def identity (qubits : Nat) : PrimitiveProgram qubits where
circuit := []
globalPhase := .rational 0
/-- Execute `left`, then `right`, using chronological list semantics. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “seq”. Execute 'left', then 'right', using chronological list semantics.
def seq {qubits : Nat} (left right : PrimitiveProgram qubits) :
PrimitiveProgram qubits where
circuit := left.circuit ++ right.circuit
globalPhase := .add left.globalPhase right.globalPhase
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “dagger”.
def dagger {qubits : Nat} (program : PrimitiveProgram qubits) :
PrimitiveProgram qubits where
circuit := program.circuit.reverse.map PrimitiveGate.dagger
globalPhase := .neg program.globalPhase
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “resource”.
def resource {qubits : Nat} (program : PrimitiveProgram qubits) : Resource :=
program.circuit.resource
commit-pinned source · Verso Blueprint panel