The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/26/2015 04:56 AM, Soegtrop, Michael wrote:
> Dear Coq users
>
> for guiding  automation heuristics I sometimes need to classify terms. For 
> this I am missing an ltac function has_var, similar to has_evar. Is there a 
> way to implement this in ltac?

I am assuming you want has_var to spot only free vars.  In which case it 
can be written in ltac as:

Ltac has_var term :=
  match term with
    context[?V] => is_var V
  end.

> 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.

> Another useful thing would be an ltac function, which evaluates some sort of 
> complexity measure of a term. I have some idea how this could be done, but 
> before I try it, I wanted to ask if someone has something ready I could use.

I would think this must be already done as part of some plugin or 
extension, although maybe not with the same complexity measure you are 
looking for.

-- Jonathan