The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi,

As far as Ltac is concerned, its "match" is pretty constrained when it
is about matching a "fix" or "match" term (for instance the {struct id}
of a "fix" has to be the same in the pattern and in the matched term,
and, for "match" of terms, it has to be on the same inductive type).

There is otherwise a tactic "is_fix t" which tests if t is a fix and
fails it is not. There is also an ad hoc "destauto"/"destauto in H"
which destructs the "x" of all "match x with ... end" present in the
conclusion or in an hypothesis. Don't know what others would recommend
and what would more generally be the nicest approach to imagine to
deal with this kind of configuration.

Best,

Hugo

On Fri, May 15, 2020 at 06:17:13PM -0700, Eddy Westbrook wrote:
> 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