Decidability/computability of lambda equality hinders reasoning abilities

[romac]

Background: #62

In short, because lambda equality is assumed to be decidable within Inox' semantics, the assertion in the following testcase is deemed invalid unknown (with --check-models). That stems from Inox assuming that an implementation of bar could discriminate between k and x => k(x), and return a different result in each case. While that is possible in Scala because of reference equality [1], this is in general not something we want to support within Stainlesss' semantics.

abstract class Foo {
  def bar(f: Int => Int): Int
}

val k = (i: Int) => i

def test(foo: Foo) = {
  assert(foo.bar(k) == foo.bar(x => k(x))) // INVALID
}

We should thus (as discussed with @samarion) add a mode to Inox where lambda equality is deemed undecidable, and enable that mode when used through Stainless. See the corresponding issue in the Inox repository: epfl-lara/inox#87.

We therefore also need to check that user-land code does not rely on such semantics (ie. compare lambdas for equality).

• [1]

  case class Bar() extends Foo {
    def bar(f: Int => Int): Int = if (f == k) 0 else -1
  }

[romac]

@samarion Please feel free to edit/comment on this issue if I misunderstood/misrepresented the issue and potential solution.

[vkuncak]

Assuming lambda equality is actually very useful in reasoning about higher-order functions.
We may be encoding parameter passing through equalities or lets and we need to have at least some use of positive equalities in assumptions to get the expected proofs go through.