Is it possible to implement a tactic that can inspect the structure of an inductive type? I'd like to generically generate some match patterns, similar to what destruct/inversion etc are capable of.
You can do that in Ltac2 for sure (using the Ltac2.Ind module). Slightly more heavy solutions would leverage Elpi (examples in this paper) or Metacoq (as a reification plugin; see here). You can also abuse Ltac hacks (see for instance the coq deriving library) .
Last updated: Sep 25 2023 at 12:01 UTC