The Coq mailing list

[Jacques-Henri Jourdan <jacques-henri.jourdan AT normalesup.org>]

What would happen if you tried to unify your term with an evar that forbids this hypothesis?

On 02/13/2017 04:31 PM, Matthieu Sozeau wrote:

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/