The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/26/2015 04:43 PM, Jonathan Leivent wrote:
> 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

Well, case_eq has its own issues, doesn't it?  I looked at what case_eq 
generated as the equality in the @eq_refl case - and it was "eq_refl = 
eq_refl".  Which may be a bug, I guess - as it should probably be 
"H=eq_refl" for case_eq H.

OK, so let's not depend on either the "eqn:" version of destruct or the 
"_eq" version of case - and use just vanilla destruct - which hopefully 
is used often enough that it doesn't have goofy behavior even in unusual 
cases:

Inductive Any2{T}(x:T) : Prop := any2.

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)$);
                       pose (any2 h) as E;
                       destruct h;
                       match type of E with Any2 ?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.

-- Jonathan