coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Qinshi Wang <qinshiw AT cs.princeton.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] option for simpl to never simplify certain subterms
Date: Thu, 13 Feb 2020 21:55:42 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=qinshiw AT cs.princeton.edu; spf=Pass smtp.mailfrom=qinshiw AT cs.princeton.edu; spf=Pass smtp.helo=postmaster AT yellowcard.cs.princeton.edu
Ironport-phdr: 9a23:tbvTeRPa3w49Vta4Cmgl6mtUPXoX/o7sNwtQ0KIMzox0Lfr/rarrMEGX3/hxlliBBdydt6sYzbSH+P24EUU7or+/81k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba59IRmsrAjcssYajIt+Jq0s1hbHv3xEdvhZym9vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhNww4DaboKbOudgcKzBZt4VX3ZNU9xLWiBdHo+xbY0CBPcBM+ZCqIn9okMDowC/BQmqH+Pvyj5IjWL20qIg1eQhHhzN0Qs5H9IPtnTUt9X1NKYcUO2u0KbI1i/Pb+tM2Tf87ojHbg4uoe2LXbJ2a8be11QgFx7cg1iWtIfrPCuV2/wQv2SF7OdsT/+jh3M5pw1rvzSiyMYhhpPIi48U0lzI6zl1zYIvKdC7SEN3e8CoHIZUui2AOIZ7RsUvSHxytikg0L0Jo5u7cTAKyJs5wx7fbOSKcoiW7RLnUOaRJjl5i25/d7Klmhm+61SvyvbmWsmsylZKryxFncXSuXAR0BzT7NKLReVg8Ue8wTqP1gbT5f9YIU0siKbXNZ0szqQtmpYOr0jPBDL6lUv3gaOMd0gp+/Ck6+H9bbXnop+cOZV0igb7Mqk2g8y/AOI4MhMOX2ia9+Wxz6Hs/VbjTLVSlP02k6/Zv4zEKsQHoa65BRVZ3Zg+5BaiFzumysgXnWEbLFJZfxKKl5TmO1bXIPzhEfi/h0msnyxwyvDdPrzhB43NIWLZnLfge7Z98U9cxxApwdBR/ZIHQo0Gdfn0Qwr6sMHSJh4/KQ29hej9W/tn0YZLYGOJGa+YeJzbt1DAsvsuJfKMZZA9sy27M+Ik4fXjkXg/31IRYP/6jtMsdHmkE6E+cA2ian32j4JZSDtYjk8FVOXvzWa6f3tLfX/rD/A3/XcjEoOgBorfQYbrjbCcjn/iT89mI1teA1XJKk/GMoCNWvMCciWXe58zmSdCTaKgTYQsyRao8gL21ug+d7eGymgjrZvmkeNNyajTmBU1r20mHsmZ12aSRGhukiUDXHkuxqF5qkFhzVHF3KRl0aVV

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