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|

调用该函数后得到新序列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)
{
}

通过建立序列元素唯一性与多重集元素计数为1的等价关系，用矛盾法完成证明。

首先定义核心等价引理：

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

以下是完整证明实现：

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

2. 元素唯一推导出多重集计数为1 #

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

3. 多重集计数为1推导出元素唯一 #

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

4. 完成等价性证明 #

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

内容的提问来源于stack exchange，提问作者MogicFrog