search

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

"search" does not ensure that all logical variables are instantiated with ground terms #105

Closed yvting closed 6 years ago

yvting commented 6 years ago

Consider the following examples:

Kind i type.

Theorem foo : exists (x:i), x = x.
search.

Theorem bar : exists (x y:i), x = y.
search.

For 'foo', search will generate an logical variable for 'x' and consider the equality to be provable.

For 'bar', search will generate logical variables for 'x' and 'y' and unify 'x' with 'y'. Again, the goal is proved without checking that 'x' and 'y' are instantiated to ground terms.

chaudhuri commented 6 years ago

As far as I can tell, this is not a bug since you can use nominal constants in both cases. If we ever get around to differentiating between nominal and non-nominal types, this may be an important thing to watch out for.

yvting commented 6 years ago

Yes. You are right. Abella currently treats every type as a nominal type. Therefore, a unifier for logical variables can always be turned into a solution by using nominal constants.

I was worried that top-level logical variables will result in unsound proofs. It looks like not a problem for the 'search' tactic.

yvting commented 6 years ago

Close this issue since it is not a real problem for now.