这是关于用 Coq 语言编写的 2021 年 Advent of Code 的解决方案总结：

• 运行代码：依赖 Coq（测试版本 8.13）和 coq-stdpp，安装依赖后可通过cd src/进入目录，使用./a.sh aoc01.v aoc01_input.txt solve12运行 Day 01，sh./runall.sh运行所有天数。

• 注意事项：

  • 执行：答案通过直接评估计算，无提取操作。
  • 解析：输入可直接包含在 Coq 文件中利用符号扩展，不行时通过预处理脚本处理，如引号处理、去除特殊字符等。

  • 证明：部分解决方案有相关规范和证明。

    • Day 1：Part 2 两种计算方法结果相同有证明，通过融合算法避免重复计算。
    • Day 2：用“模拟”概念证明 Part 2 的“aim”与 Part 1 的“depth”行为相同。
    • Day 7：证明 Part 2 在给定范围内找到最小成本解，涉及凸函数和二分搜索的相关定理。
    • Day 8：有正确性规范但未证明，可改进以检测无效输入。
    • Day 10：包含完整的解析器正确性定理，包括成功和失败情况的描述。
    • Day 11：依赖章鱼闪光顺序不影响最终状态的属性（confluence），有相关规范但无证明。
    • Day 19：有优化的规范但证明不完全，处理多个匹配较复杂。
    • Day 22：通过隐式表示立方体实现效率，有对应证明，缺失体积计算的引理。
    • Day 24：利用输入迭代规律简化，有证明和最终搜索算法的规范。
• 额外评论：未正式规范的天数中，Day 6、12、21 是典型动态规划问题，Day 14 是简单的表示变化，Day 15 可验证 Dijkstra 算法，Day 18 可验证蜗牛鱼加法的终止性。