用 dafny 编写归纳引理答案

【问题标题】：writing inductive lemmas in dafny用 dafny 编写归纳引理
【发布时间】：2019-06-28 20:27:28
【问题描述】：

我想用 dafny 证明以下几点：

function append(xs: seq<int>) : seq<int> {  
  if |xs| == 0 then []  
  else [xs[0]] + append(xs[1..])
}

method test(o:seq<int>, xs: seq<int>, i:int)
requires 0 <= i < |xs|
{  
  if o == append(xs[..i])
  {
    assert o + [xs[i]] == append(xs[..(i+1)]);
  }
}

我认为这需要使用引理编写归纳证明，但我不确定如何编写引理。 online doc 给出了对序列内容使用结构归纳的示例，但我认为在这种情况下，我认为归纳步骤需要在 i 上？我试着写一个如下：

lemma appendLemma (xs:seq<int>, o:seq<int>, i:int)
requires 0 <= i < |xs|
requires o == append(xs[..i])
ensures o + [xs[i]] == append(xs[..(i+1)])
{
  if i == 0
  {
    assert o + [xs[0]] == append(xs[..1]);
  }
  else
  {    
    appendLemma(xs, o, i);
    // what to do here?
  }
}

但它一直要求一个减少子句，在这种情况下我不确定是否有一个？

【问题讨论】：

你所谓的append 似乎只是序列的副本。这是你的意图吗？
是的。我正在尝试学习如何使用 dafny 编写证明，所以我决定选择应该足够简单的东西。

标签： z3 dafny

【解决方案1】：

您将对序列的长度（xs 和 o）进行归纳，然后 i 也必须减少，如下面的证明所示。所以你可以说你对 i 进行归纳。但无论你做什么，对 appendLemma 的内部调用必须在较小的参数上。它代表归纳假设，见。这就是达夫尼抱怨解雇的原因。

由于我们所知道的函数 append 是它的归纳定义，以头/尾方式，我们必须在 appendLemma 的证明中遵循这种方式，并且我们在 xs 的尾部应用归纳。

我需要一个额外的引理 (appendIsCopyLemma) 来捕捉上面 Levent Erkok 的观察结果，即 append 实际上是一个简单的副本。请注意，Dafny 无需进一步帮助即可验证此引理，但您必须在 appendLemma 的证明中明确调用它（两次）。

请注意，Dafny 在原始代码中遗漏的减少子句现在将由 Dafny 自己推断；递归调用的参数现在已经有足够的帮助了。

// Verified by Dafny 2.2.0
// definition of append and test in the question above
lemma appendIsCopyLemma(xs: seq<int>)
  ensures xs == append(xs);
{ }

lemma appendLemma (xs:seq<int>, o:seq<int>, i:int)
  // decreases i; // Dafny can infer a decrease clause by itself
  requires 0 <= i < |xs|
  requires o == append(xs[..i])
  ensures o + [xs[i]] == append(xs[..(i+1)])
{
  if |xs| == 1 || i == 0
  {
    assert o + [xs[0]] == append(xs[..1]); //redundant
  }
  else
  {
    appendIsCopyLemma(xs[..i]);
    assert o[1..] == xs[1..][..i-1];
    appendLemma(xs[1..], o[1..], i-1);
    appendIsCopyLemma(xs[..i+1]);
    assert xs[..i+1] == append(xs[..i+1]);
  }
}

【讨论】：