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

No "Contexts don't match" error #78

Closed lambdacalculator closed 7 years ago

lambdacalculator commented 7 years ago

Attached minimal example that should produce "Contexts don't match" error, but apply is accepted.

test.zip

chaudhuri commented 7 years ago

Thanks. This looks like a serious bug.

chaudhuri commented 7 years ago

Actually, wait, this is not a bug at all since G is not constrained in any way!

Basically, what Abella does is implicitly apply monotonicity to use, effectively, the equivalent of:

apply IH to H4 H6 with G = (of n1 T2) :: (of n1 T1) :: G.

If you had constrained the shape of G with a ctx definition, then you would not be able to do this because obviously this is not a well-formed context.

lambdacalculator commented 7 years ago

I see, thanks. Sorry for the false alarm!