coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Ltac and constr arguments with holes, Robbert Krebbers, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Arnaud Spiwack, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/07/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/07/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/07/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/06/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Robbert Krebbers, 11/10/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/10/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jason Gross, 11/10/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Jonathan, 11/10/2014
- Re: [Coq-Club] Ltac and constr arguments with holes, Arnaud Spiwack, 11/06/2014
Archive powered by MHonArc 2.6.18.