When search is attempted in assert, on success the assertion is added in the same state as the search success. This was not an issue in the past because search would never instantiate variables. However, since Abella version 2.0.4 we do some left-asynchrony in search (with recursive_metaterm_case), so this invariant no longer holds. This causes the following invalid proof to be accepted.
Kind i type.
Type a i.
Theorem foo : forall A, A = a.
intros.
assert A = a -> true.
search.
This issue was flagged by Jinxu Zhao on the Abella mailing list.
When search is attempted in
assert, on success the assertion is added in the same state as the search success. This was not an issue in the past becausesearchwould never instantiate variables. However, since Abella version 2.0.4 we do some left-asynchrony in search (withrecursive_metaterm_case), so this invariant no longer holds. This causes the following invalid proof to be accepted.This issue was flagged by Jinxu Zhao on the Abella mailing list.