时间戳

首页 > 解决方案 > 达芙妮。证明一个区间的所有值都出现在 seq 中

seq - 达芙妮。证明一个区间的所有值都出现在 seq 中

问题描述

我试图证明以下引理。这似乎真的微不足道，但我无法证明这一点。先感谢您！

lemma test(x : seq<int>)
  // if the values from x are margined by an interval
  // the values are different
  // and the number of values equals the size of the interval
  // then all values from the interval appear in x

  requires forall i :: 0 <= i < |x| ==> 
    0 <= x[i] < |x|;

  requires forall i :: 0 <= i < |x| ==>
   forall i' :: 0 <= i' < |x| && i != i' ==>
     x[i] != x[i'];

  ensures forall v :: 0 <= v < |x| ==>
    exists i :: 0 <= i < |x| && x[i] == v;
{

}

https://rise4fun.com/Dafny/d8VK

标签： seqdafny

解决方案

这是一种方法，使用一些关于集合基数的事实。

lemma test(x : seq<int>)
  // if the values from x are margined by an interval
  // the values are different
  // and the number of values equals the size of the interval
  // then all values from the interval appear in x

  requires forall i :: 0 <= i < |x| ==> 
    0 <= x[i] < |x|;

  requires forall i :: 0 <= i < |x| ==>
   forall i' :: 0 <= i' < |x| && i != i' ==>
     x[i] != x[i'];

  ensures forall v :: 0 <= v < |x| ==> v in x
{
    var L: set<int>, R: set<int> := {}, RangeSet(0, |x|);
    var i := 0;
    CardinalityRangeSet(0, |x|);
    while i < |x|
        invariant 0 <= i <= |x|
        invariant L == set j | 0 <= j < i :: x[j]
        invariant forall v | v in L :: v in x
        invariant forall v | 0 <= v < |x| :: v in L || v in R
        invariant |R| == |x| - i

    {
        L, R := L + {x[i]}, R - {x[i]};
        i := i + 1;
    }
}

predicate InRange(lo: int, hi: int, i: int)
{
    lo <= i < hi
}

function RangeSet(lo: int, hi: int): set<int>
{
    set i | lo <= i < hi && InRange(lo, hi, i)
}

lemma CardinalityRangeSet(lo: int, hi: int)
    decreases hi - lo
    ensures |RangeSet(lo, hi)| == if lo >= hi then 0 else hi - lo
{
    if lo < hi {
        assert RangeSet(lo, hi) == {lo} + RangeSet(lo + 1, hi);
        CardinalityRangeSet(lo + 1, hi);
    }
}

我稍微更改了您的规范以使用 Dafny 语法v in x，这与您编写的内容等效，并且对 Dafny 来说更容易推理。

R证明的基本思想是从元素的范围开始0..|x|，然后迭代地x[i]从中删除元素R并添加它们L。0..|x|这保持了该范围内的每个数字都在L或中的不变量，而在每次迭代R时，基数都会减少。R因此，循环结束时R为空，因此范围内的每个数字都必须在 中L，因此在 中x。

我还使用了一个通过归纳证明的辅助引理来证明它RangeSet具有预期的大小。

（已编辑以消除 中的“未找到触发条件”警告RangeSet。引入谓词InRange使其具有触发条件，但您仍然需要在其中包含显式范围，RangeSet否则它无法确定该集合是有限的。 )

推荐阅读