coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Finding a pattern-matching fix in a term?

From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
To: coq-club AT inria.fr, Eddy Westbrook <westbrook AT galois.com>
Subject: Re: [Coq-Club] Finding a pattern-matching fix in a term?
Date: Mon, 18 May 2020 11:40:01 +0200
Autocrypt: addr=pierre-marie.pedrot AT inria.fr; prefer-encrypt=mutual; keydata= mQINBFOFpSQBEACyDotTWHydRK+7nzdk+ULrBszrG8Eu7J59+eogMOIOQYKw/joFiTOHnJgG vUzt//PqMURC7tZ72teZHeyLKHwr3a9oOC4W36Wrt4jVGvAnYk60hF20i921ljIN8aj41UYz t+8vgsqgpTCNbcgxhhgXSQ+9n/OZs1yoy6kgIE378HsIhGoGTQxmwdz2k0Aic/qun2Z4CO9v zjTjkUYMJxs4XwVsprMkO/a6qVBkNtEjbwVDJS5d7qzfph2DHJXFyUOPc1GudPI+VW2Abi4A 2US/ycyGMUTYRVaUDUF/GqfqmYgUj4vFvANdB3Roa3XDVxAlkYcNuUqtcpQi9yoU6t+Agobp nqcn+WrtOwrJtvEh3KaaQvI4Yudz3pEmP9KL2VYenUQLuDqVL4KgdCPcAZmpkSC7KCm8Ns2v y69zHasNsPD9YiIXCgpGNZEEUjrG8Si+ej3/3MTqTBQqpSzqTagtGhGANrjEgHj6zdh+plby k/bCYHjX4oDPJZQx6GjmtGPandUAD+SImEwS6WMyCKtUSKJtqD+DVNWiwKAK3+CNxDW/DbRS /N2ACdtItJhFmPAb9Nxs6O27xyPCse4n9fMCT5pLQpDfMmkOQsjr1kCWiOWgjIgfOG64HrxQ Vcjg6mf9EEGVi4kpMhl6RzZ7wsg+ff3w/5NR1e1HX9yj/UbsLwARAQABtDNQaWVycmUtTWFy aWUgUMOpZHJvdCA8cGllcnJlLW1hcmllLnBlZHJvdEBpbnJpYS5mcj6JAj4EEwECACgFAlOF pSQCGwMFCRLMAwAGCwkIBwMCBhUIAgkKCwQWAgMBAh4BAheAAAoJEHkiwB/Zujx745sP/3JA gDdlat/mjqxgpC30Jy5Rnkgblxo/qnEmmhPxSQJKt77JaaDgRfsTrJZcO1K9LN6aLs8dPo26 V29TSt0UJhw5bQcTqi/wlD/ZfQ3I69gn9x6ln3T/7TV/g0tyObbzPYQLsi6p8wgJzO1F3Dr2 9XjEfB2jVs7ancTKbE+5yvwN0v3VCrtG5cFpAdkrMtZzXbXMAxRa7HueUjtxm/ls5zqbwTZ6 1tmJlSJJS+rL43InCxDFRbPO4YzV3z7+sEw/Kpn3HwVQz6y3aDQWqQlq/vF8r0p+3E3CB+h/ h6coMySbpwHZAAMsu9KpQBqGpbAjI5RXvcNJD+7MCqT5LYy/QmULqVaLS7zaspcZc2V2CW1w 4LaZtlMjt4gedGvd/UICuy1pw1GdR3YRlUCQGKnzVp8Cw1Bsd1SbZu0DT/DOt3DHyZLliENu P6PRPQT+Rmj21mDpj+bLJliIpRWQ99/cFA6mmKv7qYk49xWsUL0YxcGabGIObBbMpFoq+Coj 8Gmm10706NrJuhYJMxdxHQNbiV8eYnC6jKnL0F3BPeEloSpw0saq/8PVU7eTwvkrOBTVfiwa UFe7HLFDo6SaRoXJAeBa22ADM4bTQCrf856BMT/4BjHdSUAj4Sq1j1QUHVTWWRVsnNH8Nz10 /n2x8sxQIf8yVX4aN/Km/uz7Xq14hL6suQINBFOFpSQBEADMsZKO9fPtbmyMlS5YQl3B+p5E 17sEJAHSNGA4rfx7Uxij1H1PnTZ0kHhngrhEG1wzv2+1aORCg31Jqrwf//XPbcv6QL4CinD7 QUpbMdrZFo296AkAjuhO8J0LvB8CY3GY6n/G3njy9ISmemEH3dAzOM87Wt0En1dcSYJxdfM2 fmWq6ghlmcQA6A6g1vJ0iKnFcvh/IXHBm1/dtVSOj+2+S4/PLALMCUzugFQLVAKiv7pkdxPz KGxMMEnQuLXjoFivXV6i3q9+0FVVo2t9LfD1EzTNoKwx4866nVnVMU9myd6IS03lKAREmHhb YRKJt+dlmJoqttVczsruFa1SRmzhpp5O2jFWzR0C+SD23s70PXaZ4wcn4TzQKL+tGMRqELLF XepqWcmKnROvX+agmeZK1UxhaIGI0JpPtZHsNGNoU1dbzUE+opzHP5Lpouc5Te+MkXe4wSM6 WrfyTRqUfVr7CeaSozkX/AfgubNnNYmi8RduUjUBjukMEsRchirbyCh1397xK90HDpiiqPy/ PLaUx/sp2vp0TSxGPFtl9CmuSOPVi0HQI51SrnckMA/zQJu6AZyFkbb7fpUi/cPds7AVCLjd mNkLOe77sZ+/D3YKXiHujrpncau+NaQ2SKMrqcRocAeogbd+VV3DFGRgHereAZwHD87ruHeg jEO92QRw/QARAQABiQIlBBgBAgAPBQJThaUkAhsMBQkSzAMAAAoJEHkiwB/Zujx7eSsQAJnw yYs/yiYjwzYdlmGQP1fuG0RG6DwHXZDti9etXRhjgOMvE4+TKqSeM9gXCxdGE7M2aKV+PJvi twb4FRLBOl9YwlHTiV5UIJpcbJv+zvdNSDrlqSSln1Qfqq7HJUvDwSKcY8316pVuF5Q9gknX P/gRG4O8e/fBXuSiL08cDudnkbhSm6zb+VGaewivO0FuuCX4RpYtF4EULbCKof7SSCK3/WWl roX6H3S6dNo/3cUGahj7FfTaQMwHH34P6wGWtJCh7vhaxQ5QdXjj8ZkJfcE03uo+GbF7/xmo g5wxtsFUWhs5G0P534BmahBBKsINIyExt6JYASYL/oouC9c+AOjc3bON7Ae1jeHgx3BSSUju 81x+5MrXAqrLhJ6xDsQpATL7qDcBEHBodo0xlAIgb71qeIU5gZUOw/43eJOnexDFs4VWMthJ z2ot6WdRzYEKt75nuCZqaaUEM+MvOGNZZRM3Dkbqw3Jik1X+lOjc/OgUs+Xn9oaIylA1nojO 9E31ulGmniydilLd+4Vd+WQn0ZEwy75EzDTl0Ne/j8nvLyzeYIWbt5/06mR2L87DIEXmXkAM mwfFXNzzX9gVX8m7owb4CPTf5DCDrguwNdvcPePy81w+fXM7c0Dq+5hzPvh5MRruEDOfqaZw HXQ4ZkGmhsCD6dMF2cKX+EqLjopA136U

Hi,

On 16/05/2020 03:17, Eddy Westbrook wrote:
> Is there any way to pattern-match on a fix + match term like (fix foo
> (x1:A1) … := match xi with … ) in a term? I am trying to write some
> tactics to determine if a particular argument is being destructed in
> a term, in order to apply the destruct or induction tactic on it, but
> it seems that Ltac at least won’t let me search for fix terms…?

if you're using Coq >= 8.11, it is possible to do this in Ltac2, albeit
in a way deemed "unsafe". Once done, you can also wrap the resulting
Ltac2 tactic into a proper Ltac1 tactic, so that it is transparent for
the end-user. Look at the Ltac2.Constr.Unsafe module for more details.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature

[Coq-Club] Finding a pattern-matching fix in a term?, Eddy Westbrook, 05/16/2020
- Re: [Coq-Club] Finding a pattern-matching fix in a term?, Hugo Herbelin, 05/17/2020
  - Re: [Coq-Club] Finding a pattern-matching fix in a term?, Beta Ziliani, 05/17/2020
- Re: [Coq-Club] Finding a pattern-matching fix in a term?, Pierre-Marie Pédrot, 05/18/2020