title: Dafny: How can I quantify over the "contents" of a codatatype?
body: <p>Background: I am trying to write parser combinators in Dafny. This requires working on very long lists which I do not want to fully compute unless they are needed, so I am using an <code>IList</code> instead of a <code>seq</code> in order to simulate lazy evaluation. The problem which I am having is that I cannot find a way to express an equivalent to <code>forall x in sequence</code> when working with <code>ILists</code>.</p>
  <p>I'm defining <code>IList</code> in the same way as Dafny's documentation and tests:</p>
  <pre><code>codatatype IList&lt;T&gt; = Nil | Cons(head: T, tail: IList&lt;T&gt;)
  </code></pre>
  <p>I want to define an <code>fmap</code> function over <code>IList</code>s which allows partial functions. Here is my initial (incorrect) implementation:</p>
  <pre><code>function method fmap&lt;S, T&gt;(list: IList&lt;S&gt;, fn: S --&gt; T): IList&lt;T&gt;
  {
    match list
    case Nil =&gt; Nil
    case Cons(s, rest) =&gt; Cons(fn(s), fmap(rest, fn))
  }
  </code></pre>
  <p>This does not work, because the precondition to <code>fn</code> might not hold, and this is the root problem I'm trying to solve.</p>
  <p>I tried to define a copredicate to express the concept of &quot;forall&quot; on infinite lists, and use that:</p>
  <pre><code>greatest predicate IListForall&lt;T&gt;(list: IList&lt;T&gt;, fn: T -&gt; bool) {
    match list
    case Nil =&gt; true
    case Cons(head, rest) =&gt; fn(head) &amp;&amp; IListForall(rest, fn)
  }
  
  function method fmap&lt;S, T&gt;(list: IList&lt;S&gt;, fn: S --&gt; T): IList&lt;T&gt;
  requires IListForall(list, fn.requires)
  { /* body unchanged */ }
  </code></pre>
  <p>This makes <code>fmap</code> verify, but when I try to use <code>fmap</code> I can't find a way to make this precondition satisfied. It comes up when I try to define a mapping function which works on lists containing a certain type:</p>
  <pre><code>datatype Container&lt;T&gt; = Container(value: T)
  
  function method fmapContainers&lt;T, U&gt;(cs: IList&lt;Container&lt;T&gt;&gt;, fn: T -&gt; U):
    IList&lt;Container&lt;U&gt;&gt;
  {
    fmap(cs, (container: Container) =&gt; Container(fn(container.value)))
  }
  </code></pre>
  <p>The invocation of <code>fmap</code> here gives me the error <code>possible violation of function precondition</code>. This doesn't seem right to me. <code>fn</code> is total, and so is the lambda that I'm passing to <code>fmap</code>, so I don't think there should be any precondition in play? I've attempted to write <code>fmapContainers</code> a few different ways with no success, which makes me think that I messed up from the beginning when I tried to express <code>forall</code> as a copredicate.</p>
  <p>Is there a better way to express <code>forall</code> than what I did?</p>
  <hr />
  <p>footnote: <code>fmapContainers</code> might sound useless, but it's the simplest form of my actual problem. To explain my motivation, here's the full implementation that I'm trying to get working:</p>
  <pre><code>datatype OneParse&lt;T&gt; = OneParse(parsed: T, remainder: string)
  datatype Result&lt;T&gt; = Failure | Success(forest: IList&lt;OneParse&gt;)
  
  type parser&lt;T&gt; = string -&gt; Result&lt;T&gt;
  
  function method fmapSuccess&lt;S, T&gt;(result: Result&lt;S&gt;, fn: S --&gt; T): Result&lt;T&gt;
    requires result.Success?
    {
      Success(fmap(result.forest,
        (one: OneParse&lt;S&gt;) =&gt; OneParse(fn(one.parsed), one.remainder)))
    }
  
  function method fmapParser&lt;T, U&gt;(p: parser&lt;T&gt;, fn: T --&gt; U): parser&lt;U&gt; {
    s =&gt; var result := p(s); match result
        case Failure =&gt; Failure
        case Success(forest) =&gt; fmapSuccess(result, fn)
  }
  </code></pre>
  <p>I think I can figure out how to make the full solution work on my own if someone provides tips for implementing <code>fmap</code> and <code>fmapContents</code>, so this is just for context.</p>