关于seq(i,f)的定理证明求助：seq_thm引理无法被SMT自动调用

Dafny的SMT求解器无法自动推导递归定义的seq的全称量化性质，直接用forall块无法完成证明，需要通过归纳法来证明该引理，这样才能让求解器后续自动调用它。

方法1：手动归纳证明 #

lemma seq_thm<T>(j: nat, f: nat ~> T)
  requires forall i :: 0 <= i < j ==> f.requires(i)
  ensures forall i :: 0 <= i < j ==> seq(j, f)[i] == f(i)
{
  if j == 0 {
    // 基础情况：j=0时无满足条件的i，性质自动成立
  } else {
    // 递归调用，应用归纳假设到j-1
    seq_thm(j-1, f);
    
    forall i | 0 <= i < j {
      if i < j-1 {
        // 利用seq的递归定义，前j-1个元素和seq(j-1,f)一致
        assert seq(j, f)[i] == seq(j-1, f)[i];
        // 应用归纳假设得到结论
        assert seq(j-1, f)[i] == f(i);
      } else {
        // i=j-1时，seq(j,f)的最后一个元素就是f(j-1)，直接用seq构造定义
        assert seq(j, f)[i] == f(i);
      }
    }
  }
}

方法2：使用Dafny内置归纳关键字 #

用induction关键字可以简化归纳框架的书写：

lemma seq_thm<T>(j: nat, f: nat ~> T)
  requires forall i :: 0 <= i < j ==> f.requires(i)
  ensures forall i :: 0 <= i < j ==> seq(j, f)[i] == f(i)
  induction j
{
  case 0 => {}
  case j+1 => {
    forall i | 0 <= i < j+1 {
      if i < j {
        assert seq(j+1, f)[i] == seq(j, f)[i];
        // 直接引用归纳假设的结论
        assert seq(j, f)[i] == f(i);
      } else {
        // 匹配seq的构造规则，最后一个元素等于f(j)
        assert seq(j+1, f)[i] == f(i);
      }
    }
  }
}

关键说明 #

• seq是递归构造的（seq(0,f)=[]，seq(k,f)=seq(k-1,f)+[f(k-1)]），全称量化的索引性质无法被SMT自动展开，必须通过归纳覆盖所有可能的j和i。
• 证明完成后，Dafny会将该引理标记为可自动调用的定理，后续涉及seq索引访问的证明场景中，求解器会自动应用这个结论。
• 前置条件forall i :: 0 <= i < j ==> f.requires(i)确保了f(i)的调用合法性，避免证明过程中出现前置条件违反的错误。

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