coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] detecting opaque defintions that block computing

From: "jonikelee AT gmail.com" <jonikelee AT gmail.com>
To: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] detecting opaque defintions that block computing
Date: Fri, 26 Jun 2020 20:24:49 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qt1-f172.google.com
Ironport-phdr: 9a23:k4ua1RfCVwSjEq17FwVIQGHAlGMj4u6mDksu8pMizoh2WeGdxcW9Zh7h7PlgxGXEQZ/co6odzbaP7ua5CDZLu8vJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MRW7oR/MusQSn4duJbg9xxvUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+vqRxxzZDJbo+WNvV+cKTTctwGSmRORctRSy5MD5mgY4YVE+YNI+BVpJT9qVsUqhu+ABGhCO3tyj9PgH/23K463PolEQ7YwgMtBN0OsHHOo9X0MKceS/y6zK7NzTnNcvhb3jX96I/OchAgovGDQ7ZwftTPxkQ0GAPFi0+fqY3hPz+PyusNtG2b4vNmWOmyhGEptxt/rSKzxscwlIbJnIQVx0jE+Ch3wIs5O8G1RFBnbdOgHpVdqyKXOYt4TM4/TGxkpiQ3x7kJtJO/fCUHyooqywPDZ/GbbYWG7AzuWeeRLDpmgn9uZbyxhxG38Ue6y+38UNG530pNripflNnDqHQN1xjJ5seZV/R940Gs0iuM2QDL8uxIP1w4mK7BJ5MiwrM8jIcfvEXfEiPshUn7jrGael069uWp9+jrf7DrqoKYOoBojwzzPaUjltCjDek9PQUBRXSX9vq52bL/4UL0QKtGg/gqnaTWvpDaK8EWpqCnDABP3Ysu7gywAjOn3dkXm3QMMUhLdwidj4fzPlHDOPD4Aum7g1SriDprwurJPrzlApnUN3jDjKrtca9z60JBygc/08pT551TCrEGL/LzXlH+uMbEAR8+Ngy42+fnCNNj2YMCQW+DHLOVPafIvVKL5u8jOfSAaY4JtDrnNvQo5eDigWc8mVAHfKmp2ZUXaGq/HvRjO0iZY33sgtEAEWcJoAU+SPLlh0OZXD5cYna9RaM85jUhBI26CofDQ5ihgKad0yejAp1WemdGB0iQHnfvboWIQusDaCaPIsB6iTEETrigS4o51R60rgP6yrxnLvDV+iICr57j2sJ1tKXvkkQb/zx1FMSQ0CmkSWhykitcTjU23bt/rE87w1GK16Q+gv1EGvRc4vpIVkExMpuKnMJgDNWnEADGeNaKRVKrT/2pBDgwSpQ6xNpEKxJ/HNOjjR3H0ieCDLoclrjND5sxpPGPl0PtLtpwni6VnJIqiEMrF5MWZD+Ww5Vn/g2WPLbn1kCQlqKkb6MZhXef+2KKzG7It0ZdAlcpDff1GEsHb06TluzXo1vYRub3W7siOwpFj8WFL/kSM4C7vRB9XP7mfe/mTSexlmO3X0jaw7qNaM/zZzxY0nyCUg4LlAcc+XvAPg87VH+s

I was hoping for an existing solution, rather than wishing for a
possible one. But, in the case of relevant wishes, mine would be for a
variety of opaqueness that would disallow unfolding but allow
computing. I think the fact that opaque functions can be extracted,
including those permanently opaque because closed with Qed, means that
there could be two varieties of opaqueness. One is what we have
now: an opaque function won't compute or unfold. But another would
share Qed's benefits over Defined, disallow unfolding, but allow
computing by way of some internal representation generated similarly to
extraction.

On Fri, 26 Jun 2020 16:05:24 -0700
Abhishek Anand <abhishek.anand.iitg AT gmail.com> wrote:

> More general variant that I wish Coq had:
> given a (possibly open) term, either tell me that no amount of
> unfolding (possibly after making transparent) will lead to a head
> normal form, or give me the smallest set (or at least a minimal set)
> of definitions to be unfolded that will guarantee head normal form
> (there is at least a bruteforce algorithm to solve this problem
> because the set of definitions in the term is finite).
> In the former case, suggesting a sequence of variable destructions
> that lead to head normal form would be nice but I don't know even any
> bruteforce algorithm for this problem; it seems hard to bound
> sequences of destructions.
>
>
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
>
>
> On Fri, Jun 26, 2020 at 3:25 PM jonikelee AT gmail.com
> <jonikelee AT gmail.com> wrote:
>
> >
> > Is there a way in Coq to detect which opaque functions used in
> > the definition of a transparent function will block computing with
> > the transparent one?
> >
> > Other than attempting to compute with test cases?
> >
> > If I Print Opaque Dependencies, that shows too much, as not all
> > dependencies are involved in computing.
> >
> > I think there used to be messages printed out during recursive
> > extraction when it encountered an opaque function, but I don't see
> > that anymore.
> >

[Coq-Club] detecting opaque defintions that block computing, jonikelee AT gmail.com, 06/27/2020
- Re: [Coq-Club] detecting opaque defintions that block computing, Abhishek Anand, 06/27/2020
  - Re: [Coq-Club] detecting opaque defintions that block computing, jonikelee AT gmail.com, 06/27/2020
    - Re: [Coq-Club] detecting opaque defintions that block computing, Gregory Malecha, 06/30/2020