在 Dafny 中证明：一个非空的偶数序列，是它的两半的串联

Question

我想证明 Dafny 中的这个“微不足道”的引理。一个非空的偶数序列，是它的两半的串联：

lemma sequence_division(sequ:seq<int>)
    requires sequ != []
    requires even(|sequ|)
    ensures sequ[0..|sequ|] == sequ[0..(|sequ|/2)]+sequ[|sequ|/2+1..|sequ|]
    //{}

问题是我不习惯在没有典型数据类型的情况下证明归纳引理（使用 match...case...）。我必须使用 if 还是什么？

我试过了：

lemma sequence_division(sequ:seq<int>)
    requires sequ != []
    requires even(|sequ|)
    ensures sequ[0..|sequ|] == sequ[0..(|sequ|/2)]+sequ[|sequ|/2+1..|sequ|]
    {
        if |sequ| == 2 { assert sequ[0..|sequ|] == sequ[0..(|sequ|/2)]+sequ[|sequ|/2+1..|sequ|]; }
        //if |sequ| == 2 { assert sequ[0..2] == sequ[0..1]+sequ[1..2];}
    }

并将其标记为 assertion violation（因此 if 语法似乎有效），所以我可能表达了一些不好的意思。这是我正在做的完整证明的最后一步，所以这是最后一种可能性很重要。

有什么帮助吗？

Answer 1

问题是引理不成立，无法证明。在后置条件中等式的右侧，您正在跳过一个元素。这是引理后置条件的正确版本：

  ensures sequ[0..|sequ|] == sequ[0..|sequ|/2] + sequ[|sequ|/2..|sequ|]

下限默认为0，上限默认为|sequ|，所以可以将条件简化为

  ensures sequ == sequ[..|sequ|/2] + sequ[|sequ|/2..]

您可以进一步简化引理，因为两个前提条件都不是后置条件成立所必需的。最后，如果您愿意，可以通过对序列元素类型进行参数化来使引理更通用：

lemma sequence_division<T>(sequ: seq<T>)
  ensures sequ == sequ[..|sequ|/2] + sequ[|sequ|/2..]
{
}

在 Dafny 中证明：一个非空的偶数序列，是它的两半的串联

Proving in Dafny: A non-empty even sequence, is the concatenation of it's two halves

arrays

formal-verification

theorem-proving

induction

dafny