Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

"search" is inconsistent on list of nominal constants #71

Closed
MortenRhiger opened this issue Dec 16, 2016 · 2 comments
Closed

"search" is inconsistent on list of nominal constants #71

MortenRhiger opened this issue Dec 16, 2016 · 2 comments
Assignees
Labels

Comments

@MortenRhiger
Copy link

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

Kind t type.
Type f t -> o.

Abella (unexpectedly) proves this theorem with just an application of the search tactic:

Theorem bug : forall A, member A (f n1 :: nil) -> member A (f n2 :: nil).
search.

This results in inconsistencies. Indeed, we can (as expected) prove that no element can be a member of the two singleton lists mentioned above:

Theorem ok : forall A, member A (f n1 :: nil) -> member A (f n2 :: nil) -> false.
intros. case H1. case H2. case H3. case H2. case H3. case H3.

But then

Theorem proof_of_false : false.
assert member (f n1) (f n1 :: nil). apply bug to H1. apply ok to H1 H2.
@chaudhuri chaudhuri added the bug label Dec 16, 2016
@chaudhuri
Copy link
Member

Thanks. The theorem bug should not be proved by search.

@chaudhuri chaudhuri self-assigned this Dec 16, 2016
@MortenRhiger
Copy link
Author

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

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Projects
None yet
Development

No branches or pull requests

2 participants