Forall quantifiers and Booleans

[jad-hamza]

I'm trying to clarify something about quantifiers, and the fact that we consider them as Boolean's. We are considering an "impredicative" forall quantifier, where when we create a Boolean x that is a forall quantifying over all Boolean's b, we are also quantifying over x itself.

I wonder whether this can lead to inconsistencies in our setting, perhaps with something similar to the example below. That example isn't accepted by Stainless (which is good!) but I'm not sure it is for the good reasons (there are various problems due to the use of choose and due to higher-order contracts that make the example fail).

Ideally, assuming we only have total functions, where should Stainless detect that this program is faulty? As @ravimad said, the extract function is highly suspicious! (and gets rejected for now which is good)

import stainless.lang._

object ForallBoolean {
  def exists[T](p: T => Boolean) = {
    !forall((t: T) => !p(t))
  }

  def isForall(b: Boolean, p: Boolean => Boolean): Boolean = {
    b == forall((x: Boolean) => p(x))
  }

  def extract(b: Boolean): Boolean => Boolean = {
    if(exists((p: Boolean => Boolean) => isForall(b,p)))
      choose((p: Boolean => Boolean) => isForall(b,p))
    else
      _ => true 
  }

  val bb: Boolean = forall((b: Boolean) => !extract(b)(b))

  def theorem() = {
    val x = extract(bb)(bb) // is equivalent to !extract(bb)(bb)
    assert(x == !x)
    assert(false)
  }
}

[jad-hamza]

I've retried running that example today but there is an internal error:

[Internal] Error: key not found: x$71. Trace: [...] [Internal] key not found: x$72 [Internal] Please inform the authors of Inox about this message

[samarion]

I can't reproduce your error with the current Stainless. Stainless fails to verify the assertion assert(x != x) for me.

[jad-hamza]

Yes for me too, the internal error is gone!

About the original issue, I think I was confused. I wanted to define extract(bb) to be equal to (b: Boolean) => !extract(b)(b) by definition, but that is not the case. We just know the result of extract(bb) is some p such that isForall(bb,p) holds.