coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Courtieu <Pierre.Courtieu AT cnam.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] name management in highly automated proofs
- Date: Tue, 31 Aug 2021 00:43:34 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Pierre.Courtieu AT cnam.fr; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-il1-f180.google.com
- Ironport-hdrordr: A9a23:ZIzeu6NPPTE/+sBcTvijsMiBIKoaSvp037BN7TEJdfU1SL3/qynApoV46faZskdzZJhko7C90cq7L080l6QFhLX5VI3KNGLbUSmTTb2KhrGSpwEIdReOkdK1Fp0MT0G9MrfN5JRB4foSKTPWL+od
- Ironport-phdr: A9a23:vzT34BPmyPvG1NABY+sl6naVDRdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv60r3QaCANqTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yfy+94fXbglVizawYbF/JwiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjULxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrVr0/Ryis4Ll3Rx/pkCcHNiA28GfLisxrkalXpAutqwFjz4LIZY2YMud1cKHActMAXWdOUchRWC5BDI2ybIUBEvQPMvpXoYTmu1sOtAGzCRWwCO/zyDJFgGL9060g0+QmFAHLxBYuH9MQv3TOttX6KroZXP6yzKnV1zXDc/JW1ing6IPVdR0vu/CMUqxqccrL10YjDR3IjlKNqYz/IzOV1/oCs3WA4uV8U+KgkWsnpxt/oji138ohjJTCiY0JxF7e7yp53Jo1KsOiSE59edOqHptduzyUOYZ4Qs4sTGBltik6x7AGp5O2cjUHxpo7yhPbaPGLboyF7xDtWeiRLzl0mm5pdr27ihuw9UWtzunxW8+p21hEqSpFl8PDtnEL1xHL5ciHS+d9/ke82TmUzQzc9uZEIUUsmaXHLJ4h2LgwmYQXsUTHBCP5hlj5jLKQe045+eao8/zqbqv6qpKYLYN5iQHzPr4zlsG+AOk0KBUCUmuH9em6ybbt51f2QK9Qgf0ziqTZsI7VJcAcpqOhBg9ayIcj6xKmAzen1NQUgGALLFxYdB+Ek4TlIV7OIPf/Dfewh1Sjji1nyOzBPr3kGpnNL37Dn6n9fbtl9UJQ1A4+wcpc6p9UEL0NPfP+V07ruNDFDRI1LxS4w+P9B9V80oMeV3iPAqicMK7KqV+I5/wgI/OWZIALojryN/8l5+P0jX8lmF8SY7Sp0IAYaHC9BPtmIkGZbWDwjdcGFGcGphA+Q/DyiF2eTT5TYG6/UL475jEiEY6pEYPDRp22j7Gaxye6HphWZnhcBVyWEHfocZ+EW/YWZy6ILM9hiG9Mab/0YIg4nTqqqQWyn7FgN6/f/jASnZPlztl8oePJw0Ic7ztxWvyc3nuXQilfmX4SWz47wegrmU1w0E2Ol4N/nuZEFNFOz/hPWwJ8O4SKnL8yMMz7Rg+UJoTBc12hWNjzRGhpFrrZLPcBZk98H5OpiRWRhkJC4pcQnr2PQZ0wq+fShiipYcl6zHnC2e8qiFx0GqOn0EWtgKd6sQbJVdahrg==
Hi Abhishek,
It is indeed difficult to write script robust against changes. As
λ-termers we are naturally inclined to provide names by hand, but I
think this is not appropriate for 1) the imperative nature of ltac, 2)
the "change in my definitions" problem.
There are three solutions I am aware of:
1) call a hypothesis by (a pattern matching) its type:
https://github.com/pedagand/coq-label
2) Use only automated tactic (à la CPDT)
3) Or do sometinh like what I did there
https://github.com/Matafou/LibHyps which looks very much like what you
suggest: an automatic, customizable, naming system for "new"
hypothesis. Pure ltac currently. Remarks and suggestions most welcome.
Best
P.
Le lun. 30 août 2021 à 19:21, Abhishek Anand
<abhishek.anand.iitg AT gmail.com> a écrit :
>
> In my experience, the more automated a proof is, the more nameless it gets:
> the manual or automation steps don't care about what names get assigned to
> variables/hypotheses in the context and if some hypothesis has to be
> identified, it is done by shape matching, not by names.
>
> That said, some people see some value in having complex automation tactics
> preserve the user-chosen names as much as possible and perhaps also choose
> names of new hypotheses in a predictable way, perhaps based on the existing
> names. The simplest example is perhaps:
> destructing H: A /\ B could result in
> Hl: A
> Hr: B
> But doing this is complex in most cases, e.g. when a lemma is applied to
> multiple hypotheses to produce a new one.
>
> Does anyone have experiences to share trying to design complex automation
> tactics that preserve the user chosen names as much as possible? Or is
> there some fundamental conflict between the degree of automation and the
> reliability of names of hypotheses?
>
> (In general, I wish there was more science about the art of writing Coq
> proofs robust against "future changes": I see a lot of debates about it but
> not much hard evidence)
>
> Thanks,
> -- Abhishek
> http://www.cs.cornell.edu/~aa755/
- [Coq-Club] name management in highly automated proofs, Abhishek Anand, 08/30/2021
- Re: [Coq-Club] name management in highly automated proofs, Pierre Courtieu, 08/31/2021
Archive powered by MHonArc 2.6.19+.