Soundness issue with non-strict positive types and impredicativity of Boolean (or of choose realizability)

jad-hamza commented 6 years ago

Stainless is able to derive false in that example adapted from http://vilhelms.github.io/posts/why-must-inductive-types-be-strictly-positive/ (original source: Inductively Defined Types (COLOG-88), also discussed in [Coq-Club] Positivity and Elimination Principle: https://sympa.inria.fr/sympa/arc/coq-club/2012-01/msg00087.html)

I don't really understand the example, but the ingredients needed in Stainless are: non-strict positive types for A, and quantifiers/impredicativity of Boolean in p0

import stainless.lang._

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

  case class A(magic: (A => Boolean) => Boolean)

  // i(a) = \b. a == b
  def i[T](a: T): T => Boolean = (b: T) => a == b

  def f(p: A => Boolean): A = A(i(p))

  // notContained is the predicate used for the existential formula p0
  def notContained(x: A, p: A => Boolean) = f(p) == x && !p(x)

  // paradoxical p0 and x0; p0(x0) can be neither true nor false
  def p0(x: A): Boolean = exists((p: A => Boolean) => notContained(x,p))
  val x0: A = f(p0)

  // simple lemma about the predicate `notContained`
  def lemma(x: A, p: A => Boolean) = {
    require(!notContained(x,p) && f(p) == x)

    p(x)
  } holds

  // Stainless can prove lemma1 without the require, is that normal?

  // we can then prove that p0(x0) implies !p0(x0)
  def lemma1() = {
    require(p0(x0)) 
    !p0(x0)
  } holds

  // and vice versa
  def lemma2() = {
    require(!p0(x0))
    assert(forall((p: A => Boolean) => !notContained(x0,p)))
    assert(!notContained(x0,p0))
    assert(lemma(x0,p0))

    p0(x0)
  } holds

  def theorem() = {
    // since lemma1 is clear for Stainless, only lemma2 is required here
    assert( 
      if (p0(x0)) lemma1()
      else lemma2()
    )
    assert(false)
  }
}

Edit: added an assert in theorem to prevent the if then else from being simplified away.

vkuncak commented 5 years ago

This should be resolved in #452 ?

jad-hamza commented 5 years ago

Yes, at the moment #452 rejects all non strictly positive types. This can be relaxed by allowing them and then forcing the user to use explicit indices when folding/unfolding an A (and only allow the generalization rules, without indices, for types that are strictly positive).

jad-hamza commented 5 years ago

Here is another example, which doesn't use non-strict positive types but uses forall and choose:

import stainless.lang._
import stainless.proof._

object ForallBool {
  def isEmpty[T]: Boolean = forall((x: T) => false)

  case class A() {
    require(isEmpty[A])
  }

  def isEmptyImpliesFalse(): Unit = {
    require(isEmpty[A])
    val a = A()
    check(false)
    ()
  } ensuring(_ => false)

  def nonEmptyImpliesFalse(): Unit = {
    require(!isEmpty[A])
    val a = choose((x: A) => true)
    assert(isEmpty[A])
    check(false)
    ()
  } ensuring(_ => false)

  def proveFalse() = {
    if (isEmpty[A]) isEmptyImpliesFalse()
    else nonEmptyImpliesFalse()
    assert(false)
  }
}