The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/31/2015 04:04 AM, Soegtrop, Michael wrote:
> Dear Jonathan,
>
> thanks a lot for your elaborate answer! I am still digesting it. I am 
> experimenting if it works better for my automation control to detect terms 
> which contain only constructors using the method you described or to detect 
> terms which contain something which is not a constructor. The first is more 
> directly what I want. The other might be more efficient, but as I said I am 
> still experimenting.
>
> Thanks & best regards,
>
> Michael

I am not sure how one would determine that a term contains something 
which is not a constructor without examining each function symbol to see 
whether or not it is a constructor symbol.  Do you have an idea how to 
do this, or are you searching for such an idea?

By the way, I was able to create a ctors tactic based on that is_ctor 
tactic which returns all of the constructor symbols for an inductive 
type without requiring much more complexity or kludges - even a version 
that works in versions of Coq prior to 8.5 - meaning without 
tactic-in-term.  I had previously thought it would be much more complex 
and/or kludgey to do this without a plugin, and not even possible prior 
to 8.5.  If anyone wants this, I can post it.

Another point that occurred to me about your goal of an Ltac tactic that 
produces a complexity measure for a term - I think one area where this 
could get very complicated is when analyzing terms that contain match 
expressions.  Unless it is OK for your purposes to not bother to analyze 
the branches within a match expression.  I am not saying it is 
impossible, it just seems like it would be quite difficult.

-- Jonathan