如果Z3不支持，Dafny如何支持归纳

Question

Dafny可以选择设置{:induction false}。此外，据我所知，每当我们在Dafny中使用断言时，它会构造证明义务，然后使用Z3对其进行计算。

然而，我读到Z3不支持归纳：例如，。。。然而，任何非平凡性质都需要通过归纳来证明。Z3目前不支持归纳证明(z3中的叉积)

所以我的问题是：每当我们设置{:induction true}时，如果不使用Z3，这个归纳在Dafny中是如何执行的？是否存在不同的底层解算器？有什么启发法吗？最后一个是在这里提出的(Z3模型用于正确的Dafny方法)。

然而，我们谈论的是哪种类型的启发式？

Answer 1

可能没有@alias的答案那么详细，但简而言之，Dafny的隐式{:induction true}属性将添加关于子项的假设，这样您就不需要自己编写它们。

因此，如果你写一个递归引理来证明每三个斐波那契数是偶数，而没有{:induction}，你就必须递归调用引理。Dafny还需要递归调用才能终止：

function fib(x: nat): nat {
if x == 0 then 0 else
if x == 1 then 1 else
fib(x-1) + fib(x-2)
}
lemma {:induction false} FibIsDivisibleBy2(a: nat)
ensures a % 3 == 0 <==> fib(a) % 2 == 0
{
if a <= 2 {
} else {
FibIsDivisibleBy2(a-1);
FibIsDivisibleBy2(a-2);
}
}

在引擎盖下，发送给Z3进行验证的公式不包含归纳，但它将使用燃料展开fib，从而展开，得到的公式将看起来像这个超简化的Dafny假装是SMT LIB语法：

(declare-fun a Int)
(declare-fun fib (Int) Int)
(assert forall fib[fuel+1](a) == fib[fuel](a))
(assert fib[n+1](a) == (if a == 0 then 0 else if a == 1 then 1 else fib[n](a))
(assert (
|| (a <= 2                        // First branch
&& !(     a % 3 == 0
<==> fib[2](a) % 2 == 0)  // Postcondition, negated.
|| (a > 2
&&   // We add the assumptions provided by the recursive calls to lemma:
( && ((a-1) % 3 == 0 <==> fib[1](a-1) % 2 == 0)
&& ((a-2) % 3 == 0 <==> fib[1](a-2)  % 2 == 0)
&& 
!(a % 3 == 0 <==> fib[2](a) % 2 == 0)  /// Postcondition, negated
))))
(check-sat)

z3将返回为"0"；未说出"；而不需要诱导。你可以自己动手证明这个公式，如上所述。请注意，我省略了对终止的强制检查，它看起来像0 <= a - 1 < a && 0 <= a - 2 < a，以及子集类型0 <= a。

现在，如果你添加{:induction true}，Dafny将在幕后做的就是

• 1. 每次它看到另一个fib(X)时，它都会自动为您实例化引理
• 2. 展开fib的定义一次，并根据需要重新应用1)

这样，你就不需要自己编写这些递归调用，你的引理可以用零证明语句来证明：

lemma {:induction true} FibIsDivisibleBy2(a: nat)
ensures a % 3 == 0 <==> fib(a) % 2 == 0
{
}

Answer 2

Dafny首先是一种编程语言，它内置了对所编写程序的验证机制的支持。这台机器包括感应支架。注意，这与z3无关：这是Dafny自己支持的东西。所以，简单地回答你的问题：因为Dafny对归纳的支持不是由z3实现的：它是由Dafny自己实现的。将此与z3的目标进行比较：z3是一个理解SMTLib的按钮工具，非常适合将决策过程应用于(通常)一阶逻辑、代数数据类型、实数、线性整数运算等的无量词子集。特别是，z3本身不是一种编程语言，也不打算以这种方式使用。这使得它适合作为"；后端"；用于像Dafny这样专注于特定编程风格的自定义工具的工具。

归纳法的难点在于提出归纳不变量。一个很好的方式"；猜测；不变量是遵循程序的结构，这在ACL2定理证明中得到了很大程度的利用：程序的递归性质表明了一种归纳模式。当然，这并不总是足够的。归纳假设可能真的很难想出，而且通常需要用户指导。这是大多数定理证明者使用的风格，如HOL、Isabelle、Coq、Lean和许多其他人。

回顾Dafny，归纳的需求通常来自于Dafny程序中的循环。(请参见：https://dafny.org/dafny/DafnyRef/DafnyRef#20141-循环不变量sec循环不变量)。因此，Dafny可以构建；感应的"；使用典型的霍尔逻辑环路原理进行证明。(https://en.wikipedia.org/wiki/Hoare_logic)因此，Dafny所做的是获取带注释的程序(这是关键，你应该用它们的不变量来注释循环)，设置归纳证明(即基本情况和归纳步骤)，并根据SMTLib查询来制定这些证明，并将其传递给z3。(这是一个简化的账户，但它大致也是Why3等类似工具所遵循的策略。)因此；感应的"；证明由Dafny完成，它跟踪证明状态、归纳的子目标如何相互关联以及总体目标等，z3仅用于建立这些单独的目标中的每一个，这些目标不需要对其证明进行归纳。

关于Dafny是如何工作的一篇很好的论文是Rustan的论文：使用SMT的自动化定理证明。从某种意义上说，这是一篇非常好的论文，它概述了如何使用SMT构建定理证明器：虽然归纳法将是主要的工具，但在这样的系统中有许多活动部件，Rustan对所涉及的技术和挑战进行了非常好的概述。

总之，Dafny支持归纳，因为Dafny的验证系统实现了对归纳证明的支持。z3只是Dafny用来实现非归纳目标的后端工具；其他的一切都由Dafny自己记录。

最后一点：SMTLib的最新版本确实支持递归定义，其证明需要归纳。因此，SMT解算器有可能获得诱导能力，CVC5已经在一定程度上支持了诱导。(http://lara.epfl.ch/~reynolds/VMCAI2015 ind/smt ind RK.pdf)。因此，我预计在未来几年，smt解算器将具有更多的感应功能。然而，像Dafny、ACL2等工具将发挥关键作用，因为对于大多数软件应用程序来说，提出归纳不变量仍然是一门艺术，而不是工程；所以用户干预仍然是游戏的名称。但是，正如过去50年的定理证明文献所充分证明的那样，期望自动化系统随着时间的推移而变得更好是合理的。