The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/22/2016 04:27 AM, Robbert Krebbers wrote:
> On 09/22/2016 10:15 AM, Frédéric Besson wrote:
> > >  Otherwise:
> > >
> > >  Class is_var_bool {T} (x : T) := decide_is_var : bool.
> > >  Hint Extern 0 (is_var_bool ?x) => first [ is_var x; exact true | 
> > > exact false ] : typeclass_instances.
> > >  Ltac is_var_bool x := constr:(_ : is_var_bool x).
> > This is what I would call Ltac kung-fu.
> > A dark art which I sincerely admire but do not intend to practice.
> Jason's trick can be simplified as follows:
>
>   Ltac is_var_bool x :=
>     constr:(ltac:(first [is_var x; exact true|exact false])).
>
> I sometimes use this constr:(ltac:t) trick to define tactics that 
> return a term while being implemented using possibly side-effecting 
> tactics.
>
> IMHO my solution isn't very pretty either...

Yet another solution is:

  Ltac is_var_bool x :=
    match goal with
    | _ => let dummy := match goal with _ => is_var x end in true
    | _ => false
    end.

This is a throwback to the pre-tactic-in-term days of 8.4+.

IMHO none of these are pretty.  But, one can mask them with a Tactic 
Notation.  One additional behavioral feature of this ugly match form is 
that - if one instead uses multimatch for the outer match, the form have 
multiple backtracked successes, unlike the constr:(ltac:(...)) form.

-- Jonathan