search

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

Weird interaction between subordination and schematic theorems #144

Open chaudhuri opened 1 year ago

chaudhuri commented 1 year ago

This is based on this thread on the mailing list started by Todd Wilson (@lambdacalculator). His example:

Kind t type.
% Close t.

Theorem member_prune[A] : forall E (L:list A), nabla (x:A),
  member (E x) L -> exists E', E = y\E'.
induction on 1. intros. case H1.
  search.
  apply IH to H2. search.

This fails unless the Close t is commented out. Obviously t can be introduced after the theorem is proved and there would be no error.