Inconsistency with lambda equality

[jad-hamza]

It seems there is a consistency issue with the equality used for terms, and the ones used for lambdas. In theorems, f1 and f2 are constant functions that return equal constants, so we can prove they are equal, using equalFunctions. But they are also structurally different, allowing us to assert(false).

Does Stainless use structural equality to compare lambdas? Could we use the same kind of equality across all types? Not sure what is the most appropriate definition for equality here. Do we want something extensional?

import stainless.lang._
import stainless.annotation._

object Equality {
  sealed abstract class Nat
  case class Zero() extends Nat 
  case class Succ(n: Nat) extends Nat

  def plus(a: Nat, b: Nat): Nat = a match {
    case Zero() => b
    case Succ(a2) => Succ(plus(a2,b))
  }

  @induct
  def plusZero(a: Nat) = {
    plus(a, Zero()) == a
  } holds

  def equalFunctions[X,Y](y1: Y, y2: Y) = {
    require(y1 == y2)

    val f1 = (x: X) => y1
    val f2 = (x: X) => y2

    f1 == f2
  } holds

  def theorem(a: Nat) = {
    val p = plus(a, Zero())
    val f1 = (x: Nat) => a
    val f2 = (x: Nat) => p
    assert(f1 != f2)
    assert(plusZero(a))
    assert(equalFunctions(a, p))
    assert(f1 == f2)
    assert(false)
  }
}

[samarion]

This issue was due to invalid let inlining causing the structure of f1 and f2 to be different in formulae when p was used only once. I fixed the issue in https://github.com/epfl-lara/inox/commit/e1de7fa92154b487c776e86acce084b18afb194b.

Note that the structures of f1 and f2 are the same (and the functions should therefore always be equal).