试图在 Dafny 中证明非重复元素序列的问题-解网

问：

假设我们有一个序列 s，并且所有元素都与其他元素不同。我这样描述这个属性

predicate all_element_different(s: seq<int>)
{
  forall i,j :: 0 <= i < j < |s| ==> s[i] != s[j]
}

当然，另一种等效的方法是

forall i,j :: 0 <= i < |s| && 0 <= j < |s| && i != j ==> s[i] != s[j]

所以我在这里写了一个引理

lemma different_properties(s: seq<int>)
  requires all_element_different(s)
  ensures forall i,j :: 0 <= i < |s| && 0 <= j < |s| && i != j ==> s[i] != s[j]
{
}

出于某种原因，我需要对这个序列进行排序，我想得到另一个新序列，而不是直接修改旧序列。类似的东西

function insertionSort(s: seq<int>): (r: seq<int>)
  ensures multiset(s) == multiset(r)
  ensures sorted(r)
  ensures forall x :: x in s ==> x in r
  ensures |s| == |r|

只需忽略的实现。无论如何，最后我们得到另一个序列，其属性如下：insertionSortr

  var r := insertionSort(s);
  assert multiset(s) == multiset(r);
  assert |s| == |r|;
  //assert sorted(r); This property is not used here
  assert forall x :: x in s ==> x in r;
  assert all_element_different(s);

显然，谓词应该成立，但我无法证明。我试图提取该过程：all_element_different(r)

lemma sequence_properties(s: seq<int>, r: seq<int>)
  requires multiset(s) == multiset(r)
  requires |s| == |r|
  requires all_element_different(s)
  ensures all_element_different(r)
{
}

有人对这个引理的证明有一些想法吗？

================================================

受 @Divyanshu Ranjan 启发的新方法

在我问这个问题之前，我一直在探索使用多重性来完成证明。微不足道的是，这个引理成立

lemma equivalence(s: seq<int>)
  ensures UniqueElements(s) <==> forall k :: k in multiset(s) ==> multiset(s)[k] == 1

但我在证明方面有一些问题。现在使用矛盾，我完成了它。

lemma UniqueMultiSet(s: seq<int>, r: seq<int>)
  requires UniqueElements(s)
  requires |s| == |r|
  requires multiset(s) == multiset(r)
  ensures UniqueElements(r)
{
  equivalence(s);
  equivalence(r);
}

lemma unique_elements_imply_multiplicity_equals_1(s: seq<int>)
  requires UniqueElements(s)
  ensures forall k :: k in multiset(s) ==> multiset(s)[k] == 1
{
  var ms := multiset(s);
  if !(forall k :: k in ms ==> ms[k] == 1)
  {
    var k :| k in ms && ms[k] > 1;
    var i :| 0 < i < |s|;
    var left := s[..i];
    var right := s[i..];
    assert s == left+right;
    // assert multiset(s) == multiset(left) + multiset(right);
    // assert multiset(s)[k] == multiset(left)[k] + multiset(right)[k];
    if k in left && k in right
    {
      assert !UniqueElements(s);
    } else if k in left && k !in right
    {
      unique_elements_imply_multiplicity_equals_1(left);
    } else if k !in left && k in right
    {
      unique_elements_imply_multiplicity_equals_1(right);
    }else
    {
      assert k !in multiset(s);
    }
  }
}

lemma multiplicity_equals_1_imply_unique_elements(s: seq<int>)
  requires forall k :: k in multiset(s) ==> multiset(s)[k] == 1
  ensures UniqueElements(s)
{
  if(!UniqueElements(s))
  {
    var i, j, k :| 0 <= i < j < |s| && s[i] == s[j] == k;
    var left := s[..i+1];
    var right := s[i+1..];
    assert s == left + right;
    assert j >= i+1;
    assert k in left && k in right;
    assert multiset(s)[k] >= 2;
  }
}

lemma equivalence(s: seq<int>)
  ensures UniqueElements(s) <==> forall k :: k in multiset(s) ==> multiset(s)[k] == 1
{
  if(UniqueElements(s))
  {
    unique_elements_imply_multiplicity_equals_1(s);
  }
  if(forall k :: k in multiset(s) ==> multiset(s)[k] == 1)
  {
    multiplicity_equals_1_imply_unique_elements(s);
  }
}

序列 Dafny

如果不是这样，序列的所有元素 r 是唯一的，那么应该存在索引 m < n 使得 r[m] == r[n]。
接下来，我们尝试将序列 s（左）的元素与序列 R（右）的元素相等。
为此，我们在 r 中找到索引 ridx，例如 r[ridx] 相等对于我们正在配对的 S 的当前元素。
现在，如果 ridx 恰好是 n，那么我们可以将电流配对其中 r[m] 为 r[m] == r[n] 的 s 元素
实际上，我们正在将 n 个不同的元素与 n-1 个元素。
我们做了一些指数转移来说服 dafny 我们确实与右侧的 n-1 元素配对匹配。
通过鸽子洞，左边的两个元素应该与右边的相同元素。
这意味着这两个元素是相等的，但事实并非如此可能，因为所有元素在左侧都是不同的。
我们的假设是错误的，所有元素都是正确的是不同的。

predicate UniqueElements(s: seq<int>)
{
  forall i, j :: 0 <= i < j < |s| ==> s[i] != s[j]
}

lemma pigeonhole(m : int, n: int, f : int -> int)
  requires 0 <= m < n
  requires forall i :: 0 <= i < n ==> 0 <= f(i) < m
  ensures exists j, k :: (0 <= j < k < n) && f(j) == f(k)
{
  if m <= 0 {
    assert 0 <= f(0) < 0;
  }
  else {
    var i : int := 0;
    while i < n
      invariant forall k :: 0 <= k < i ==> 0 <= f(k) < m - 1
      invariant i <= n
    {
      if f(i) == m-1 {
        var j : int := i + 1;
        while j < n
          invariant forall k :: i < k < j ==> 0 <= f(k) < m - 1
        {
          if f(j) == m-1 { return; }
            j := j + 1;
        }
        var g : int -> int := x => if x < i then f(x) else f(x+1);
        pigeonhole(m-1, n-1, g);
        return;
      }
      i := i + 1;
    }
    pigeonhole(m-1, n, f);
  }
}


lemma UniqueMultiSet(s: seq<int>, r: seq<int>)
  requires UniqueElements(s)
  requires |s| == |r|
  requires multiset(s) == multiset(r)
  ensures UniqueElements(r)
{
  assert |multiset(s)| == |multiset(r)|;
  if !UniqueElements(r){
    var m, n :| 0 <= m < n < |r| && r[m] == r[n];
    forall idx | 0 <= idx < |s| ensures exists ridx :: 0 <= ridx < |r| && r[ridx] == s[idx]
    {
      assert s[idx] in multiset(r);
    }
    var f : int -> int :=
      x => if 0 <= x < |s|
           then
              var idx :| 0 <= idx < |r| && r[idx] == s[x];
              if idx < n then idx else if idx == n then m else idx - 1
           else -1;
    pigeonhole(|s|-1, |s|, f);
    var k, l :| 0 <= k < l < |s| && f(k) == f(l);
    assert s[k] == s[l];
  }
}

试图在 Dafny 中证明非重复元素序列的问题

Problems in trying to prove non-duplicate-element sequence in Dafny

评论

评论