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: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Ltac and constr arguments with holes
  • Date: Mon, 10 Nov 2014 00:54:18 +0100

Arnoud, Jonathon: thanks for the replies.

Inspired by Jason's message on splitting evars, I ended up with

Tactic Notation "my_destruct" open_constr(z) :=
match goal with
| _ : context [?z'] |- _ => unify z z'; destruct z
end.

Goal forall x, 1 + 2 = x -> True.
intros.
my_destruct (_ + _).
Restart.
intros.
my_destruct (1 + _).
auto.
auto.
Qed.

This seems to work, even on Coq 8.4.

On 11/06/2014 01:38 PM, Robbert Krebbers 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