The Coq mailing list

[Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>]

On 10/02/2017 21:21, Abhishek Anand 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.

Just a naive question: why don't you instrument the parametricity
translation not to generate these hypotheses in the first place? I think
it's rather easy to do, at least with the Bernardy-Lasson translation.
If so, what you're looking for is an XY problem...

PMP

Attachment: signature.asc
Description: OpenPGP digital signature