The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/26/2015 04:34 PM, Jonathan Leivent wrote:
> On 03/26/2015 04:28 PM, Jason Gross wrote:
> > On Thu, Mar 26, 2015 at 4:18 PM, Jonathan Leivent 
> > <jonikelee AT gmail.com>
> > wrote:
> >
> > > On second thought, it isn't very hard to write an Ltac "is_ctor" 
> > > tactic.
> > > This way might not even be considered too kludgey:
> >
> > Nice tactic!
> > But it doesn't work on sufficiently dependent types; [is_ctor @eq_refl]
> > fails with an "illegal application" error.
>
> Oops - that's because destruct isn't a universal tactic for inductive 
> types.  Maybe I can use case_eq instead?  Unless that also has issues 
> with some inductive types...
>
> -- Jonathan

Actually meant to say "[destruct eqn:] isn't a universal tactic". Is 
that a bug?

Anyway, here's a version with case_eq:

Ltac is_ctor sym :=
  let h:=fresh in
  let E:=fresh in
  let A:=fresh in
  let t:=type of sym in
  let m:=constr:($(clear; intros A h; repeat specialize (h $(apply A)$);
                       case_eq h; intro E;
                       match type of E with _ = ?C =>
                         let c:=head_of C in exact (any c)
                       end)$ : (forall T, T) -> t -> Any) in
  match m with
    context[any sym] => idtac
  end.

It works for @eq_refl - but that doesn't mean there isn't something out 
there that will confuse it.

-- Jonathan