Dafny中filter函数相关引理filterLemmaExtra与filterLemmaSizes证明受阻

基础函数定义 #

先明确我们用到的filter和统计满足谓词元素数量的count辅助函数（匹配常见快速排序场景的定义）：

function filter<T>(s: seq<T>, p: T -> bool): seq<T> {
  if s == [] then []
  else if p(s[0]) then [s[0]] + filter(s[1..], p)
  else filter(s[1..], p)
}

function count<T>(s: seq<T>, p: T -> bool): nat {
  if s == [] then 0
  else if p(s[0]) then 1 + count(s[1..], p)
  else count(s[1..], p)
}

一、filterLemmaExtra的证明 #

假设你的引理目标是：当i < |filter(s, p)|时，filter(s + t, p)[i] = filter(s, p)[i]（拼接序列filter结果的索引对应关系），以下是可行的证明方案：

证明思路：结构归纳+分情况拆解 #

对序列s做结构归纳，分基例和归纳步骤，再针对首元素是否满足谓词拆分场景，把复杂断言拆成Dafny可自动验证的小步骤。

实现代码 #

lemma filterLemmaExtra<T>(s: seq<T>, t: seq<T>, p: T -> bool)
  ensures forall i: nat :: i < |filter(s, p)| ==> filter(s + t, p)[i] == filter(s, p)[i]
{
  if s == [] {
    // 基例：空序列无有效i，断言 vacuously true
  } else {
    filterLemmaExtra(s[1..], t, p); // 先应用归纳假设
    if p(s[0]) {
      // 验证i=0的场景
      assert filter(s + t, p)[0] == s[0];
      assert filter(s, p)[0] == s[0];
      // 验证i>0的场景
      forall i: nat where 0 < i < |filter(s, p)| {
        let j := i - 1;
        assert j < |filter(s[1..], p)|;
        assert filter(s + t, p)[i] == filter(s[1..] + t, p)[j];
        assert filter(s, p)[i] == filter(s[1..], p)[j];
        calc {
          filter(s + t, p)[i];
          == filter(s[1..] + t, p)[j];
          == filter(s[1..], p)[j];  // 应用归纳假设
          == filter(s, p)[i];
        }
      }
    } else {
      assert filter(s + t, p) == filter(s[1..] + t, p);
      assert filter(s, p) == filter(s[1..], p);
      // 直接复用归纳假设
      forall i: nat where i < |filter(s, p)| {
        calc {
          filter(s + t, p)[i];
          == filter(s[1..] + t, p)[i];
          == filter(s[1..], p)[i];  // 归纳假设
          == filter(s, p)[i];
        }
      }
    }
  }
}

二、filterLemmaSizes的证明 #

假设你的引理目标是：|filter(s, p)| = count(s, p)（filter结果长度等于原序列中满足谓词的元素数），以下是直接有效的证明方案：

证明思路：结构归纳+谓词分情况 #

这类等式证明用结构归纳最直接，无需反证法。对s归纳后，按首元素是否满足谓词拆分，复用归纳假设即可完成推导。

实现代码 #

lemma filterLemmaSizes<T>(s: seq<T>, p: T -> bool)
  ensures |filter(s, p)| == count(s, p)
{
  if s == [] {
    // 基例：空序列长度均为0
    assert filter(s, p) == [];
    assert count(s, p) == 0;
  } else {
    filterLemmaSizes(s[1..], p); // 应用归纳假设
    if p(s[0]) {
      assert filter(s, p) == [s[0]] + filter(s[1..], p);
      assert |filter(s, p)| == 1 + |filter(s[1..], p)|;
      assert count(s, p) == 1 + count(s[1..], p);
      calc {
        |filter(s, p)|;
        1 + |filter(s[1..], p)|;
        1 + count(s[1..], p);  // 归纳假设
        count(s, p);
      }
    } else {
      assert filter(s, p) == filter(s[1..], p);
      assert |filter(s, p)| == |filter(s[1..], p)|;
      assert count(s, p) == count(s[1..], p);
      calc {
        |filter(s, p)|;
        |filter(s[1..], p)|;
        count(s[1..], p);  // 归纳假设
        count(s, p);
      }
    }
  }
}

额外提示 #

如果你的引理断言和上述假设不同，比如涉及多序列组合或更复杂的索引范围，可以调整归纳对象（比如对t归纳），或者拆分更多子断言降低验证复杂度——核心是避免让Dafny一次性处理复杂逻辑，把大目标拆成可逐步验证的小步骤。

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