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

Error in renaming of bound variables in metaterms #106

Closed yvting closed 6 years ago

yvting commented 6 years ago

Renaming of bound variables in a metaterm does not check clash of names between renamed variables and top-level constants

Consider the following (contrived) example:

Set instantiations on.

Kind i   type.

Type p2   i.

Theorem rename_failure: forall (p:i), 
   false \/ forall (p:i), false \/ forall (p1:i), p2 = p1.
intros. right. intros. right. intros. search.

To prove rename_failure, the first intro introduces a new eigenvariable named p. The second intro introduces a variable named p1 which is the first fresh name that does not conflict with p. This triggers the renaming of bound variable p1. Because the renaming process does not consider conflicts with top-level constants, it wrongly decides that p2 is the first fresh name that does not capture free variables after renaming. As such, the final goal becomes forall (p2:i), p2 = p2 which is provable.

Using rename_failure, we can easily prove false, as follows:

Theorem all_eq : forall (p:i), p2 = p.
intros. apply rename_failure with p = p2.
  case H1. apply H2 with p = p2. case H3. 
  apply H4 with p1 = p. search.

Type q    i.

Theorem unsound: false.
assert (p2 = q -> false). backchain H1. backchain all_eq.
yvting commented 6 years ago

The bug is caused by the function replace_metaterm_vars in metaterm.ml. I have pushed a fix to the branch renaming-fix.

  1. I have added a function named find_free_constants to compute the top-level constants in a metaterm.
  2. I have given a new implementation to replace_metaterm_vars. First, it makes use of find_free_constants and other functions to compute free variables of metaterms. Second, the new implementation divides free variables into two parts: the first contains free variables that are unchanged and the second contains free variables that are renamed or substituted for. Using those information, it decides whether to rename bound variables and what they should be renamed into to avoid conflicts. See the comments in code for details.

Let me know if you have any question.

BTW, I feel that it is very cumbersome to use explicit names for bound variables in metaterms. It seems better to represent them using debruijn indexes, like in terms.

chaudhuri commented 6 years ago

I've tried to De Bruijn-ify metaterms a number of times, but never had the tenacity to see it through. I think it is a good idea nevertheless.