如何解决在 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..]
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。