The Coq mailing list

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

Thanks everyone for the suggestions.

Jacques: Yes, I am using unification to produce the new proof. However, before normalization, the unification fails with an error saying that it cannot instantiate the evar with .. because the unused var is not in its scope.

However, unification succeeds after I manually fully normalize. 

Can the unification function be tuned to try more reduction before giving up?

Currently, I am doing the unused-hypothesis removal manually in Ltac and my script looks like:

eexists.

Fail reflexivity. (* error : Unable to unify "?f" with "fOld" (cannot instantiate "?f" because 

... is not in its scope: available arguments are .....) *)

lazy. (* if lucky, it succeeds after taking a long time, all the RAM, and "ulimit -s unlimited" *)

reflexivity (* succeeds *)

Defined.

-- Abhishek

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

On Mon, Feb 13, 2017 at 11:10 AM, Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr> wrote:

Where I wrote "faster" I meant "farther", ie Matthieu's reply about checking recursively.

Gaëtan Gilbert

On 13/02/2017 16:45, Gaetan Gilbert wrote:

There's Indtypes.weaker_noccur_between:

(* [weaker_noccur_between env n nvars t] (defined above), checks that
   no de Bruijn indices between [n] and [n+nvars] occur in [t]. If
   some such occurrences are found, then reduction is performed
   (lazily for efficiency purposes) in order to determine whether
   these occurrences are occurrences in the normal form. If the
   occurrences are eliminated a witness reduct [Some t'] of [t] is
   returned otherwise [None] is returned. *)
let weaker_noccur_between env x nvars t =
  if noccur_between x nvars t then Some t
  else
   let t' = whd_all env t in
   if noccur_between x nvars t' then Some t'
   else None

You could go faster by iterating on subterms if variables still occur after the whd.

Gaëtan Gilbert

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.

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/%7Eaa755/>