The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Abhishek, 

  I think the only existing versions of shrinking like this in Coq's codebase do not involve any reduction but work on a given, fixed term (and are hence much simpler).

Best,

-- Matthieu

On Fri, Feb 10, 2017 at 9:22 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

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/