coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Chris Dams <chris.dams.nl AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Using patterns as arguments to Ltac tactics
Date: Thu, 20 Jul 2023 06:22:51 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=chris.dams.nl AT gmail.com; spf=Pass smtp.mailfrom=chris.dams.nl AT gmail.com; spf=None smtp.helo=postmaster AT mail-vs1-f54.google.com
Ironport-data: A9a23:+80D2ak1bUyoyRh5tuLuenzo5gxKIkRdPkR7XQ2eYbSJt1+Wr1Gzt xIfWmuFOvmJMDf9ftwgPd+w80tS6JbTmoJlQQJtpCw1RltH+JHPbTi7BhepbnnKdqUvb2o+s p5AMoGYRCwQZiWBzvt4GuG59RGQ7YnRGvymTrSs1hlZHWdMUD0mhQ9oh9k3i4tphcnRKw6Ws LsemeWGULOe82Ayajt8B56r8ks156yt4WJA5DTSWNgS1LPgvylNZH4gDfrpR5fIatE8NvK3Q e/F0Ia48gvxl/v6Io7Nfh7TKyXmc5aKVeS8oiI+t5uK3nCukhcPPpMTb5LwX6v4ZwKhxLidw P0V3XC5pJxA0qfkwIzxWDEAe81y0DEvFBYq7hFTvOTKp3AqfUcAzN01HX8ML5wq/N9WGFlJp MQ+DToiZDeM0rfeLLKTEoGAh+wmJcjveZ0E4zRukG2fAvEhTpTOBa7N4Le03h9q3pEITauYP ZNGL2czBPjDS0Un1lM/A5IknfzuinD6aHterHqaoKM25y7YywkZPL3FaYOFIIfQGJ0P9qqej nLi/VXZOT8FDoSWkADf3GC+iLKRvhquDer+E5XhrqIw6LGJ/UQYDwRTXl+mq9Gim0umUpReL VYV82wgt8APGFeDS9D8W1imuyfBsENAHdVXFOI+5UeGza+8Dxul6nYsFS9/Us43hskPZCUS0 Q6xufbjKjZIv+jAIZ6CzYu8oTS3MCkTCGYNYy4YUAcIi+UPRqlj3nojqf4zQMaIYs3J9SLYm G/V8XBv71kHpYtaiPXhpAGvbyeE/8CRFmYIChPrsnVJBz6Viaagbo2srEbAtLNOcdrfQV6Gs 3wJ3cOZ6Yji7K1hdgTdHY3h/5nzv55p1QEwZ3YxR/HNEBzwqhaekXh4um0WGauQGp9slcXVS EHSoxhNw5RYIWGna6R6C6roVZR7kvm5SY+6DKuNBjarXnSXXF/XlM2JTR7At10BbGBx+U3CE c3LLJjwUyhy5VpPlWfuHrx1PUAXKtAWnDuPH/gXPjyo1r2RYHP9dFv2GArmUwzN14vd+F+92 48HaaOikkwDOMWgOHW/2dBIdjgicyNkba0aXuQMKoZv1CI9RTl9YxIQqJt9E7FYc1N9zbmRo yrsBR8ElDISRxTvcG23V5yqU5u3Nb4XkJ7xFXVE0Y+AiiN7M7W8prwSbYU2drQB/eluh6w8B focdsnKRrwFRj3b8n5PJdPwva5zRiSN3AiuBiuCZCRgXphCQweSxMToUDGy/wYzDw22l/AEn Zue6i3hT6A+GjtSVPTtVKr3znean2Qsp+Zpbk6ZfvhRYBrN9aZpGQzQj9g2AccGFjvbzBDH1 QzMWRY8jsvOqr8T79Pmq/2lrYCoMu0mBWtcPTDRwoiXPBng3FiI4NF/QsfRWhvCRkbYxb6EW dxF693dbNgWg0dssadnNrRgkJIF+NrkooFFwjReHHnka0qhDpViKCKk2fZjm7JsxLhLnxmfQ WOKp8dnPIuWNPPfEFI+IBQvasKB36o2nhjQ9fEEH1Xo1hRo/baoUVRgADfUsXZzdIBKCYICx fstnOU06Abl0xojDYugvxBurm+JKiQNbrUjupQkG7TUswsMyG8TRbzHCyTz3oODVMUUDGkuP Q2vpfTjg5Zy+xP8VkQdRFn34PplpJURuRp14kcICHaXl/Hk2PIm/h1j3g4mbwZSzx94/fp5E TExPF9YOZeMwm9MgcRdVTqgADN6WR+ToBTw73Arl2TpaVaieUKQDW86OMeLpFs49UAFdBdl3 bio8kTXehe0Q9PUwQ0zRl9Dl/zvafdT5z/yspmrMOrdFqZrfAe/pLGlYFQ5jifOAOQztRXhn vZr9uMhUp/LH3ccjINjArbLyIlKbg6PIVFDZvRT/KkpO2X4UxPq0BisL3GBQO98F8bow2SZV fM3ftluUi6g3hmgtjoYXK4AA4Fllc4TueYtROnZGn4kgZC+8BxZ6Ind5wrvtl8NGt9Oq/swG qnVVjCFE1GTu0dqpn/wnJFEF1e8MPY5Z1za/eGq8e82OYoJn8NyfGoTjLalnXWnHzF23hCTv TGZPq/f8PN/+N49g6rtDaRxKAGmIvzjVOmz0V6SsvYfSfjtIMvxpwcuhV2/BDtvPJwVQMVRq buWlczehWfpge4TaH/IvLWkDIxL1NWWcMsMFfyvN1hcvy+JePG00is542ridKB4yoJM1PeoV y6TSZWVZ9UKf/x/2XcMSSxVMyhFOpTNdq26+B+M9aWdOCM8jz7CAsisr0LyTGdhcSQNBZ3yJ yn0t9uq5fFatI58PwAFNd43H65HJELfZoV+e+3TrTW4CkyasmGGsJbmljsi7mjFNCDVWoKyq 5fIXQP3exmOqbnFhoMR+ZB7uhoMSm1xm68sd0Ya4MR7kC2+EHVAF+kGLJEaEdtBp0QeDn0ji O3lNwPOyBkRXAiotT356dXnGxmEX6kAZ4u/KTsu8EeZLSyxAetsxVenGjhIux9LlvnLlYlL6 u3yPlX/OxGwxtdiQuN7CjmTn7J83v2Drp4X0RmVriExairyxZ0F0XVgGExGUimv/wQhUqnUD TBdeF2oi31XhaI8/QiMtpKV9NwkUOvT8ggV
Ironport-hdrordr: A9a23:Qb3XdaBb2EGKtwXlHemV55DYdb4zR+YMi2TDtnoBMCC9F/bzqy nApoV/6faZskdyZJhko6HiBEDiexLhHPxOkO0s1N6ZNWGMhILrFuFfBODZslrd8kPFh4hgPG RbH5SWyuecMbG3t6nHCcCDfeod/A==
Ironport-phdr: A9a23:AXnpKRVStLYvT5yzboSbOI+1EWrV8KzIXzF92vMcY1JmTK2v8tzYM VDF4r011RmVB9udt6MP1LuempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQRFiCCybL52I xm7rwHcvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2Q rJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6 apgVR3mhzodNzMh/27XhM5/gqJVrhyiuhJx3ZLbbZqJNPZiZK7RYc8WSXZDU8tXSidPApm8b 4wKD+cZI+tYr5P9p1oVrRCjCwejHubvyiRVjXLxwaI60/4hEQDd3AA6At0BqnHUrM7vOKcUV eC416bIzTDZYPNX3Tfx8pTHchckofyVW797bMXex1U1GQzfklWQtZLqPymT1ukVsGWX8ettW f6yhmI5tg18ojqiy8Qjh4XVhI8YxVTJ+CV4zYorKtC2SFJ2bMO4HZdNsyyXN5V6T948Tmx2u Ss0xLsLsoO4cigS0Jkr2QLTZvidf4WL4h/vTvidLSp6iX5/eL+yiBC/+lW6xOLmTMm7ylNKo zJFktbSsnAN0ATe6s2dRft8+ketwCiP1xvO5u1dL0A5laXWJ4Quwr43kZoTvkDDETHslErqi 6+Wc10o+umu6+v5frXrvoGQO5Nwhw3kMakjmtazDfolPgUMRWSW+eux2KXm/ULjQbVKivM2k rPesJDfPckUuq65AxVU0oY48RqwEi2p0NEDnXUdKlJFfAmKj4fsO17UIfD4Ce2zjEirkDdu3 /zGOKbuDY3XLnffiLfhYap960lExQYu1dxf/Y5bCqkdIPLvXU/8rMDXDhggMwCt3+nnDMh92 ZgFVGKUAq6ZNbvSvkWS6uIuJemMfo4VtyznJ/gr/f69xUM+zFQaZOyi2YYdQHG+BPVvZUuDM lT2hdJUOmcQvxF2YOXvkxXWWj5JZm30U6s5/Xc9DKqpCI7CQsamh7nXj3TzJYFfem0TUgPEK nzvbYjRA5/kCQqXK85lyHkfUKS5DpUm3leovRP7zLxuKqzV/DcZvNTtzos9/PXdwDc18zE8F MGByyeVVWghlWMSRiRw0Kl6ugp7zn+M1KF5h7pTEtkAr+hRXFICPIXHh/d/F8i0XwvAetmTT 1PzSdW8ACp3Qts02JkIZ25yHtyjilbI2C/5S6QNmemtA5o5urnZw2C3J8t5zCPe07I9ilA9X sZVHWivh6o66ROKQoCUzwOWkKGlcala1ynInIua5UyJukwQEAt5UKGfGGsaelOTt9PyoEXLU 76pD70jdApH08+LbKVQOJXvih1dSfHvNc67ASr5knqsBRuO2rKHbZb7M2Qb0iLHDUEYkgcVt X+YPAk6Dy2lrirQFjtrXV7oZkrt96F5phbZBgc/zxuLdAtt3r+uvBgRrfOZQvIXmLkDvWZpq jl5Gkq8w8ODE8CJ9G8DNO1XZdIw5ksC1HqM7VQseMz9afo72RhDL1cS3QumzRh8B4RenNJ/q XoryFA3MqeEyBZbcDje25nsO7rRI220/Ra1aqeQ1EuNtbTesqoJ9vk8rE3u+Q+zEU93uX5ny dhOlXeV446MCg46Xpf4U0Jx/B9/7eK/AGF198bP2HtgPLPh+DTCwdMyQucszw3medN3P6aNF Qu0GMofTZvLSqRiix2iaRQKO/pX/ag/Mpa9dveI76WsOf5pgDOsiWkvDJlV6kuX7GI8T+fJ2 8xA2PSExk6dUDy6il69s8fxkIQCZDcIH2P5xzK2TIJWY6Rze84MBwLMa4W8xs9/nNjhUntDs linL1wD0c6tPxGVahTx0BZR2kIevXG80XHgnnokzndz9/XZgXCGyv+qbBcdP29XWGRu6DWka ZO5idwXRgngbgQkkgek+VevwqFaoKplKGyACUxMfiXwMyRjSv7q7uvEM5MJssp393gLA4HeK RiAR7XwogUXyXbmFmpannUgci2y/4/+lFp8gX6cK3B6qDzYf9txzFHR/o+5J7YZ0zwYSS1/k TSSCEK7Oozj9tWOloyFvum7TCSnUrVcdCDqycWLsy7xtggISVWv2uu+nNHqC11w2i/h1sIsW SzNt1D6ZqHk0q27NaRseUwiVzqeo4JqX4p5lIU3npQZ33MX046U8XQwmmD2KdxH2Kj6YSlFV XsRztXS+gSgxFx7IyfD2dfiTnvEiJgEBZHyciYM1yk69cwPFKqE8OkOg35uulTh5QPJPaomw 3FEmKNosiJFxblO4lZlzz3BUO5OWxMDZmq1yUzOt5fn/cA1LC6uaeTiihQ4xIj7SunE+kYGA D74YstwQ3E2tJkudgKUliW0sNmsecGMP41J8ETI1U6R1a4Nb8th85hCzSt/ZTCi4Tt8kbN91 Vo2msjk9Imfdzc0pPL/W0EHcG2zP4RJo3nslfoMx5nNmdn+QtM5XG1MBcWNL7rgESpO566/Z kDeTXtl8CfdQf2GQkee8Bs09SuRVc37cSjGfj9BiowzDBiFeB4F2V5SBm5r2MVjUFjtnZ2EE g8x8DkV4hSQRgJk7OVuOlG/V27eoF3tcTIoUN2FKxEQ6Ahe5kDTOMjY7+RpHige8Ifz5AqKY neWYQhFFwRrEgSNGkzjM7+y5NLB7/nQB+ywKOHLaKmPruoWXumBxJam2I9rtziWMcDHMn5nB vw9kk1NOBIxU9zegCkKQjcLmjjlaseaoFKi4XQyoJ3jtvvsXw3r6M2EDL4TedRj9haqgLuSY u6dgCEqTFQQnpgIxHLO1P0exAtI03AoJ2TrS+1f83ORH8ey0udNAhUWaj1+Lp5N5qM4hExWP NLDz8ny3fh+h+I0DFFMURrgnNuobIoEOTLYVhuPCUCVObCBPTCOzdvwZPb2Qr1Kjf4SuxS1o nCdF2fsOz2Ck3/iUBXlYoQuxGmLeQdTvo2waEMnEW/4UNfvcQG2KvdyhDwyhKMv3zbEaDJaP j97fEdA6LaX6GkL55c3U3wE5X1jI+6eni+f5OSNMZcav8xgBSFsnv5b6nA3o1O6xC5BTf1x3 iDVq4w3y7lHuuyGyz4iTgEX7zgW2MSEukJtPaif/Z5FCy6sFPcl4mCZChBMrNxgWIWHhg==
Ironport-sdr: 64b8b6a8_jvn+P2CbEKI9aeS3V4Ffa5RCzo4EQiPNMYKX3Akp6Q9FHrE 7exJnGcekO19qZ8jujbUWq16zYMioDUf6pq3a0A==

Hello Peirre,

Thanks for the info. The simple_intropattern does seem to apply to a
different situation, though.
I suppose for now I just allow a bit of code duplication and have
multiple tactics, like, for instance,

Ltac assign_expr_destruct ll glob H
:= destruct (assign_expr (mk_program_data _ _) _ _ _) as [ll glob|] eqn:H;
[fold mk_program_data in H |- *|fold mk_program_data_error in H |- *].

Ltac set_pointer_destruct ll glob H
:= destruct (set_pointer (mk_program_data _ _) _ _ _) as [ll glob|] eqn:H;
[fold mk_program_data in H |- *|fold mk_program_data_error in H |- *].

I don't think the list of that kind of tactics is going to grow all
that large anyway.

Besides, I realized that another option is to first do, e.g.,
set (st := set_pointer (mk_program_data _ _) _ _ _). Then I can use st as a
parameter to the tactic.

Kind Regards,
Chris

[Coq-Club] Using patterns as arguments to Ltac tactics, Chris Dams, 07/19/2023
- Re: [Coq-Club] Using patterns as arguments to Ltac tactics, Pierre Courtieu, 07/19/2023
  - Re: [Coq-Club] Using patterns as arguments to Ltac tactics, Chris Dams, 07/20/2023
- Re: [Coq-Club] Using patterns as arguments to Ltac tactics, Gaëtan Gilbert, 07/20/2023
  - Re: [Coq-Club] Using patterns as arguments to Ltac tactics, Chris Dams, 07/21/2023