Dafny中codatatype与least predicate的合理性及矛盾问题问询

我尝试用以下代码处理无限列表：

codatatype iList = iCons(head: int, tail: iList)

least predicate isIn(e: int, l: iList)
{
  e == l.head || isIn(e, l.tail)
}

least predicate allThrees(input: iList)
{
  input.head == 3 && allThrees(input.tail)
}

least lemma Check1_Lemma(input: iList)
  requires allThrees(input)
  ensures forall b: int :: isIn(b, input) ==> b == 3
{}

我选择用least predicate而非greatest predicate，因为它能证明更多属性，但这里出现了问题。当我定义如下谓词：

least predicate aValidInput(input: iList)
{
  0 <= input.head && input.head <= 3 && aValidInput(input.tail)
}

尝试证明引理时：

least lemma Check2_Lemma(input: iList)
  requires allThrees(input)
  ensures aValidInput(input)
{} 

竟然也能证明它的反命题：

least lemma Check3_Lemma(input: iList)
  requires allThrees(input)
  ensures ! aValidInput(input)
{} 

问题出在least predicate上吗？但用greatest predicate时，我连那些基础引理都证明不了。

问题根源：最小谓词对无限递归的语义特性 #

在Isabelle/HOL中，least predicate（最小不动点谓词）的语义是仅包含能通过有限次递归展开满足谓词的元素。但对于无限列表这种共归纳类型，最小不动点的定义实际上无法覆盖任何无限递归的实例——因为无限递归永远无法通过有限次展开完成验证。

具体到你的例子：

• allThrees作为最小谓词，其最小不动点是空集。要满足allThrees(input)，需要无限次验证每个元素都是3，而最小不动点只接受有限步可证明的情况，因此没有任何无限列表能满足该谓词。
• 由于requires allThrees(input)的前提永远为假，根据逻辑中的空虚真原则，任何结论（无论是aValidInput(input)还是!aValidInput(input)）都会被自动证明为真——前提不成立时，蕴含式恒为真。

为什么最大谓词能解决这个问题？ #

greatest predicate（最大不动点谓词）才是为共归纳类型设计的，它允许通过共归纳证明验证无限递归的属性：

• 最大不动点包含所有满足递归谓词的元素，包括无限展开的实例。
• 对于allThrees，使用最大不动点时，你可以通过共归纳证明：只要当前元素是3，且尾部满足allThrees，整个列表就满足该谓词。

修正方案 #

把涉及无限列表的谓词都改为greatest predicate，并使用共归纳证明验证引理：

codatatype iList = iCons(head: int, tail: iList)

greatest predicate isIn(e: int, l: iList)
{
  e == l.head || isIn(e, l.tail)
}

greatest predicate allThrees(input: iList)
{
  input.head == 3 && allThrees(input.tail)
}

coinductive lemma Check1_Lemma(input: iList)
  requires allThrees(input)
  ensures forall b: int :: isIn(b, input) ==> b == 3
proof -
  assume "allThrees input"
  thus "forall b. isIn b input --> b = 3"
  by(coinduction arbitrary: input b) auto
qed

greatest predicate aValidInput(input: iList)
{
  0 <= input.head && input.head <= 3 && aValidInput(input.tail)
}

coinductive lemma Check2_Lemma(input: iList)
  requires allThrees(input)
  ensures aValidInput(input)
proof -
  assume "allThrees input"
  thus "aValidInput input"
  by(coinduction arbitrary: input) auto
qed

这样既可以证明基础引理，也不会出现矛盾的证明结果——因为allThrees的前提现在可以被无限列表满足，空虚真的情况不再发生。

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