The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

I've been experimenting with firstorder - but, other than hitting bugs 
(4401), all I've succeeded in doing is convince myself that I don't 
really know what it is supposed to do.  Can someone explain?

The two sentence description in doc is is confusing to me.  It says "The 
tactic firstorder is an experimental extension of tauto to first-order 
reasoning, written by Pierre Corbineau. It is not restricted to usual 
logical connectives but instead may reason about any
first-order class inductive definition."

In terms of what the "first-order reasoning" part means, my naive 
conception of what firstorder might do is:  do as the intuition tactic 
would do - and if any branch of intuition can't make progress, but 
contains appliable hypotheses such that not all parameterizations of 
those appliable hypotheses vs. other hypotheses exist as hypotheses, 
then do the missing generation and recurse. Sort of like:

  Ltac firstorder tac := intuition (tac || progress 
generate_new_parameterizations; firstorder tac).

where Set Firstorder Depth is used to limit that recursion.  Is 
firstorder indended to do just that, or something else?  Might it have 
some smarter way to generate useful parameterizations vs. all 
permutations, for instance?

As for the "may reason about any first-order class inductive definition" 
means - this has something to do with being able to construct and 
eliminate inductive definitions of things beyond just "and" and "or".  
For instance:

Goal bool. firstorder idtac. Qed.

works.  But, surprisingly:

Goal nat. firstorder.

does nothing.  Why?  Is firstorder limited to non-recursive inductive 
definitions only?  I can possibly see why that would be a useful 
limitation when doing elimination (but isn't that limitation redundant 
with Set Firstorder Depth?).  But why when doing construction, if there 
is a non-recursive constructor (as 0 for nat)?

-- Jonathan