About CoqQ
Framework for foundational verification of quantum programs in Coq. Provides deeply embedded quantum programming language qwhile, labelled Dirac notation, and verified quantum Hoare logic. Case studies include HHL, Grover, QPE, and QFT.
Proof Assistant and Foundation
| Aspect | CoqQ | Fanal |
|---|---|---|
| Proof assistant | Coq | Lean 4 |
| Math library | MathComp + MathComp Analysis + ~22K LOC custom extensions | Mathlib (community-maintained, existing infrastructure) |
| Type theory | CIC (Calculus of Inductive Constructions) | CIC variant (Lean 4 kernel) |
| Codebase size | ~33,000 lines Coq (spec + proof + comments) | Under active development |
| Foundedness | Fully foundational: all proof rules proved as lemmas w.r.t. denotational semantics | Foundational for Dirac notation; program logic planned |
Quantum State Representation
| Aspect | CoqQ | Fanal |
|---|---|---|
| Approach | Abstract linear algebra (Hilbert spaces via MathComp) | Concrete matrices over C (via Mathlib Matrix) |
| State type | Density operators in D^1(H), operators in L(H1, H2) | Matrix (ketType.interp) (braType.interp) C |
| Tensor products | Big operators (bigotimes) with commutative monoid structure | tsr constructor + bigTsr for parametric tensor products |
| Type hierarchy | HermType, PsdType, DenType, ObsType, UnitaryType, ProjType via canonical structures | Operator predicates (IsHermitian, IsUnitary, IsProjection) defined semantically |
| Algebraic properties | Automatically inherited from MathComp abstract algebra | Requires explicit proofs; amenable to native_decide for small cases |
Label System
| Aspect | CoqQ | Fanal |
|---|---|---|
| Model | Flat set of labels: each label p maps to Hilbert space H_p | Hierarchical access paths: root variable + list of AccessSteps |
| Variables | vars T mapping to subset of labels, composition via [x1, x2] | LabelTerm inductive: var, tuple, tupleIdx, arrayIdx |
| Array support | n-tuple types with for-loop constructs | First-class DataType.array n t with arrayIdx and bigTsr |
| Disjointness | Static set intersection = empty | Dynamic runtime atom overlap check |
| Cylindrical extension | cl_T(A_S) = A_S tensor I_{T\S} lifts local operators | Access path model with RegAtom lists and dimValAppendEquiv |
Type System
| Aspect | CoqQ | Fanal |
|---|---|---|
| Approach | Shallow embedding: Coq types + canonical structures for automatic inference | Deep embedding: explicit DataType, DiracSort, UnifiedContext, DTIso |
| Data types | Coq finite types {t_1, t_2, ...} | DataType inductive: fin n | tuple ts | array n t |
| Type isomorphism | Handled implicitly by canonical structures | DTIso: structural isomorphism (unit elimination, tuple flattening) |
| Inference | Coq's elaboration with canonical structure resolution | Deterministic, decidable synthesizeType functions |
| Semantic equality | Matrix equality via MathComp | SemEq (same-sort) and HSemEq (cross-sort via SortIso) |
Dirac Notation
| Aspect | CoqQ | Fanal |
|---|---|---|
| Architecture | Single integrated labelled Dirac notation layer | Two layers: plain Dirac (DiracTerm) + labelled Dirac (LDiracTerm) |
| Notation elements | Kets |t>_S, bras <t|_S, inner/outer products, tensor products | Full AST: cpx, ket, bra, delta, add, neg, sca, mul, tsr, adj, smul, bigSum, bigTsr, dVar |
| Labelling | Implicit via disjoint labels with automatic lifting | Explicit register patterns via label constructor with ket/bra patterns |
| Big tensor product | No direct constructor; handled via for-loops in program language | First-class bigTsr constructor for parametric tensor products |
| Equational reasoning | Basic rewriting with linearity, associativity, commutativity | Certified dirac_eq tactic based on term rewriting with soundness proofs |
Program Logic
| Aspect | CoqQ | Fanal |
|---|---|---|
| Status | Complete, verified quantum Hoare logic for qwhile | Planned (roadmap item D) |
| Judgments | {A_S1} C {B_S2} with total and partial correctness | Planned: Hoare logic over labelled Dirac assertions |
| Proof rules | ~30 rules: syntax-directed, structural, state-based, R.Inner | Planned: syntax-directed + structural rules |
| Soundness | Proved from first principles (Theorem 6.1) | Will be proved foundationally in Lean |
| Weakest precondition | Existence and characterization proved | Planned |
Automation
| Aspect | CoqQ | Fanal |
|---|---|---|
| Type inference | Canonical structures for automatic Hilbert space resolution | synthesizeType functions producing typing derivations |
| Equational reasoning | Manual proof assembly from lemmas; no dedicated decision procedure | dirac_eq tactic: push-button certified equational reasoning |
| Parsing | Coq notations | Lean 4 macro-based parsing syntax for natural Dirac encoding |
| D-Hammer | Not available | Planned integration of D-Hammer decision procedure |
Expressiveness
| Aspect | CoqQ | Fanal |
|---|---|---|
| Fixed-size tuples | x : vars (T1 * T2) | tuple [r1, r2] |
| Parametric n-tuples | x : n.-tuple (vars T) with for-loops | arrayIdx r idx with bigTsr |
| Array indexing | x_i via tuple projection | r[i] via arrayIdx with classical expression index |
| Classical expressions | Coq native types (full dependent types) | CExprTerm AST: arithmetic, booleans, comparisons, casting |
| Classical variables | Not supported (acknowledged as future work) | Built-in eVar with UnifiedContext |
| Programs | qwhile: skip, abort, sequence, init, unitary, if-meas, while, for | Planned: classical-quantum language with full control flow |
Case Studies
| Aspect | CoqQ | Fanal |
|---|---|---|
| Hidden Subgroup Problem | Verified (~390 lines) — first-ever formalization | Not yet |
| HHL algorithm | Verified (~280 lines) | Not yet |
| Grover's search | Verified (~180 lines) | Not yet |
| QPE | Verified (~90 lines) | Not yet |
| QFT | Verified (~140 lines) | Not yet |
| Dirac identities | Used in proofs but not isolated | Encoded and verified (QCQI examples, Pauli identities, circuit equivalences) |
Summary: Key Differences
| Aspect | CoqQ | Fanal |
|---|---|---|
| Proof System | Coq (Calculus of Constructions) | Lean 4 (CIC with quotients) |
| Math Library | MathComp (SSReflect style) | Mathlib (tactic style) |
| Register Model | Flat labelled qubits | Hierarchical access paths with value-dependent labels |
| Automation | Manual Coq tactics | dirac_eq tactic + D-Hammer integration |
| Development | Traditional manual development | AI-native, specification-driven workflow |