SOUNDNESS BUG: `Import ... with` does not check that the replacements are distinct

abella-prover / abella

An interactive theorem prover based on lambda-tree syntax

https://abella-prover.org/

GNU General Public License v3.0

90 stars 18 forks source link

Closed chaudhuri closed 10 months ago

chaudhuri commented 10 months ago

Here is a proof of false:

A.thm

Type p, q prop.
Theorem diff : p = q -> false.
intros. case H1.

B.thm

Type r prop.
Import "A" with p := r, q := r.
Theorem bad : false.
apply diff to _.

Bug found in discussions with @innofarah and @thatdalemiller.