The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

If you don’t mind including a plugin, I’m certain that this can be done in Mtac2, although it isn’t trivial. I’ve started playing with it but I stumble upon the issue that a fixpoint only reduces when the argument is a constructor. If you want to have the solution, I can help you work it out.

To give you an idea of a piece of code relevant to the problem, the following helper function applies a given function f with a list containing enough parameters to make the function fully applied:

Definition get_parameters {C} (f: mlist dyn -> M C) : dyn -> M C :=
  (mfix2 app (l: mlist dyn) (d: dyn) : M C :=
    mmatch d return M C with
    | [? A P fu] @Dyn (forall x:A, P x) fu =>
      \nu x:A, app (Dyn x :m: l) (Dyn (fu x))
    | _ => f l
    end) [m:].

Best,
Beta

On Sun, May 17, 2020 at 5:05 AM Hugo Herbelin <Hugo.Herbelin AT inria.fr> wrote:

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