Soundness issue when quantifying over tuples

[jad-hamza]

On this file, Stainless/Inox returns a wrong counter-example to lemma. The problem disappears if we replace forall( (t: (A,A,A)) => with forall( (x: A, y: A, z: A) =>

import stainless.lang._

object Associativity {

  def isAssociative[A](f: (A,A) => A): Boolean = {
    forall( (t: (A,A,A)) => {
      val (x,y,z) = t
      f(x,f(y,z)) == f(f(x,y),z)
    })
  }

  def lemma[A](f: (A,A) => A, x: A): Boolean = {
    require(isAssociative(f))

    f(f(x,x),x) == f(x,f(x,x))
  } holds

}

[samarion]

Fixed in https://github.com/epfl-lara/inox/commit/30cedecb826b8c93f80d11e46c156213cd083aec (note that this definition of isAssociative doesn't fit in the fragment for which Inox will find valid models). If you think this is a useful pattern, we could potentially add some rewriting steps to bring it into a form Inox likes better.