Closed MortenRhiger closed 7 years ago
Thanks. The theorem bug
should not be proved by search.
A similar error can actually be produced without lists and nominal constants: We have
Theorem bug2 : forall A, nabla x y, (A = f x) -> (A = f y).
search.
even though
Theorem nominals_differ : nabla x y, f x = f y -> false.
intros. case H1.
Again it's easy to establish a contradiction:
Theorem ok2 : forall A, nabla x y, (A = f x) -> (A = f y) -> false.
intros. case H1.
The problem seems to be the universally quantified A
since neither of the following can be proved by searching:
Theorem not_provable1 : f n1 = f n2.
skip. % cannot search here
Theorem not_provable2 : nabla x y, f x = f y.
intros. skip. % cannot search here
In version 2.0.4 of Abella, the search tactic seems inconsistent when working with lists of nominal constants (or my understanding of the underlying logic is terribly wrong). With
Abella (unexpectedly) proves this theorem with just an application of the
search
tactic:This results in inconsistencies. Indeed, we can (as expected) prove that no element can be a member of the two singleton lists mentioned above:
But then