The Coq mailing list

[Abhishek Anand <abhishek.anand.iitg AT gmail.com>]

I have a parametricity-like program translation that produces theorems and their proofs.

Often these theorems have hypotheses that are not needed in their proofs,

in the sense that after fully normalizing the proof, the variable denoting the hypothesis is not

even mentioned in the proof. I want to identify and eliminate such hypothesis

from the theorem's statement.

However, naively doing the normalization blows up on bigger examples.

Is there a mechanism (e.g. a function in Coq's sources, or a tactic)

that can take a term in a context and do the reduction less naively in order to eliminate mentions

a given variable? For example, it can ignore subterms that don't even mention the variable.

Even If there isn't a function that does exactly what I want, it would be helpful for me to 

get pointers to functions that I could use in my implementation.

Thanks,

-- Abhishek

http://www.cs.cornell.edu/~aa755/