The Coq mailing list

[Gregory Malecha <gregory AT bedrocksystems.com>]

It is late, but you can do this in template-coq simply by quoting the term and writing a function to check what you want. It wouldn't be truly gorgeous, but it doesn't require anything that is unsafe. Note that what template-coq gives you is a Gallina inductive type that reifies a Gallina term, so inspecting a term is *literally* just Coq pattern matching. That said, this is definitely not unification, so if you want "definitionally equal to" rather than "syntactically equal to you are currently out of luck with template-coq.

On Mon, May 18, 2020 at 5:40 AM Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr> wrote:

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

--

Gregory Malecha

Mail: gregory AT bedrocksystems.com

BedRock

Systems Inc
UNBREAKABLE FOUNDATION FOR

FORMALLY SECURED COMPUTING