coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Cc: Coqdev <coqdev AT inria.fr>
- Subject: Re: [Coq-Club] [coqdev] efficiently reducing away mentions of a variable
- Date: Tue, 14 Feb 2017 07:58:03 -0500
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f170.google.com
- Ironport-phdr: 9a23:ecZlwxTSnw/5PwjxtJ83i94o9Npsv+yvbD5Q0YIujvd0So/mwa67bReN2/xhgRfzUJnB7Loc0qyN4v2mATRLu8zJ8ChbNscTB1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Izkn9y1rpbUekBDgCe3Ked5KwzzpgHMvOEXh5FjI+A/0E2ajGFPfrF/z2NpPlKenF7V4M628NY3+i5Quukh+s0GWKPzeah+TL1EAxwpNmk04IvgshyVHljH3WcVTmhDykkAOAPC9hyvBpo=
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/>
- [Coq-Club] efficiently reducing away mentions of a variable, Abhishek Anand, 02/10/2017
- Re: [Coq-Club] efficiently reducing away mentions of a variable, Matthieu Sozeau, 02/13/2017
- Re: [Coq-Club] efficiently reducing away mentions of a variable, Jacques-Henri Jourdan, 02/13/2017
- Re: [Coq-Club] efficiently reducing away mentions of a variable, Enrico Tassi, 02/14/2017
- Re: [Coq-Club] efficiently reducing away mentions of a variable, Jacques-Henri Jourdan, 02/13/2017
- Message not available
- Message not available
- Re: [Coq-Club] [coqdev] efficiently reducing away mentions of a variable, Abhishek Anand, 02/14/2017
- Message not available
- Re: [Coq-Club] efficiently reducing away mentions of a variable, Matthieu Sozeau, 02/13/2017
- Re: [Coq-Club] [coqdev] efficiently reducing away mentions of a variable, Pierre-Marie Pédrot, 02/14/2017
Archive powered by MHonArc 2.6.18.