The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

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

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?