The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

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