尝试在 Dafny 中证明非重复元素序列时遇到的问题

Question

假设我们有一个序列 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|

忽略

insertionSort

的实现即可。无论如何，最后我们得到另一个序列

r

，具有这样的属性：

  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)
{
}

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

Answer 1

下面的证明背后的想法如下

1. 如果不是的话，序列中的所有元素 r 是唯一的，那么应该存在索引 m < n such that r[m] == r[n].
2. 接下来我们尝试将序列 s（左）的元素与 序列 r（右）的元素相等。
3. 为此，我们在 r 中找到索引 rodx，这样 r[ridx] 等于 与我们正在配对的 s 的当前元素。
4. 现在如果ridx恰好是n，那么我们可以将当前的 s 中 r[m] 的元素为 r[m] == r[n]
5. 实际上，我们将 n 个不同的元素与 n-1 个元素。
6. 我们做了一些索引转换来让达夫尼相信我们 确实与右侧的 n-1 个元素配对 匹配。
7. 通过分类，左边的两个元素应该与 右侧相同的元素。
8. 这意味着这两个元素相等，但事实并非如此 这是可能的，因为所有元素在左侧都是不同的。
9. 我们的假设是错误的，所有元素都在右边 是不同的。

---

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];
  }
}