coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Eddy Westbrook <westbrook AT galois.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Finding a pattern-matching fix in a term?
Date: Fri, 15 May 2020 18:17:13 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=westbrook AT galois.com; spf=PermError smtp.mailfrom=westbrook AT galois.com; spf=None smtp.helo=postmaster AT mail-pg1-f174.google.com
Ironport-phdr: 9a23:1h/dEBFWUOrvJ3HoqpNRL51GYnF86YWxBRYc798ds5kLTJ7zpcSwAkXT6L1XgUPTWs2DsrQY0reQ4vGrAjxIyK3CmUhKSIZLWR4BhJdetC0bK+nBN3fGKuX3ZTcxBsVIWQwt1Xi6NU9IBJS2PAWK8TW94jEIBxrwKxd+KPjrFY7OlcS30P2594HObwlSizexfLN/IA+yoAjVucUbj4hvIbstxxXUpXdFZ/5Yzn5yK1KJmBb86Maw/Jp9/ClVpvks6c1OX7jkcqohVbBXAygoPG4z5M3wqBnMVhCP6WcGUmUXiRVHHQ7I5wznU5jrsyv6su192DSGPcDzULs5Vyiu47ttRRT1jioMKjw3/3zNisFojKxUvB2vqBNizYDXbo+bKv1wc7jBfdMDQGpNQsZRWzBDD466coABD/ABPeFdr4TlqFUBsAaxBAmxD+zv1DBInWP20rYg0+QmFgHG3xErEtUAsXvKt9X1KLwdUfqyzKnPzjXOdPxW1i356IjPcxAhuuuAUq53ccrU0EQiER7OgVqMp4L/JTyVyvgNvHaB7+pmTe+hhWoqpg5+rzWx28ohiIfHi4Abx13a9Sh03ok7KNm2RkB1fdOoDZteuiWHO4Z2Qs0vR2VltSg+x7AYuZC3YicHxZI6zBDcc/yKa5aE7g7nWeqLIjp1hGhpdKyiixuy60Ss1+/xW8as3FtIoCdJiMfAu3AX2xDO6sWKTuFx80Ov1DuJygvd8PtLIVoumqreM5MhwqA/lp4UsUnbGy/5gkT2jKuPekU89eik9v3rYrv7qpKeOIJ4kA7+MqMpmsywBeQ3LBICUHSc+eS5zLHj/Ev5T6tWjvAujKXVrJTXKd4Yq6O5GQNZzJsv5halAzu70tkVkmELLFdfdxKGi4jpNUvOIPf9DfqnjVWjjixrx+zdMb37BZXNKXvDnazufbln705czwszzctF651IDbEBJer/WlXtu9zAEh85Lwu0zv77B9V6z4MSQH6AAquEMKzJqlKI/eIuI+yUZIAPojr9Kv4l5+TvjXAjg1Mdc7OpjtMrbyWzGe0jKEGEa1LthM0AGCEEpFkQVuvv3XCOXS8bWHupQ6gm4TY4QNa5AJzfTJqqh7+p0y6/GZxNIGtBDwbfQj/Ta4yYVqJUO2qpKch7n2lcDOXze8oazRir8TTC5f9nI+7ToHNKsJvi0J1t6LSWm0htqXp7CMOS12zLRGZxzDtRG20GmZtnqEk48W+tlLBiiqUCR9Na4/RISUExMpuOl7UrWeC3YRrIe5KycHjjR9ynBT8rSddomY0BakJ6Gs7khRfGjXSn

Hey Coq Club,

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…?

Thanks in advance,
-Eddy

[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