Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Using patterns as arguments to Ltac tactics

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using patterns as arguments to Ltac tactics


Chronological Thread 
  • From: Pierre Courtieu <pierre.courtieu AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Using patterns as arguments to Ltac tactics
  • Date: Wed, 19 Jul 2023 18:00:55 +0200
  • Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-pj1-f51.google.com
  • Ironport-data: A9a23:I/MbeqxFnUI67ktGf996t+f4wirEfRIJ4+MujC+fZmUNrF6WrkVVy jRNX2yOaauMYmSgKNskbtzi8xkOsZPWyNc3HAZu+VhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefSAOCU5NfsYkhZXRVjRDoqlSVtkus4hp8AqdWiCmthg /uryyHkEAHjg2cc3l48sfrZ80sw5aWq4lv0g3RnDRx1lA+G/5UqJMlHTU2BByOQapVZGOe8W 9HCwNmRlo8O10pF5nuNy94XQ2VSKlLgFVDmZkl+B8BOtiN/Shkaic7XAhazhXB/0F1ll/gpo DlEWAfZpQ0BZsUgk8xFO/VU/r0X0QSrN9YrLFDm2fF/wXEqfFPwwahLJltuG7ZB99RJPmFx5 fMKFQ40O0Xra+KemNpXS8Fpj8UnadHpZcYR5ygmwjbeAvIrB5vERs0m5/cChGZ21p0IR6+AI ZdAAdZsREyojxlnIlYaEogz2uyvm2PjcjBFgF2QrKszpWPUyWSd1ZCzaYWKJYbUG625mG61m z3Iz3nkKSomNZ+azyCu2Gyymcv2yHaTtIU6TeXkrJaGmma7zWsKTRYSSFGTuui8kkf4WtRFK kVS9DBGkEQp3EmiT924Rx/h5XDZ51gTXN1fF+B84waIokbJ3+qHLnQGExtrcoQAj5Y7dwIV1 mCZkMHUOwU65dV5Vkmh3ruTqDqzPw0cImkDeTIIQGM5Dz/L8NBbYvXnHoYLLUKlsjHmMWqvn G3S/UDSk51W3JFbjfzqlbzSq2v0/sChc+Ij2unAsouYAu5RYYekY8mw6wGe46sZaomeSVaFs T4PnM32AAEy4XOlxXTlrAYlRunBCxO53Nv03wQH834JqW3FxpJbVdoMiAyS3W8wWir+RRfnY VXIpSRa74JJMX2hYMdfOtzhWptykPC7TYu6DJg4i+aihLAhJWdrGwk+NSatM5zFzSDAbIlla crFLZjyZZrkIf07nWrsLwvi7VPb7nlmmTm7qWHTwBOg3r6TDEN5up9UWGZimtsRtfveyC2Mq 4g3H5LTl313DralCgGJqtF7ELz/BSNnbXwAg5cKLrLrz8sPMD1JNsI9Npt7INc6xPkMzrmYl px/M2cBoGfCabT8AV3iQhhehHnHB/6TdFpqZnR+DkXiwHU5f4ek4YEWcpZ9L/Ft9/VuwbQwB 7MJctmJSKYHADnW2SUvXb+kpqxbdTOvmV2vOQiha2MBZJJOfVHC1eLlWQrNzxMwKBSLm/Ewm YD96TODc6E/H1xjKO30dMOQy0iAuClBueBqAGrNDNphWGTt14lILSbOoOc9CJwOI0+bxx+x9 QWfMTEHr8bj/q4399jog/ifjoGLSuFRIGtTL1P5352XaxbI3zOE6pBSdcq1ZhbhbXPQ1IT+Q PRK3tf+HeYinl0Xg7FjEr1u870y1+Hvq5Be0A5gOnfBNHavNZ9NPViE2ttppIRW57oEpzazZ F2DyuNaNZqNJsnhNlwbfyghT+ab0MAriivg1us0LGr69R1I0uK+C2sKBCa1iQtZMLdRG6Emy 714uMcptiqOuiBzOdOC1i1p52CAK0IbaJoet7YYPt7PqhEqwVR8c5DjGnfIwJWQWe5tbGguA BGp3ZTnuZoN53DsUXQJEVr14dF8nrUL4RBD808DLQ+Gm/3Dnf4G4ydS+jUWECVQwgl27OZoH m1NKUdOBL6v+g1wj5NpRFGcGABmBTyY9HfuylAPqnbrckmwWkHJL0w/Ieyo/n1F1055YR5g4 +i+5Ev+dDTlbuXd/3EXYlF0je7nQfha1BzwqOr+E+urR5AFMCfY2Imwbm82mj7bKMIWhmicg MJ1/ex1OJbJBQRJr4IVU4ClhKktEjaaL2l/QNZkzqMDPUfYXBqQgTGuCUSASvlhFszw032TK pJRf5pUdhGEyiyxgCgRBvcML59KjfcZ3oc+VY2xF1EWkYm0j2RPgMrL+znclV0bZYxksfwAJ 7P7cxOAFW2thkVopVLdkfkcOkSETIkFQCbewNGK9P44EsNfkeN0LmA3/LiGn1SUFwpF4yOru BjnV4XP6tc7zKJQspbeSPRdNV+kLff2cvqCyyGoktF0ddiUG9z/hwAUjVjGPgptIroaXepsp 4mNqNLa2EDkvq48dnLwwb2tNvBuy52pfex1NsnXEiFrrRGaUpWx3ypZqnGKF5NZtfh8uO+lf lKcQ+mtf4c3X9x9+iVkWxJGGUxAN5WtP7bSngLjnfGiERNH7BfmKumg/nrXbW12UC8EFpn9K w3sscaV+dFqg9VQNSAAGs1ZLcd0EH37VYsiUu/Bhz2SI22ro1GF47XczEtqrXmBD3SfC8/17 K7UXhW0Jlz4pKjMy8ofqIBo+AEeCHFmm+QrY0YB4JhMhiunCHIdZ/EoWXnc5kq4TgSpvH05W N3MUIfmISD0XDABaRelpdq+B0GQAesBPtq/LTssl69Rh+FaG6vYaIaNNA85i5u1Rtcn5O6iI NAavHb3O3BdB7l3EP0L6KXTbfhPn5vnK7Fhxaw5u8P3ChcaR74N0RSN2eaLuTPvS6nwqakAG YT5qa2ojq12pY4d3PuMo0JoJSw=
  • Ironport-hdrordr: A9a23:x9c9DKHkg2eQ3aHGpLqE0ceALOsnbusQ8zAXPiFKOGVom6mj/f xG885rsCMc5AxhOk3I3OrwW5VoIkm8yXcW2/h0AV7KZmCP01dAbrsD0WKI+UyGJ8SRzJ866U 6iScRD4R/LYGSSQfyU3OBwKbgd/OU=
  • Ironport-phdr: A9a23:ZTADnRJoKmdPEOSyyNmcuKZsWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFu7Mx3BSWAM3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmT owZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsip1u2+4ZLebgZHiDe/Yb55M Qm7oxjWusQKm4VpN7w/ygHOontGeuRWwX1nKFeOlBvi5cm+4YBu/T1It/0u68BPX6P6f78lT bNDFzQpL3o15MzwuhbdSwaE+2YRXX8XkhpMBAjF8Q36U5LsuSb0quZxxC+XNtDwQLspWzqt8 r1rRQfnhycJNTE38G/ZhM9tgqxFvB2svAZwz5LObYyPKPZyYqHQcNUHTmRBRMZRUClBD5umY YsOEeUBJ/xYoJfgrFYQqhu+GBOsBP/uyjBWm3/9wKo30/wgEQ7YxgwgBcwBvG7Io9XyKacSS /y1zKjWwjXedP5W1jL955LJchAlu/2DQbVwcc/IxEQpCgjKgUmep5b/MDOJyuQCrXKb7+x4W O+zlmIqrxx9rDexysowjoTHiY0bx1HY+ShkwIg4OMO0RU11bNCqE5Zcqz2WOohoT80tQ2xlu Tg2xLMatZOmcyUHzoksyRDYa/yCaYeI4xTjWf6QITd+nnJleaiwiwy88Ui6zOD3S8q60E5So yZbjtXBsmoB2h/T58SdVPdx40as1SyP2gzO7OxPPFo6mrDBK5E7x749jpoTvlrHHi/xgEj2i bWZdkQg+uSx8+TnYKjqqoaSN4J0lw3yKKsumsu4AeQ3NggBQXKX9vi71L3m5UH5QbNKgeMqk qTBrpzWOcAWqrS6DgJVyIov9QuzAja83NkYgHULNFdFdwiGj4jtNVHOOvf4DfKnjlS0kTdk2 erGPqf/DZnXMnfDl6rhfaxh605d1gUz0MtS551RCr4bIfLzXlX9u8DfDh88KwC0xf3oB81n1 owCQWKPHrOZMKTKvFOV/u4vOfWDZJcJuDbhLPgo/+LhjXggmVMEYaap2YYXZ2ujE/R9I0SZZ GLsjc0bHWcLuAo+Vu3qh0eYXT5dfXbhF547szo8EcetCZrJboGrmr2ImimhTbNMYWUTMlGBC 23lP66DRu0QaS+Papt5kzEeT7XnQIg8zw2vuRLSxL9uL+6S8Sod48GwnONp7vHewElhvQd/C N6QhjnlpwBcm2oJQ2Rzx6VjuQlmzU/F16FkgvteHNgV5vVTUw58O4SPh/diBYXUXQTMNsyMV E7gWs+vVCkwQ8grzpkFZFtnB9SvkzjM2iOrB/kekLnYTIcs/Pfk1mPqb914126A0aAgi1c8R c4aLWyrnLRysQPUGpTVkkiEv6mvfKUYmiXK8TTL1nKA6WdfVgM4SqDZRTYfa0/R+Mz+/V/HR qSyBK4PNwJAzYuaKPIPZICwy1pBQ/jnNZLVZGfZd36YIxGOy/vMaYPrfz5YxyDBEA0flBhV+ 3+aNA84DyPnomTEDTUoG0i9K0XrufJzrn+2VCpWh0mDclFh2ryp+xUUme3USvUd2agBsTsgr DM8FUi03tbfAd6N7wR7e6AUbdQ46VZBnWXX0m41doShIrp4ixgVdBlto0Ljyj14D4xBlY4hq 3ZrhAt+JKSE0U9QIiuC1MOVWPWfIW3z8RazLq/OjwuGgZDGp+FVsap+9gyw2WPhXlAv+Hhmz dRPhn6V55GRSREXTYq0SUEvsR5zu7DdZCA5oYLSz3xld6eu4Vqgk5okAvUozhG4cpJRKqSBQ UXqEsAAHcXoI+s3gUSoYw8sM+Vb9apyNMSjPajjuubjLKN7kTSqgH4Sqph831iW+mx3TfPSw 5cI3tmX2wKGU3H3i1Lr4aWV0chUIDoVGGS40y3tAoVcM7ZzcYg8AmCrO8Srx996ivYBQlZg/ UW4TxMD0c6tIl+JakDlmBZXzQIRqGCmni2xy3p1lSsop+yRxn6Gz+PnfRsBcmlFIQsqxU/tL JKugpYRW1WycwkkiTOq4E/7w+5Qo6E3I2TIQEhOdjT7NCk4Cvr25ufEOZcRrs5x+SxMNYb0K UiXULv8vwcX32v4Em1SySp6PzCmt5PlngBr3WeULXJ9tn3cKol7wRbS4sCZROYEhGJXAnklz 2OOWB7hZorMn53cjZrIv+GgWnj0U5RSdXKu1oacrG6g4nUsBxSjnve1k9mhEA4g0Ca92cM5M EeA5Bv6fITv0Ly3dOx9eUw9Tkf95tBgF8d1lZYqmJAdxFAVg5yU+TwMlmK5YrA5keruKWEAQ zIG2Yuf+AnowlduaHmO2pjlV3iA6sRkbti+JGgR32huiqICQLfR57tCkyxvp1O+pg+Eevlxk AAWzv424WIbieUE60I9iz+QCbcIEQxELDThwl6WusumovwdNwPNOfCgkVBzlte7APSerxFAD TznL4w6E3Y4790jYgmRliSisse+JIaWNZVJ6lWVi0uS0bQTcslq0KNU3Ww/fjus2B9tg+8j0 U4wg9fj5NLBcyM1u/jhSh9Aam+rOYVJpmCr3f4YxoHMh8iuBskzRW9NBceuFKPyVmpV7KSCV U7GESVg+CjHX+OFQEnHrh8h9iyHEoj3ZSjPdD9AkookFF/FYxYGyAEMAGdjwcV/T1H2gpSnK AAguFVzrhb5skcekLo5cUmiFD6F9EHwLW5rAJmHcEgMt18EuheTaJ3EqLo0RnAQ/4X9/lbUd CrBPFUOVjtPAgvdVjWBdvG47N3EuYB0H8KYKP3DKfWLoO1aDLKTwI63l5Bh53CKP9mOOX9rC 7s63FBCVDZ3AZaRnTJHUCERmy/XCqzT7B6h5i16qNy++/X3SUru44WIEb5bLdRo/Vi/n66CM +eagCsxJyxf09sAwnrByb5X21B36Wkmbz62DbEJrjLAVorVk65TSgYZMmZ9aZIO4KU70Q1Af 8Xcj5K917J1iOI0F0YQVVHlnZLMB4RCKGW8OVXbQUeTYe7edHubnoetOP36FOQD6Ycc/we9s juaDUL5azGKlj2yEguqLfkJlyaDehpXpIC6dB9pT2nlVtPvLBOhY7oVxXU7x6M5gnTSOCsSK z95JglVr7CK9y4eifJiAXBA42dNIuyNmiLf5O7dYMVz07MjEmFvmuRW7W5vgaNS9z1BTedpl TH6q9dvpxS+kLDKxGc+FhVJrTlPicSAukAoasC7vtFQHH3D+hwK92CZDR8H8sBkBtPYsKdV0 tHTlaj3JV+qHPrb+MIdA47fL8fVaRLJ1DLmHTfVCE0OSjv5bQk3ZmRYmfCWs2WX990098Gql 50JRbtWElcyE6FCYnk=
  • Ironport-sdr: 64b808c5_DinbS21Nve/+vJaoXAwZsCO7uq3s5nI8eg3cMSbQNBBIChj 8XwnBlgx5+dofqGc1LqAGlTlT4lfew85RV1SaOA==

Hi.
AFAIK the only way to take a pattern as argument is to use tactic notations and the « simple_intropattern » argument type.

https://coq.inria.fr/distrib/current/refman/user-extensions/syntax-extensions.html#tactic-notations

Best regards
Pierre

Le mer. 19 juil. 2023 à 17:30, Chris Dams <chris.dams.nl AT gmail.com> a écrit :
Dear All,

I would like to be able to use a pattern as an argument to an Ltac
tactic. Is this somehow possible? At the moment I am running into:

Ltac program_data_destruct st ll glob H
:= destruct st as [ll glob|] eqn:H;
     [fold mk_program_data in H |- * | fold mk_program_data_error in H |- *].

I would like to use a pattern instead of a complete term for st
because what I would like to pass as st can be quite large and I like
to fill in a few parameters to indicate which instance I want to
destruct but not all of them because that would be a bit too large.
E.g., I would like to do

program_data_destruct (set_pointer (mk_program_data _ _) _ _ _) ll' glob' H4.

but that runs into the error 'Cannot infer this placeholder of type
"program.stack program_global_type_info"'. Note that it would be quite
possible to pass the pattern term (set_pointer (mk_program_data _ _) _
_ _) as an argument to the destruct tactic, it is just the Ltac macro
that apparently forbids using this pattern term.

Is it possible to make this work somehow?

Kind Regards,
Chris



Archive powered by MHonArc 2.6.19+.

Top of Page