Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Ltac and constr arguments with holes

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ltac and constr arguments with holes


Chronological Thread 
  • From: Jonathan <jonikelee AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Ltac and constr arguments with holes
  • Date: Thu, 06 Nov 2014 10:48:54 -0500

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?






Archive powered by MHonArc 2.6.18.

Top of Page