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

The exists tactic does not do capture-avoiding substitution #22

Closed chaudhuri closed 10 years ago

chaudhuri commented 10 years ago

Consider the following Abella development.

Kind i type.

Theorem foo : exists (x:i), exists y, x = y.
assert exists (y:i), y = y.
case H1. exists y.

The final exists y produces the obligation exists y, y = y instead of the obligation exists y1, y = y1.

This bug is reported by @matteocimini.