Proving false when using import-with

[ThatDaleMiller]

Put the following into a file named p_and_q.thm.

Type p  prop.
Type q  prop.

Theorem test : p = q -> false.
 intros. case H1.

Put the following into a file named ``p_is_q.thm''.

Type pq  prop.

Import "p_and_q" with p := pq, q := pq.

Theorem contradiction : false.
  assert pq = pq.
  apply test to H1.

Abella 2.0.8 happily accepts this proof of false!

The changelog entry that describes the import command with the feature to rename predicates requires that the predicates that are renamed must be undefined predicates and that the predicates that are substituted into those undefined predicates must be defined predicates. This latter restriction is not respected in the current implementation: note that pq is not defined.

The problem still exists if we define pq. That is, Abella will also accept the following file.

Define pq : prop by pq := true.

Import "p_and_q" with p := pq, q := pq.

Theorem contradiction : false.
  assert pq = pq.
  apply test to H1.

I believe that the fix would be to insist (using the symbols in the changelog) that the command

Import "thmfile" with id1 := defid1, ..., idn := defidn.

is only allowed as long as the defid1, ..., defidn are pairwise distinct. It seems that they can be defined or undefined.

[chaudhuri]

I believe this has already been fixed in master (8c86b5ae0473f957e06de5cc6d003b6ce66753c1).

[ThatDaleMiller]

Sorry that I had forgotten about this previous issue. I am glad to know it will be fixed in a new release.

[chaudhuri]

Closing this issue. We'll have a release "soon".