codatatypes 和最少谓词。有意义吗？

Question

我正在尝试按如下方式处理无限列表：

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

那么，问题是出在“最小谓词”的使用上吗？但是用“最伟大的谓词”我无法证明这些朴素的引理。

Answer 1

考虑以下片段。

least lemma IsFalse(input: iList)
  requires aValidInput(input)
  ensures false
{} 

给定

aValidInput

，

false

是可证明的。这意味着

aValidInput

永远不会成立。 Dafny 使用前缀谓词来定义最小/最大谓词。对于最小谓词，这意味着存在序数

k_

，最小谓词为真。请查看

paper

的Working with Extreme Predicates部分。如果您展开

aValidInput

的最小谓词前缀的定义，您将看到它始终是

false

。

对于无限流的推理，应该使用最大谓词。正如人们所希望的那样，对于任意数量的流展开都是如此。