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

如何解决Dafny 证明了高阶多态函数中的引理

我一直在研究一种算法 (Dafny cannot prove function-method equivalence,with High-Order-Polymorphic Recursive vs Linear Iterative) 来计算包含属性 P 的序列的子序列的数量。例如，有多少子序列认为“其左侧的正数比右侧的多”。

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

重要的函数就是下面这个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,i+1,j)
}

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

这些是我想证明的引理：

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

lemma countLemma2<T>(P: T -> bool,k:int,l:int)
requires 0<=i<=j<=|sequ| && 0<=k<=l<=j-i
ensures CountAux(P,sequ[i..j],l)==CountAux(P,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,i+l);
  }
  else{
    assert CountAux(P,i+l);
  }
}

编辑：

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

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

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

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

解决方法

您可以以递归方式证明您的引理。 详细解释请参考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,k)+CountAux(P,k,j)
decreases j - i
//i.e. [i,k) [k,j)
{
  if i == j {
    assert CountAux(P,j);
  }
  else{
    if i == k {
        assert CountAux(P,j);
    }
    else {
        countLemma1(P,i+1,j,k); 
        assert CountAux(P,j);
    }
  }
}

lemma countLemma2<T>(P: T -> bool,k:int,l:int)
requires 0<=i<=j<=|sequ| &&  0<=k<=l<=j-i
ensures CountAux(P,sequ[i..j],l)==CountAux(P,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,l) == CountAux(P,i+l);
  }
  else{
    if k == l {
        assert CountAux(P,i+l);
    }
    else {
        countLemma1(P,l,l-1); 
        assert CountAux(P,l-1) + CountAux(P,l-1,l);

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

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

        lastIndexDoesntMatter(P,l);
        assert CountAux(P,l-1);   // this part is what requires two additional lemmas

        assert CountAux(P,i+l);

        assert CountAux(P,i+l);
    }
  }
}


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

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


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