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

问题描述

我想在 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 语法似乎有效），所以可能我表达了一些不好的东西。这是我正在做的完整证明的最后一步，所以这是最后一种可能性很重要。

有什么帮助吗？

解决方法

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

<script src="https://cdnjs.cloudflare.com/ajax/libs/jquery/3.3.1/jquery.min.js"></script>
<div class="flex">
  <div>Box1</div>
  <div>Box2</div>
</div>

下限默认为 ensures sequ[0..|sequ|] == sequ[0..|sequ|/2] + sequ[|sequ|/2..|sequ|] ，上限默认为0，因此您可以将条件简化为

|sequ|

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

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