The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 11/06/2014 09:16 AM, Arnaud Spiwack wrote:
> I believe the behaviour of [destruct] with respect to goals is really tied
> to its grammar rule. On the other hand, trunk's Ltac has a [uconstr:(…)] to
> do this sort of things. There has been some talk about using [uconstr] as
> input for tactics which accept open terms instead of ad hoc mechanism,
> which would provide your feature. But today, I don't think there is a way
> to do what you want.
>
>
> Arnaud

I think Arnaud is right about that, but maybe the following is close enough:

  Ltac my_destruct f :=
  match goal with W : context[?C] |- _ => f C; destruct C end.

  Goal forall x, 1 + 2 = x -> False.
  intros.
  my_destruct ltac:(fun X => match X with 1 + _ => idtac end).

In other words, simulate what destruct's special pattern syntax can do 
with an ltac function wrapped around the target pattern.  This at least 
allows one to pass around the equivalent of a pattern with holes as an 
ltac function.

-- Jonathan

> On 6 November 2014 13:38, Robbert Krebbers 
> <mailinglists AT robbertkrebbers.nl>
> wrote:
>
> > Tactics like destruct accepts terms with holes for their arguments. For
> > example:
> >
> >    Goal forall x, 1 + 2 = x -> False.
> >    intros.
> >    destruct (1 + _) eqn:?.
> >    Abort.
> >
> > Here, I am allowed to put an "_" instead of the 2, and Coq will infer it.
> > Especially if one has to deal with very large terms, this is extremely
> > useful.
> >
> > Now I want to use destruct as part of an Ltac tactic, and be able to use
> > underscores in arguments to the Ltac tactic as well. However, that does not
> > seem to work:
> >
> >    Ltac my_destruct z := destruct z eqn:?.
> >
> >    Goal forall x, 1 + 2 = x -> False.
> >    intros.
> >    Fail my_destruct (1 + _).
> >    (* Cannot infer this placeholder. *)
> >    Abort.
> >
> > I tried to play around with tactic notation, but without luck:
> >
> >    Tactic Notation "my_destruct_alt" open_constr(z) := destruct z eqn:?.
> >
> >    Goal forall x, 1 + 2 = x -> False.
> >    intros.
> >    my_destruct_alt (1 + _).
> >    (* Now I have a meta in Heqn *)
> >    Abort.
> >
> > Any suggestions?