Assertion using higher-order functions and match doesn't go through

[jad-hamza]

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

object AssertedLemma {
  @extern
  def p(x: BigInt, y: BigInt, z: BigInt): Boolean = {
    (??? : Boolean)
  }

  @extern
  def lemma(l: List[(BigInt, (BigInt, BigInt))]): Unit = {
  }.ensuring(_ =>
    l.forall { (xyz: (BigInt, (BigInt, BigInt))) => xyz match { case (x, yz) => p(x, yz._1, yz._2) } }
  )

  def test(l: List[(BigInt, (BigInt, BigInt))]) = {
    lemma(l)
    assert(l.forall { (xyz: (BigInt, (BigInt, BigInt))) => xyz match { case (x, yz) => p(x, yz._1, yz._2) } })
  }
}

The assertion in test doesn't go through (timeout), while it should thanks to the postcondition of lemma.

[vkuncak]

This is due to lack of function extensionality. The following code does not work, but if you comment out @inline, it does.

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

object AssertedLemma {
  @extern
  def p(x: BigInt, y: BigInt, z: BigInt): Boolean = {
    (??? : Boolean)
  }

  @inline
  def check(l: List[(BigInt, (BigInt, BigInt))]): Boolean = {
    l.forall { (xyz: (BigInt, (BigInt, BigInt))) =>
      xyz match {
        case (x, yz) => p(x, yz._1, yz._2)
      }
    }
  }

  @extern
  def lemma(l: List[(BigInt, (BigInt, BigInt))]): Unit = {
  }.ensuring(_ => check(l))

  def test(l: List[(BigInt, (BigInt, BigInt))]) = {
    lemma(l)

    assert(check(l))
  }
}

[samarion]

This sounds like a bug in Inox function normalization, I'll have to take a look.