About D-Hammer
Automated decision procedure for labelled Dirac notation equalities. Unverified C++/Mathematica tool. Handles 158 CoqQ examples. From the same research group as Fanal.
Relationship and Origin
| Aspect | D-Hammer | Fanal |
|---|---|---|
| Research group | BASICS Lab (Yingte Xu, lead author) | BASICS Lab (Yingte Xu, lead developer) |
| Role | Provides the automation algorithm | Provides the foundational semantics and kernel-checked proofs |
| Integration | Vendored inside Fanal at extern/D-Hammer/ | Roadmap item B.1: port D-Hammer's algorithm as certified tactics |
| Complementarity | Efficient but unverified decision procedure | Verified foundational framework incorporating D-Hammer's algorithms |
Normalization Pipeline
| Aspect | D-Hammer | Fanal |
|---|---|---|
| Step 1 | Rule-based term rewriting (expand definitions, simplify) | Certified rewrite rules in Supportive/Dirac/EqAxioms.lean |
| Step 2 | Variable expansion (abstract -> element-wise via sum_i) | Corresponding expansions with soundness proofs |
| Step 3 | Rule-based rewriting modulo axiom set R | Term rewriting framework in Supportive/Dirac/Rewrite.lean |
| Step 4 | AC normalization (sorting operands of +, * on scalars) | Variadic add/smul with list-based representation |
| Step 5 | Swapping successive summations (SUM-SWAP normalization) | bigSum handling in dirac_eq tactic |
| Step 6 | De Bruijn indices for alpha-equivalence | Named bound variables; alpha-equivalence handling planned |
Type System Correspondence
| Aspect | D-Hammer | Fanal |
|---|---|---|
| Index types | sigma ::= x | sigma1 x sigma2 (variable or product) | DataType inductive: fin n | tuple ts | array n t |
| Term types | Basis(sigma), S, K(sigma), B(sigma), O(sigma1,sigma2), forall x.T | DiracSort: scalar, ket alpha, bra alpha, oper alpha beta |
| Dependent types | First-class forall x : Index. T in object language | Lean's native dependent types; no object-level forall needed |
| Higher-order | Lambda abstractions in the object language | Lean's native functions; bigSum uses bound variables |
| AC symbols | ADDS, MULS with indefinite arity, flattened/sorted | DiracTerm.add (variadic list), DiracTerm.smul (variadic list) |
| Register types | Reg(sigma) with R ::= r | (R, R) | LabelTerm with RegAtom atoms; WTLabel for well-typed labels |
Semantic Gap
| Aspect | D-Hammer | Fanal |
|---|---|---|
| LDirac typing | Static types D(s1, s2) with disjointness as typing side condition | Dynamic typing: disjointness checked at evaluation time (Option DynLDiracVal) |
| Semantics formalization | Paper-level denotational (Hilbert spaces) | Machine-checked denotational (Mathlib matrices) |
| Cylindrical extension | cl(D, s) = D tensor 1_s with SWAP operators for reordering | Access path model with RegAtom lists and dimValAppendEquiv |
| Scalar reasoning | Delegated to Mathematica engine via WSTP | Lean-native: ring, field_simp, norm_num, complex number lemmas |
| Big operator handling | SUM[s, FUN[i, BASIS[sigma], body]] with de Bruijn + sum-swap | bigSum x s body with named bound variables |
Coverage and Benchmarks
| Aspect | D-Hammer | Fanal |
|---|---|---|
| Textbook (QCQI) | 18/18 solved in 0.82s | Subset encoded and verified |
| CoqQ examples | 158/162 solved in 9.74s (4 use unsupported projectors) | Growing coverage; roadmap target: encode most D-Hammer examples |
| Labelled Dirac (LDN) | 6+ solved (0.03s-7.37s) | Labelled Dirac examples available |
| Quantum Circuits | 5/6 solved (1 timeout on QC-6) | Circuit equivalences encoded via labelled Dirac |
| Performance | Sub-second on most examples (C++ native) | Compilation-time checking (slower but certified) |
Integration Impact
| Aspect | D-Hammer | Fanal |
|---|---|---|
| Push-button proofs | Already achieves this (as unverified tool) | dirac_eq and ldirac_eq would close goals automatically with kernel-checked proofs |
| Program verification | Not in scope | Labelled Dirac reasoning is prerequisite for quantum Hoare logic |
| Loewner order | Not in scope | Builds on equational reasoning as foundation |
| Trust model | User trusts C++ + Mathematica implementation | Every proof step verified by Lean kernel |
Label Elimination
| Aspect | D-Hammer | Fanal |
|---|---|---|
| Approach | Three-step: decompose to labelled basis -> rewrite to normal form -> order and eliminate quantum variables | Needs soundness proofs against LDiracWellTyped.eval semantics |
| Soundness | Proved on paper (Theorem 2) | Would be machine-checked in Lean |
| Completeness | Proved on paper for the label elimination reduction | Would be machine-checked in Lean |
| Implementation | C++ with ANTLR4 parsing | Lean 4 metaprogram or Expr-level tactic |
Summary: Key Differences
| Aspect | D-Hammer | Fanal |
|---|---|---|
| Relationship | Standalone decision procedure | Integration target for D-Hammer |
| Trust Base | Unverified C++ / Mathematica | Lean 4 kernel (fully verified) |
| Scope | Dirac equational reasoning only | Full program verification |
| Research Group | Same group (BASICS Lab) | Same group (BASICS Lab) |
| Synergy | Provides automation engine | Provides kernel-checked proof certificates |