Dafny：我如何量化共数据类型的 "contents"？

Question

背景：我正在尝试在 Dafny 中编写解析器组合器。这需要处理非常长的列表，除非需要，否则我不想完全计算这些列表，因此我使用 IList 而不是 seq 来模拟延迟评估。我遇到的问题是，在使用 ILists.

时，我找不到表达等同于 forall x in sequence 的方法

我定义 IList 的方式与 Dafny 的文档和测试相同：

codatatype IList<T> = Nil | Cons(head: T, tail: IList<T>)

我想在 IList 上定义一个允许部分函数的 fmap 函数。这是我最初的（不正确的）实现：

function method fmap<S, T>(list: IList<S>, fn: S --> T): IList<T>
{
  match list
  case Nil => Nil
  case Cons(s, rest) => Cons(fn(s), fmap(rest, fn))
}

这行不通，因为 fn 的先决条件可能不成立，这是我要解决的根本问题。

我试图定义一个共谓词来表达无限列表上“forall”的概念，并使用它：

greatest predicate IListForall<T>(list: IList<T>, fn: T -> bool) {
  match list
  case Nil => true
  case Cons(head, rest) => fn(head) && IListForall(rest, fn)
}

function method fmap<S, T>(list: IList<S>, fn: S --> T): IList<T>
requires IListForall(list, fn.requires)
{ /* body unchanged */ }

这使得 fmap 验证，但是当我尝试使用 fmap 时，我找不到满足此前提条件的方法。当我尝试定义一个适用于包含特定类型的列表的映射函数时出现：

datatype Container<T> = Container(value: T)

function method fmapContainers<T, U>(cs: IList<Container<T>>, fn: T -> U):
  IList<Container<U>>
{
  fmap(cs, (container: Container) => Container(fn(container.value)))
}

这里调用fmap报错possible violation of function precondition。这对我来说似乎不对。 fn 是总的，我传递给 fmap 的 lambda 也是总的，所以我认为游戏中不应该有任何先决条件？我尝试用几种不同的方式写 fmapContainers 但没有成功，这让我觉得当我试图将 forall 表达为共谓词时我从一开始就搞砸了。

有没有比我做的更好的表达方式forall？

footnote: fmapContainers 可能听起来毫无用处，但它是我实际问题的最简单形式。为了解释我的动机，这里是我正在努力工作的完整实现：

datatype OneParse<T> = OneParse(parsed: T, remainder: string)
datatype Result<T> = Failure | Success(forest: IList<OneParse>)

type parser<T> = string -> Result<T>

function method fmapSuccess<S, T>(result: Result<S>, fn: S --> T): Result<T>
  requires result.Success?
  {
    Success(fmap(result.forest,
      (one: OneParse<S>) => OneParse(fn(one.parsed), one.remainder)))
  }

function method fmapParser<T, U>(p: parser<T>, fn: T --> U): parser<U> {
  s => var result := p(s); match result
      case Failure => Failure
      case Success(forest) => fmapSuccess(result, fn)
}

如果有人提供实施 fmap 和 fmapContents 的提示，我想我可以自己弄清楚如何使完整的解决方案工作，所以这只是为了上下文。

Answer 1

这里的问题是 greatest predicate (IListForall) 未证明函数 (container: Container) => Container(fn(container.value))。这很容易证明

greatest lemma IListForallLemma<T, U>(cs: IList<T>, fn: T -> U)
 ensures IListForall(cs, fn.requires)
{}

现在下面的代码片段验证。我已将 fmapContainers 从 function method 变为 method 以调用上述引理。

codatatype IList<T> = Nil | Cons(head: T, tail: IList<T>)

greatest predicate IListForall<T>(list: IList<T>, fn: T -> bool)
{
  match list
  case Nil => true
  case Cons(head, rest) => fn(head) && IListForall(rest, fn)
}

function method fmap<S, T>(list: IList<S>, fn: S --> T): IList<T>
requires IListForall(list, fn.requires)
{
  match list
  case Nil => Nil
  case Cons(s, rest) => Cons(fn(s), fmap(rest, fn))
}

datatype Container<T> = Container(value: T)

greatest lemma IListForallLemma<T, U>(cs: IList<T>, fn: T -> U)
  ensures IListForall(cs, fn.requires)
{}

method fmapContainers<T, U>(cs: IList<Container<T>>, fn: T -> U) returns (r: IList<Container<U>>)
{
  IListForallLemma(cs, (container: Container) => Container(fn(container.value)));
  r := fmap(cs, (container: Container) => Container(fn(container.value)));
}

Dafny：我如何量化共数据类型的 "contents"？

Dafny: How can I quantify over the "contents" of a codatatype?

dafny