Need to repeat function body to prove

[txiang61]

Dafny version

4.4.0

Code to produce this issue

lemma Proof<A>(x: seq<A>, b: A) {
  if |x| == 1 {
    assert x == [x[0]];
    var p := a => [b];
    // assert p(x[0]) == [b]; // useless

    // var _ := Concat(Map(x, p)); // useless

    assert Map(x, p) == [[b]]; // This line and the next are both neccessary
    assert Concat([[b]]) == [b];

    // The following assertions can replace the two previous assertions
    // assert Foo(x, p) == Concat(Map(x, p));

    assert Foo(x, p) == [b];
  }
}

function Foo<A>(actions: seq<A>, b: A -> seq<A>): seq<A> {
  Concat(
    Map(
      actions,
      b
      ))
}

function Map<T, U>(s: seq<T>, f: T -> U): (res: seq<U>) {
  if s == [] then []
  else [f(s[0])] + Map(s[1..], f)
}

function Concat<A>(s: seq<seq<A>>): (res: seq<A>) {
  if s == [] then []
  else s[0] + Concat(s[1..])
}

Command to run and resulting output

No response

What happened?

Sometimes copying over the function body can prove the assertions. The example above is a short and simple but in practice the function aren't as small as the one above. The real pain comes from having to copy over the whole function body in order to prove some assertions.

What type of operating system are you experiencing the problem on?

Mac

[dschoepe]

Verifies successfully for me using 4.7.0

[robin-aws]

@txiang61 - just to confirm, are you stuck on Dafny 4.4 or can you upgrade as @dschoepe suggests?