摘要: 1、研究背景（context）。
量子电路是一种表示量子计算过程的模型。如果一个量子电路被设计出来，用于实现一个量子算法，我们不可避免地需要分析这个电路，确保它的行为与算法要求相符合。当电路规模较大时，手动分析量子电路的行为将变得非常困难，而且容易出错。此外，有些电路是参数化的，用普通测试手段不能覆盖所有可能的情况，需要寻找新的分析方法。
2、目的（Objective）：
用交互式定理证明器来推理量子电路是一种高效且可靠的方式。现有的用矩阵显式计算的方法可描述量子电路用到的量子状态和操作，但是扩展性低，可读性差。并且随着量子电路规模的扩展，矩阵维度迅速扩大，计算和比较矩阵将非常耗时。所以我们在Coq中提出了一种基于Dirac记号的符号化推理方法来分析量子电路的等价性，它提升了推理过程的效率和可读性。
3、方法（Method）：
使用Dirac记号的符号化推理方法基于一组推理规则，并设计了一套化简策略。其核心思想是将单比特的bra与ket形式的矩阵乘法化简为标量，并通过及时消除0和1来简化矩阵表示。因此我们的方法是通过（半）自动重写而不是显式地计算矩阵来完成推理。
4、结果（Result&Findings）：
我们用Dirac记号定义量子门，提出量子电路的观察等价性并设计了新颖的符号化策略库。我们在Coq中对一些典型量子算法进行了形式化分析，并用我们的符号化策略推理对应的量子电路。每个算法的耗时结果和基于显式矩阵计算的方法做了对比。我们发现符号化方法的耗时显著减少了，比如对Grover算法的分析效率能提升5倍左右。
5、结论（Conclusions）：
我们提出了一种基于Dirac记号的量子电路符号化推理方法。它基于一组等价规则设计了一些化简策略。根据我们的案例研究，该方法比通常的显式矩阵表示更有效，并且非常适合在Coq中利用重写策略实现自动化。将来我们计划把相关方法从量子电路模型扩展到量子程序，在Coq中形式化经典和量子交互的量子编程语言的语义以及证明系统，并证明带有经典计算处理的量子算法的正确性。