coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] option for simpl to never simplify certain subterms

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] option for simpl to never simplify certain subterms
Date: Fri, 14 Feb 2020 00:27:58 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f50.google.com
Ironport-phdr: 9a23:jCPD6hOhAmma0BVl/6Al6mtUPXoX/o7sNwtQ0KIMzox0Lfr5rarrMEGX3/hxlliBBdydt6sYzbSH+PC6EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba59IRmsrAjcssYajIh8Jq0s1hbHv3xEdvhZym9vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNwzY7bYoGbOvR9cK3AY90VWXFMUdxNWyFbGI6wc5cDAugHMO1Fr4f9vVwOrR6mCAeoHuzv0ThIhnnr1qM7yeQhFhrG3Bc9FN8JsnTbts71NKAUUeC61qnIyi7Db+hS1Drm54jIdwouofCIXb5qbcXRzkwvGhrDg16Np4LlODaV2f4Ms2id9+dgWuOvi3InqwFsuTej3Nsjio7Mho8T11vK9j15zZ4rKdGkTEN3e92pHZtKuy2EK4d7QdkuTmF0tCs817YIo4S0fDIQx5Qi3xPfa+KIc4yP4h/7UeaeOzZ4hHZ8dL2hmhm+7FGsyuP8W8WoylpKoS1Fkt7DtnAJyRPf8NSISvx4/ku52DaP0R7c6v1cLEwqiabWL4Qtz70wm5YJr0jPAiz7lF/2gaOKbkkk//Kn6+XjYrXovJ+cMIp0hxn8Mqs0gcy/BuI4MgcUX2ic4uS8z7nu8Fb2QLVPlPI2k63ZvIrGKsQco661GxVV3Zo76xajEzem18wVkmUALFJcYR6Ik4zpO0zVL/3jFve+g1GskC9xyPzcP73hBI/NLnnZn7v7c7Z98R0U9A1mxtdGoplQF7tJdPn0Qwr6sMHSJh4/KQ29hej9XoZTzIQbDECGGaifeIzItkSTrrYtKvKLYoAPvy3metAq4vfviTkynlpLLvrh5ocedH3tRqcuGE6ee3e52o5QQ1dPhRI3SanRsHPHVDdSY3ioWKdlv2M0DYunCcHIQYX/2eXdjhf+JYVfYyV9Mn7JCW3hLtzWVPIFaSbUKchkwGRdCOqRDrQ53BTrjzfUjrpqKu2Op38dvJPnkdV5vqjdyEl0+jtzAMCQlWqKSjMskw==

This is not currently possible. Related feature requests: https://github.com/coq/coq/issues/7159 , https://github.com/coq/coq/issues/4639 , https://github.com/coq/coq/issues/4474 ,

On Thu, Feb 13, 2020, 21:56 Qinshi Wang <qinshiw AT cs.princeton.edu> wrote:

Dear Coq community,

This may be a silly question, but I couldn't find the answer in documentation. I know there are some features to specify what should be simplified or not by simpl, but I think the following extension can be helpful. Consider a function definition f. Its type is, e.g. Z -> Z. I would like to write some command like

Arguments f x : simpl never x.

Then the argument of f should be left untouched by simpl, e.g. the result of simpl on [f (1+2)] should still be [f (1+2)] instead of [f 3]. This specification allows simpl to simplify expressions on some level while not touching lower levels.

Thanks,
Qinshi Wang

[Coq-Club] option for simpl to never simplify certain subterms, Qinshi Wang, 02/14/2020
- Re: [Coq-Club] option for simpl to never simplify certain subterms, Jason Gross, 02/14/2020