自动归纳

# 自动归纳

K. Rustan M. Leino Manuscript KRML 269, 31 May 2019

摘要

对于简单的例子，Dafny的自动归纳法足够强大，可以在不需要人工输入的情况下证明一些引理，并帮助减少证明其他引理所需的人工输入。本说明解释了自动感应是如何应用的，以及如何使用两个主要旋钮来调整自动化的功能。

Dafny不仅支持手工编写的引理，而且还提供了一些自动化功能，帮助通过归纳来证明引理[0] (opens new window)。让我们从手动证明的变化开始，然后看看自动感应如何提供或无法提供证明，最后看看如何调整自动化的功能。

# 运行实例

# 列表和函数定义

考虑以下递归定义列表的标准定义，以及一个Length函数和一个构造递增整数列表的函数。

datatype List<A> = Nil | Cons(A, List<A>)

function method Length(list: List): nat {
  match list
  case Nil => 0
  case Cons(_, tail) => 1 + Length(tail)
}

function method Range(start: int, len: nat): List<int>
  decreases len
{
  if len == 0 then Nil else Cons(start, Range(start+1, len-1))
}

1
2
3
4
5
6
7
8
9
10
11
12
13

有了这些定义，我们开始证明列表Range(start, len)的长度是len。

# 引理和证明

我们要证明list Range(start, len)的长度是len。我们从手工验证开始。为了确保在第一个示例中自动归纳不会对我们有帮助，我用属性{:induction false}标记了引理。

lemma {:induction false} RangeLength(start: nat, len: nat)
  ensures Length(Range(start, len)) == len
  decreases len
{
  if len == 0 {
    // trivial
  } else {
    calc {
      Length(Range(start, len));
    ==  // def. Range, since len > 0
      Length(Cons(start, Range(start+1, len-1)));
    ==  // def. Length on Cons
      1 + Length(Range(start+1, len-1));
    ==  { RangeLength(start+1, len-1); }  // apply induction hypothesis
      1 + len - 1;
    ==  // arithmetic
      len;
    }
  }
}

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

提示

出于本文的目的，我假设您已经基本了解如何手动编写这样的证明，无论是在Dafny还是在纸上。我将在这里描述证明的要素，但不会试图解释所有可能的考虑因素。

引理称为RangeLength，由start和len参数化，就像Range函数一样。引理证明的属性在ensures子句中陈述。它也被称为“证明目标”。

引理的签名部分还定义了一个decreases子句，该子句表示表达式len将被用作引理的任何递归调用的终止度量。这个终止度规与“范围”函数的终止度规相同。这很常见，因为在引理的证明目标中，证明的结构通常遵循函数的结构。

引理主体分为两种情况，遵循“范围”定义中的情况。第一个例子是len == 0，它给出了一个非常简单的证明:当len == 0时，Range返回长度为0的Nil。

另一种情况是使用已验证的计算，通常称为calc语句[1 (opens new window)]。这个计算从表达式Length(Range(start, len))开始，并使用保持等式的转换来得到len，这正是证明目标所说的引理必须证明的。计算的前两个步骤应用Range和Length的定义，将表达式重写为我们可以看到表达式的形式

Length(Range(start+1, len-1))

这就是证明过程中有趣的一步。我们想用len - 1替换这个表达式，这需要证明表达式确实等于len - 1。用正确的参数，这就是我们要证明的引理。因此，我们使用calc语句提示并调用引理:

RangeLength(start+1, len-1);

因为这是对我们要证明的引理的递归调用，我们必须证明终止。对引理的递归调用通常被称为“归纳假设”的应用。这样，我们的终止检查对应于确保归纳是“有根据的”。在Dafny中，通过显示每个递归调用都会减少一些终止度量来证明终止，也就是说，递归调用的某个表达式的计算值比调用者的值要小。这个更小的终止度规表达式是什么“更小”是什么意思?表达式是len，由decreases子句给出，由于len是一个整数，Dafny使用“小于，以0为界的整数”作为顺序。

# 终止的细节

这太拗口了。让我们再回顾一下最后一部分，关于终止的部分。

为了证明对一个(函数、方法或)引理的递归调用会终止，我们将引理的每次调用按照合理的顺序与一个值关联起来。有充分的理由意味着不存在无限的降序链。也就是说，存在固定的排序，并且在该排序中，每一个连续的小值序列都是有限的。例如，在“小于，以“0”为界的整数”排序中，一个降序链是

57, 56, 48, 39, 20, 4

这个链是有限的。无论您写下的降序链是什么，它都是有限的(否则，您最终会得到一个负数，但请记住我们说过“以‘0’为界”0 (opens new window))。

Dafny为每种类型构建了一个固定的、基于良好基础的顺序。1 (opens new window)它还支持值的字典元组，这种元组的良好基础顺序是每个组件上类型的字典顺序。

我们将引理调用与这个固定的、有根据的顺序的值关联的方式是声明一个decreases子句。它的参数是一个表达式列表，这些表达式构成一个字典元组。对于“RangeLength”引理，我们使用了“减小len”。这意味着每次对引理的调用都将与传入参数len的相同值相关联。

函数Range也是递归的，对于它的调用，我们还使用len作为终止度量。函数Length也是递归的，但显然我们没有给它一个decreases子句。在缺少decreases子句的情况下，Dafny为我们提供了一个子句，即按给定顺序由函数/方法/引词的参数组成的字典元组。2 (opens new window)Length的终止度量是list(Dafny的有理有据的归纳数据类型的顺序是结构包含)。Dafny的ide提供了一个工具提示(你可以在函数/方法/引理声明上看到)，告诉你它为递归函数/方法/引理选择了哪个“减小”子句。

到目前为止，我已经说过Dafny定义了一个固定的、有根据的排序，而将引理调用与该排序中的值关联的方法是声明一个“减小”子句。验证者如何使用这些东西来证明终止?它证明了与被调用方关联的值严格低于与调用方关联的值。换句话说，它证明了每个递归调用都在递减链中采取了一步。因为每个链都是有限的，所以不存在无限递归。换句话说，递归调用终止。

在这个例子中，有一个从RangeLength(start, len)到RangeLength(start+1, len-1)的递归调用。引理使用了decreases len，所以验证器检查len-1 < len，这证明了终止。

类似地，有一个从Range(start, len)到Range(start+1, len-1)的递归调用。验证器检查len-1 < len，这证明了终止。

最后，有一个从Length(list)到Length(tail)的递归调用，其中tail在结构上包含在list中。因此，验证者也可以在这里证明终止。

# `RangeLength`的其他终止度量

考虑一下如果我们为“RangeLength”选择不同的终止度量会发生什么是有指导意义的。对于我们考虑的每一个元素，证明义务的构造方式都是相同的:RangeLength(start+1, len-1)的值必须小于RangeLength(start, len)的值。

假设我们声明RangeLength带有decreases 10*len + 28。是的，这个终止度规足以证明终止，因为10*len + 18小于10*len + 28。

decreases len - 6呢?不，Dafny会抱怨不能证明终止，如果你给它这个终止度量。它将无法证明在整数排序中lens -7低于lens -6，因为它们可能是负的。3 (opens new window)

让我们试试decreases start + len。不，因为start+1 + len-1不小于start+ len。

decreases start + 2*len怎么样?是的，这证明了终止，因为start+1 + 2*(len-1)小于start+ 2*len。

使用字典元组start, len怎么样?不，这不会证明终止，因为start+1, len-1在字典上并不小于start, len(事实上，它在字典上更大)。如果我们把“RangeLength”中的“减小”去掉，Dafny会为我们生成一个。它生成的值是decreases start, len，因为RangeLength的参数是start和len，按这个顺序。因此，如果没有明确的“减少”条款，Dafny会抱怨无法证明终止合同。

如何切换参数的顺序，比如len, start ?是的，这证明了终止，因为len-1, start+1小于len, start。

如果你改变RangeLength来交换它的参数start和len(并且对RangeLength做同样的交换递归调用)，那么你可以忽略decreases子句。在本例中，Dafny将生成decreases len, start，这证明了终止。然而，通常建议坚持参数顺序，这是手边函数/方法/引理最自然的顺序。

最后，这个奇怪的终止指标decreases 7,len怎么样?当你第一次大声读到这个的时候，你可能会说

减少7 ?什么东西能减少呢?7是我曾祖父母在世时的数字，7将永远是这个数字。没有办法降低!

你是对的，但“减少”条款不是这么说的。“减小”子句只是简单地说明了如何将每个引理调用以合理的顺序映射到一个值。所以，有了这个奇怪的终止度量，证明的义务是检查7,len-1在字典上小于7,len，它确实是。其实也没那么古怪。

# 一个较短的证明

让我们简化我们为RangeLength编写的手动证明。当我们写一个证明的时候，calc语句是很有用的，它也提供了一个可读的证明。但一旦我们找到了一个证明，我们有时会选择缩短它，也许是因为回想起来，我们发现自己太拘谨了，即使是对我们自己的口味来说。

我们上面写的calc陈述实际上只有一个重要步骤，即归纳假设的应用。事实上，我们可以用一个调用来替换整个calc语句:

lemma {:induction false} RangeLength(start: nat, len: nat)
  ensures Length(Range(start, len)) == len
  decreases len
{
  if len == 0 {
  } else {
    RangeLength(start+1, len-1);
  }
}

1
2
3
4
5
6
7
8
9

因为if的" then "分支是空的，我们当然也可以否定守卫，交换分支，并省略空的else:

lemma {:induction false} RangeLength(start: nat, len: nat)
  ensures Length(Range(start, len)) == len
  decreases len
{
  if len != 0 {
    RangeLength(start+1, len-1);
  }
}

1
2
3
4
5
6
7
8

# 强感应

我们还能比这个if语句做得更好吗?那要看你觉得什么更好了，但在达芙妮有办法消除这个分支。我们可以通过替换整个if语句和它对RangeLength的一次调用，用forall语句调用RangeLength来获取一大堆值。

首先，假设我们尝试使用以下代码作为RangeLength的主体:

forall start`, len` {
  RangeLength(start`, len`);
}

1
2
3

这个漫不经心的语句对所有可能的start和len值调用RangeLength。这是行不通的，因为很多递归调用都不会终止。我们需要限制自己的值为start和len，以减少终止度量。

那么，让我们试试这个:

lemma {:induction false} RangeLength(start: nat, len: nat)
  ensures Length(Range(start, len)) == len
  decreases len
{
  forall start`, len` | 0 <= len` < len {
    RangeLength(start`, len`);
  }
}

1
2
3
4
5
6
7
8

对于所有的start值和所有小于len值，调用RangeLength。也就是说，这个forall语句一次性对RangeLength进行了无数次递归调用。由于len 的值小于len，这无数次调用中的每一次都会终止。4 (opens new window)

这个版本的RangeLength进行验证。对于所有这样的小值的归纳假设的数学名称叫做“强归纳”。

好的，start的值可以大于start(在这一点上，它对于证明start + 1是其中一个值是至关重要的)。所以，你可能认为上面的“为所有人”的陈述不仅仅是强归纳。事实上，有些人可能会争辩说，这个forall语句也执行了所谓的“泛化”引理到所有的start值。但是如果你认为决定smaller的排序只是比较len组件，那么start， len decreases确实比start, len 小，只要len 小于len。不管你想怎么想，或者你想给它起什么数学名字，Dafny都接受上面的“所有人”的说法作为证明。在编程术语中，我们所做的就是证明每个递归调用都会终止，这与我们定义终止度规的方式是一样的，即decreases len。

# 自动归纳

有了这些背景知识，我们终于可以了解Dafny是如何实现自动感应的了。简而言之:如果你删除属性{:inducerfalse}(我引入这个属性只是为了禁用自动感应，而我们在一开始讨论什么是证明)，那么Dafny在默认情况下所做的就是插入我们刚才看到的forall语句。这意味着你可以删除手动插入的forall语句，因为Dafny会为你添加它。换句话说，Dafny接受了下面这个引理的证明:

lemma RangeLength(start: nat, len: nat)
  ensures Length(Range(start, len)) == len
  decreases len
{
}

1
2
3
4
5

简洁明了

# 自动归纳的详细情况

Dafny自动归纳法归根结底就是在每个引理的开头自动生成一个forall语句。这并不能解决所有的归纳法问题，但我很惊讶，这个简单的方法确实解决了这么多简单的归纳法问题。让我们来看看这个动作的组成部分。

对于带有形式参数args、前置条件P(args)、5 (opens new window)和终止度量T(args)的引理L， Dafny自动归纳在L的主体开头插入以下forall语句:

forall aa` | P(args`) && T(args`) < T(args) {
  L(args`);
}

1
2
3

此处

aa是形式参数args的子集，
aa ’是aa，适当地重命名有新的名字，
args’表示args，但是aa ’中的每个变量都被aa中的相应变量替换，并且
<表示Dafny的字典顺序是有根据的。

变量args的子集aa可以通过在引理上放置属性{:induction aa}来定制。如果没有给出这样的属性，那么Dafny启发式地选择aa。当您将鼠标悬停在引理的名称上时，Dafny会在工具提示中报告它所选择的内容。

我们可以把{:induction x}看作是‘对x进行归纳法’，但是要小心一点。我发现“归纳法胜过……”这个短语在数学上的常用用法合并了几个概念。因此，准确地说，{:induction aa}属性指定的是哪些参数要在上统一量化。

还有一个很容易忘记的微妙之处:“减少”条款很重要。当我们写一个类似于RangeLength的引理时，我们可能期望证明足够简单，以至于Dafny的自动归纳法会自动处理它。如果是这样，我们可以写下引理的类型签名和(前置和后置条件)。这通常是所有需要的，但在RangeLength的情况下，还需要提供减少子句。通常，如果引理所涉及的主函数(运行示例中的Range)需要一个显式的减小子句，那么引理也需要。唉，这很容易被忘记。

接下来，让我们考虑一些自定义RangeLength自动归纳的方法。

# 例如:缺少`decreases`

如果你忘记了“RangeLength”的“减小”子句会发生什么?引理看起来是这样的:

lemma RangeLength(start: nat, len: nat)
  ensures Length(Range(start, len)) == len
{
}

1
2
3
4

对于这个引理，Dafny提出了{:induction start，len}和decreases start，len.6 (opens new window)这意味着诱导操作插入隐含的forall语句

forall start`: nat, len`: nat |
  start` < start || (start` == start && len` < len)
{
  RangeLength(start`, len`);
}

1
2
3
4
5

正如我们在前一节中所探讨的，这并不能证明这个引理，因为关键的调用RangeLength(start+1, len-1)不在执行的调用中。

# 例如:只对`len`进行量化

如果我们手动覆盖量化变量，只列出len会怎么样?

lemma {:induction len} RangeLength(start: nat, len: nat)
  ensures Length(Range(start, len)) == len
{
}

1
2
3
4

然后我们得到下面的forall语句:

forall len`: nat |
  start < start || (start == start && len` < len)
{
  RangeLength(start, len`);
}

1
2
3
4
5

注意，这个例子中没有start。相反，原始的形式参数start用于公式化的范围表达式

P(start, len`) && T(start, len`) < T(start, len)

在这个例子中没有先决条件，所以P部分是true。因为我们没有提供一个明确的减少条款，Dafny生成了decreases start，len。因此，限制全局量化变量(即len ’)的范围表达式是

start < start || (start == start && len` < len)

简化为len ’ < len

同样，由于forall语句所包含的递归调用不包括关键的调用RangeLength(start+1, len-1)，Dafny将报告一个错误，引理的后置条件可能不成立。

即使我们手动提供了一个“减少”条款，结果也是一样的。这仍然会将len ’限制为小于len的值，这是可以的，但问题仍然是归纳假设只考虑给定的start值。

# 致谢

我很感谢Sean McLaughlin，他提供了跑步的例子和关于RangeLength自动感应的问题。

# 参考文献

[0]K. Rustan M. Leino. Automating induction with an SMT solver. In Viktor Kuncak and Andrey Rybalchenko, editors, Verification, Model Checking, and Abstract Interpretation — 13th International Conference, VMCAI 2012, volume 7148 of Lecture Notes in Computer Science, pages 315–331. Springer, January 2012. 🔎 (opens new window)

[1]K. Rustan M. Leino and Nadia Polikarpova. Verified calculations. In Ernie Cohen and Andrey Rybalchenko, editors, Verified Software: Theories, Tools, Experiments — 5th International Conference, VSTTE 2013, Revised Selected Papers, volume 8164 of Lecture Notes in Computer Science, pages 170–190. Springer, 2014. 🔎 (opens new window)

0.我化简了一下。Dafny对整数的合理排序实际上是“小于，且不超过一个负数的整数”。所以，一条链允许下降到0以下，但一旦它包含一个负数，它就必须停止。这个扩展是一个有根据的顺序，因为仍然没有办法做出一个无限递减链。[↩](http://leino.science/papers/krml269.html # back-fn-fn-int-order)

1.我化简了一下。Dafny的固定的有根据的顺序也对不同类型的值进行排序。[↩](http://leino.science/papers/krml269.html # back-fn-fn-across-types)

2.这是一个轻微的简化。Dafny为递归函数/方法/引理提出“减小”子句的启发式方法省略了类型对证明终止没有帮助的参数。例如，类型为类型参数的参数会在自动生成的“减小”子句中被省略。[↩](http://leino.science/papers/krml269.html # back-fn-fn-auto-decr)

3.在前面的例子中，我把握得很准，因为我也应该指出10*len + 18是非负的。)作者系 (opens new window)

4.“无数个电话?!”你对自己说。"即使每个调用都终止了，终止是怎么回事? "我不会在这里深入研究，但我至少要指出，我们调用的是一个引理，而不是一个编译的方法。因此，您不需要担心是否有足够的计算资源来进行无限次调用。[↩](http://leino.science/papers/krml269.html # back-fn-fn-inf-calls)

5.引理的前提条件是使用关键字requires声明的。它就像引理的一个先行词，在每个呼叫点都要检查它是否成立。运行的示例不包含前置条件。一个简单的方法是将start的类型从nat更改为int，并添加require 0 <= start。[↩](http://leino.science/papers/krml269.html # back-fn-fn-pre)

6.我提到过Dafny ide中的工具提示会告诉你Dafny选择了哪些“减少”条款。在撰写本文时，只有当函数/方法/引理的主体包含显式递归调用时，才会显示这样的工具提示。特别是，如果引理的主体是空的，则没有工具提示显示生成了什么“减小”子句。[↩](http://leino.science/papers/krml269.html # back-fn-fn-no-decr-tooltip)

编辑

上次更新: 2022/03/26, 14:38:56

自动调用引理→

自动归纳

# 自动归纳

# 运行实例

# 列表和函数定义

# 引理和证明

# 终止的细节

# RangeLength的其他终止度量

# 一个较短的证明

# 强感应

# 自动归纳

# 自动归纳的详细情况

# 例如:缺少decreases

# 例如:只对len进行量化

# 致谢

# 参考文献

# `RangeLength`的其他终止度量

# 例如:缺少`decreases`

# 例如:只对`len`进行量化