Dafny中偏函数η等价性疑问：seq构造下两种形式是否等价？

核心疑问 #

在Dafny中，偏函数 f:T~>S（可能读取堆对象）是否等价于匿名函数形式 (x:T) reads f.reads requires f.requires(x) f(x)？

从语义上看，全函数满足η等价；偏函数的话，二者前置要求一致，定义域内输出也相同，理应等价。但当偏函数作为参数传入seq时，两种形式的验证表现却不一样：

可通过验证的展开式引理 #

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,(n:nat) reads f.reads requires f.requires(n) => f(n))[i] == f(i)
{
}

无法自动验证的η简化版引理 #

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

等价性结论 #

这两种形式语义上完全等价，问题出在Dafny的自动验证器上——它无法自动识别偏函数的η-归约等价性，尤其是当偏函数作为参数传递给seq这类内置函数时。

让Dafny认可等价性的方法 #

1. 显式展开偏函数 #

像第一个引理那样，手动写出偏函数的展开式，直接暴露其reads集合和requires前置条件，让验证器能匹配seq的构造逻辑。

2. 证明辅助等价引理 #

先单独证明偏函数和其展开式的等价性，再在主引理中调用该辅助引理完成推导：

// 辅助引理：证明偏函数与展开式在定义域内等价
lemma partial_eta_eq<T,S>(f: T ~> S, x: T)
requires f.requires(x)
ensures ( (y:T) reads f.reads requires f.requires(y) => f(y) )(x) == f(x)
{
}

// 主引理调用辅助引理完成验证
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)
{
  forall i | 0 <= i < j 
  {
    partial_eta_eq(f, i);
    calc {
      seq(j,f)[i];
      == seq(j, (n:nat) reads f.reads requires f.requires(n) => f(n))[i];
      == f(i);
    }
  }
}

3. 使用reveal命令展开内置函数 #

在主引理中用reveal seq;命令让验证器展开seq的定义，从而自动关联偏函数的展开式：

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)
{
  reveal seq;
  forall i | 0 <= i < j {}
}

简化版无法验证的原因 #

Dafny的内置seq函数在处理偏函数参数时，不会自动提取偏函数的reads集合和requires前置条件。验证器需要明确看到这些细节才能完成推理，而偏函数的封装特性导致这些信息被隐藏，因此必须通过手动干预来暴露这些内容，让验证器完成推导。

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