A BUG that unexpectedly unifies term with arbitrary equality

[Jinxu Zhao]

Dear all,

I just found a bug during development, and here is a simple example to illustrate that.

Welcome to Abella 2.0.6.

Abella < Kind ty type.

Abella < Type i ty.

Abella < Type j ty.

Abella < Theorem bad : forall A, A = i.

============================

 forall A, A = i

bad < intros.

Variables: A

============================

 A = i

bad < assert A = i -> true.

H1 : i = i -> true

============================

 i = i

bad < search.

Proof completed.

It seems that any assertion with a unification as its condition (at any position) could cause this bug.

Best,

Jimmy

[Yuting Wang]

It looks like the bug is introduced between v2.0.4-b2 and v2.0.4. Before v2.0.4-b2 the example would not pass.

I run the following command and find out that there are a lot of changes to 'search' between v2.0.4-b2 and v2.0.4:

 [66] → git log --pretty=oneline v2.0.4...v2.0.4-b2
68771ed515825364b970881a84016a0cc11f204e (tag: v2.0.4) 2.0.4 release
76dce8c31be3418982f5d2124de19c679d9ad962 Non iterative use of search depth bound
9cd9d9c9fa125bbcb2404f12c1689ff34e4b200b Make tests work
a14825a888160fd7ec2662c8d718c5750c0f6e3a search: handle false-left correctly
2e51d51d9fa405539d6c031a0eb332e77f9f929c Making the fcurry example more "standard"
606e0869aca2b884fab2022a3dbe0ebc8b389a35 Shorten absolute paths in messages wrt load_path
979642574fd5729c8e04ab6d875da6310e521924 Added Ahn's example of Curry-style System F
b9837f4bdcabe2991c46d661a328ac7a398a41bc search: refactor to avoid name clashes
d74c4d178a1510a2535f0bed933d39a2e03336e3 search: asynchrony on new assumptions
f98cca3e5efec0613c9f2b3e06f4e103d67625e9 Removed an example that uses quantification over the 'o' type in specifications which is not supported by Abella.
8ec704435794949f11170fa303744a9be0070da6 Improve error messages for Split and Show.

My conjecture is that with some of these changes, some failed cases of search do not properly rewind the proof state after failure. Maybe Kaustuv has more insight on this since he made most of those changes (except one by Rob Blanco).

- Yuting

--
You received this message because you are subscribed to the Google Groups "Abella" group.
To unsubscribe from this group and stop receiving emails from it, send an email to abella-theorem-p...@googlegroups.com.
To post to this group, send email to abella-the...@googlegroups.com.
Visit this group at https://groups.google.com/group/abella-theorem-prover.
For more options, visit https://groups.google.com/d/optout.

[Kaustuv Chaudhuri]

Thanks for the report. This is fixed now in master.

https://github.com/abella-prover/abella/issues/113

Since this is a soundness bug, I'll make a bugfix release shortly.

Kaustuv