Dafny 在高阶多态函数中证明引理

Question

我一直在研究一种算法 (Dafny cannot prove function-method equivalence, with High-Order-Polymorphic Recursive vs Linear Iterative) 来计算一个序列中包含属性 P 的子序列的数量。例如，'the number of positives on its left part are more that on its right part'.

有多少子序列

但这只是为了提供一些背景信息。

重要的功能就是下面这个CountAux功能。给定一个命题 P（比如 x is positive），一个 sequ 序列序列，一个在序列中移动的索引 i，以及一个上限 j :

function  CountAux<T>(P: T -> bool, sequ: seq<T>, i: int, j:int): int 
  requires 0 <= i <= j <= |sequ|
  decreases j - i //necessary to prove termination
  ensures CountAux(P,sequ,i,j)>=0;
{
  if i == j then 0
  else (if P(sequ[i]) then 1 else 0) + CountAux(P, sequ, i+1,j)
}

为了结束它，现在，事实证明我需要几个引理（我坚信它们是正确的）。但是我不知道如何证明，任何人都可以帮助或提供证据吗？看起来不难，但我不习惯在Dafny证明（确定它们可以使用结构归纳法完成）。

这些是我想证明的引理：


lemma countLemma1<T>(P: T -> bool, sequ: seq<T>,i:int,j:int,k:int)
requires 0<=i<=k<=j<=|sequ|
ensures CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j)
//i.e. [i,k) [k,j)
{
  if sequ == [] {
    assert CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j);
  }
  else{
    assert CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j);
  }
}

lemma countLemma2<T>(P: T -> bool, sequ: seq<T>,i:int,j:int,k:int,l:int)
requires 0<=i<=j<=|sequ| && 0<=k<=l<=j-i
ensures CountAux(P,sequ[i..j],k,l)==CountAux(P,sequ,i+k,i+l)
//that is, counting the subsequence is the same as counting the original sequence with certain displacements
{
  if sequ == [] {
    assert CountAux(P,sequ[i..j],k,l)==CountAux(P,sequ,i+k,i+l);
  }
  else{
    assert CountAux(P,sequ[i..j],k,l)==CountAux(P,sequ,i+k,i+l);
  }
}

编辑：

我一直在尝试，但似乎我误解了结构归纳法。我确定了三个基本案例。其中，我看到如果 i==0，则归纳应该成立（失败），因此如果 i>0 我尝试使用归纳达到 i==0：

lemma countID<T>(P: T -> bool, sequ: seq<T>,i:int,j:int,k:int)//[i,k) [k,j)
requires 0<=i<=k<=j<=|sequ|
ensures CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j)
{
  if sequ == [] || (j==0) || (k==0) {
     assert CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j);

  }
  else {
    if (i==0) {
      countID(P,sequ[1..],i,j-1,k-1);
      assert CountAux(P,sequ[1..],i,j-1)
        ==CountAux(P,sequ[1..],i,k-1)+CountAux(P,sequ[1..],k-1,j-1);
      assert CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j);

    }
    else{
      //countID(P,sequ[i..],0,j-i,k-i);
      //assert CountAux(P,sequ[i..],0,j-i)
      //  ==CountAux(P,sequ[i..],0,k-i)+CountAux(P,sequ[i..],k-i,j-i);
      countID(P,sequ[1..],i-1,j-1,k-1);
      assert CountAux(P,sequ[1..],i-1,j-1)
        ==CountAux(P,sequ[1..],i-1,k-1)+CountAux(P,sequ[1..],k-1,j-1);
    }
    //assert CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j);
  }
}

Answer 1

你可以用递归的方式证明你的引理。详细解释可以参考https://www.rise4fun.com/Dafny/tutorialcontent/Lemmas#h25。它还有一个例子恰好与你的问题非常相似。

lemma countLemma1<T>(P: T -> bool, sequ: seq<T>,i:int,j:int,k:int)
requires 0<=i<=k<=j<=|sequ|
ensures CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j)
decreases j - i
//i.e. [i,k) [k,j)
{
  if i == j {
    assert CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j);
  }
  else{
    if i == k {
        assert CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j);
    }
    else {
        countLemma1(P, sequ, i+1, j, k); 
        assert CountAux(P,sequ,i,j)==CountAux(P,sequ,i,k)+CountAux(P,sequ,k,j);
    }
  }
}

lemma countLemma2<T>(P: T -> bool, sequ: seq<T>,i:int,j:int,k:int,l:int)
requires 0<=i<=j<=|sequ| &&  0<=k<=l<=j-i
ensures CountAux(P,sequ[i..j],k,l)==CountAux(P,sequ,i+k,i+l)
decreases j - i
//that is, counting the subsequence is the same as counting the original sequence with certain displacements
{
  if i == j {
    assert CountAux(P,sequ[i..j],k,l) == CountAux(P,sequ,i+k,i+l);
  }
  else{
    if k == l {
        assert CountAux(P,sequ[i..j],k,l) == CountAux(P,sequ,i+k,i+l);
    }
    else {
        countLemma1(P, sequ[i..j], k, l, l-1); 
        assert CountAux(P,sequ[i..j],k,l) == CountAux(P,sequ[i..j],k,l-1) + CountAux(P,sequ[i..j],l-1,l);

        countLemma1(P, sequ, i+k, i+l, i+l-1); 
        assert CountAux(P,sequ,i+k,i+l) == CountAux(P,sequ,i+k,i+l-1) + CountAux(P,sequ,i+l-1,i+l);

        countLemma2(P, sequ, i, j-1, k ,l-1);
        assert CountAux(P,sequ[i..(j-1)],k,l-1) == CountAux(P,sequ,i+k,i+l-1);

        lastIndexDoesntMatter(P, sequ, i,j,k,l);
        assert CountAux(P,sequ[i..j],k,l-1) == CountAux(P,sequ[i..(j-1)],k,l-1);   // this part is what requires two additional lemmas

        assert CountAux(P,sequ[i..j],l-1,l) == CountAux(P,sequ,i+l-1,i+l);

        assert CountAux(P,sequ[i..j],k,l) == CountAux(P,sequ,i+k,i+l);
    }
  }
}


lemma lastIndexDoesntMatter<T>(P: T -> bool, sequ: seq<T>,i:int,j:int,k:int,l:int) 
    requires i != j
    requires k != l
    requires 0<=i<=j<=|sequ| &&  0<=k<=l<=j-i
    ensures CountAux(P,sequ[i..j],k,l-1) == CountAux(P,sequ[i..(j-1)],k,l-1)
{
    assert l-1 < j;

    if j == i + 1 {
    }
    else {
        unusedLastIndex(P, sequ[i..j], k, l-1);
        assert sequ[i..(j-1)] == sequ[i..j][0..(|sequ[i..j]|-1)];
        assert CountAux(P,sequ[i..j],k,l-1) == CountAux(P,sequ[i..(j-1)],k,l-1);
    }
}


lemma unusedLastIndex<T>(P: T -> bool, sequ: seq<T>, i: int, j:int)
    requires 1 < |sequ|
    requires 0 <= i <= j < |sequ|
    ensures CountAux(P,sequ,i,j) == CountAux(P,sequ[0..(|sequ|-1)],i,j)
    decreases j-i
{
    if i == j{
    }
    else {
        unusedLastIndex(P, sequ, i+1, j);
    }
}

Dafny 在高阶多态函数中证明引理

Dafny prove lemmas in a high-order polymorphic function

formal-verification

theorem-proving

induction

dafny