coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] detecting opaque defintions that block computing
Date: Fri, 26 Jun 2020 16:05:24 -0700
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-io1-f49.google.com
Ironport-phdr: 9a23:3qZvGxKagUDKQMyM5NmcpTZWNBhigK39O0sv0rFitYgeI/nxwZ3uMQTl6Ol3ixeRBMOHsq8C0ruM+Pm+EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQpFiCe9bL9oMRm7qRvdusYLjYZjN6081gbHrnxUdupM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTYQguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhSEaPDA77W7XkNR9g61VoB2jpxJxzY3abpyLOvViZa7SZ88WSHBbU8pNSyBMAIWxZJYPAeobOuZYqpHwqkcVohu+BAmsH+PvxSFLhnTrwaA61f4uEQfb0wc9GN8Bqm/brNX0NKcJUeC60qrIwS/ZYPNQwzj97pXHfgogofGNQbJwftHcyUYqFwzfj1WQrZbpMC+S1uQIqmWW6fdrWu2zhWA9sQ5xviSvydk2ionPno8YzlDJ+TlnzYorK9O1Rk51bN+6HJdMqi2UN4t4TMM8T2xmpCs31rMLtYOmcSQUypkq2wLSZv2IfYWH4h/uSeecLDFlj3xrf7K/ggy98UmmyuDkSsa010xKrixbndnIsnABzQLc5dWaSvZ740yv2i6P2hjN5u1YJU04j6nWJp47zrItl5cesF7PEyDylUjwkaSYbF8r+vKy5OTierjmpoGTN4tzigzmN6QhgM2/AeAhPggPWGiX5P2w1LPs8ED9WrlKgfo2kq7WsJDeO8sXvLK2AwhQ0oo76ha/CSmp0MgAkHUZMF5IfAiLgovpNl3UPfz1DPayj06jnTpv3/zGO6fuApTJLnjNirfherN95lZGxwUozdBf5olUCrEfL/LwQEP+rtrYAQU/MwOp2ernCdR91p8RWW+UDa+ZNbndsV6M5u41P+aMY4oVtC7nK/c5//7ukWM5mVgFcKa12psXcWm0EehiI0WEenXhmcwBEGcPvgomVuPmklyCUThJZ3azRa0w/D87CJj1RbvEE4uqmfmK2DqxVsldYXkDAVSRG1/pcZ+FUrECcnTBDNVml2ktX7igUI8s1lmHsgb8x/IzJ+DU+zYYuJGl3d584eGVlBAu+hR7Cs2c1yeGSGQizTBAfCM/wK0q+R818VyEy6Ut26UFR+wW3OtAV0IBDbCZz+F+DIqvCAfIf9PMSVH/B9v6UHc+SdU+x9JIaEF4SY370kLzmhGyCrpQrISlQYQu+/uFjXf0Lsd5jX3B0ft51gh0co50LWSjw5VH2U3WDo/NnV+ekv/zJ6sZ1S/JsmyEyDjXsQ==

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