destruct/case transformations incorrectly handle polymorphic formulas
The transformations case
and destruct
don't take into account the fact that the formula they are applied to can be implicitely quantified over a type variable.
This allows us to prove false
in the following ways :
-
apply
case (forall x y : 'a. x = y)
and pass the resulting tasks to Eprover -
first prove that
(forall x y : 'a. x = y) \/ (not forall x y : 'a. x = y)
(by calling CVC4 for example), applydestruct
to this hypothesis and pass the resulting tasks to Eprover
What's happening ?
The formula forall x y : 'a. x = y
should be understood as forall 'a. forall x y : 'a. x = y
. When we apply case
on this formula, the negation incorrectly goes under the type quantification in the second task.