The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/26/2015 11:40 AM, Jonathan Leivent wrote:
> On 03/26/2015 04:56 AM, Soegtrop, Michael wrote:
> ...
> > Also I wonder if there is a good way to check if a term is a literal, 
> > in the sense that it consists entirely of constructors, e.g. a 
> > literal number or boolean value or more complex term, but without 
> > vars, evars, matches or function applications. On a simplified term I 
> > guess checking not has_var and not has_evar would work.
>
> The difficulty would be in determining if the function head of a 
> (sub)term is a constructor vs. another kind of function.  It is 
> possible, but very complicated to write a tactic that identifies the 
> constructors of a type in Ltac  - but there is also a plugin to do 
> this, which is more recommended.

On second thought, it isn't very hard to write an Ltac "is_ctor" 
tactic.  This way might not even be considered too kludgey:

Inductive Any : Prop :=
| any{T}(x:T) : Any. (*a simple holder for anything*)

Ltac head_of term :=
  lazymatch term with
  | (?H _) => head_of H
  | _ => term
  end.

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)$);
                       destruct h eqn: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.

Variable F : nat.

Goal True.
is_ctor 0.
is_ctor cons.
is_ctor @nil.
is_ctor S.
Fail is_ctor 1.
Fail is_ctor F.
Abort.

-- Jonathan