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 20:56:00 -0500

On 11/06/2014 11:24 AM, Jonathan wrote:
On 11/06/2014 10:48 AM, Jonathan wrote:
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

This, of course, can be improved a tiny bit by:

Tactic Notation "my_destruct" tactic(f) :=
match goal with _ : context[?C] |- _ => f C; destruct C eqn:? end.

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

Certainly still not nice to look at or type in. Maybe this is an argument for using a general macro preprocessor with Coq, such as m4? Although I don't know if that can be made to work interactively.

-- Jonathan


Actually - it is possible (in the trunk) if one is willing to use a bit of a kludge involving refine, an evar, and eval:

Tactic Notation "my_destruct" uconstr(p) :=
let e := fresh in
refine (let e := p in _);
[shelve
|let v := eval hnf in e in
match goal with _ : context[?C] |- _ => unify v C; clear e; destruct C eqn:? end].

Goal forall x, 1 + 2 = x -> False.
intros.
my_destruct (1 + _).

-- Jonathan




Archive powered by MHonArc 2.6.18.

Top of Page