The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

Hi Jonathan,

Indeed, while tauto/intuition are limited to recognizing inductive
types syntactically isomorphic to and/prod, or/sum, False/Empty_set,
True/unit (as well as recognizing not and iff and a few other ad hoc
things such a t=t), firstorder is able to recognize general
propositional-level connectives (in Prop, Set or Type) such as bool or

Inductive and_or (A B C:Prop) :=
| leftpair : A -> B -> and_or A B C
| right : C -> and_or A B C.

as well as general predicate-logic connectives such as 

Inductive exists2_2 (A B:Type) (P Q:A->B->Prop) :=
  ex_intro2_2 x y : P x y -> Q x y -> exists2_2 A B P Q.

Recognizing nat as a "connective" would have been certainly possible,
but then you would have to recognize other recursive "connectives"
such as, let's say, n-ary conjunction as defined e.g. by

Notation "p .+1" := (S p) (at level 1, left associativity, format "p .+1"). 
Reserved Notation "∧_{ i < n } P" (at level 80, i ident, P at next level).
Inductive andn (P:nat->Prop) : nat -> Prop :=
| niln : andn P 0
| consn n : P n -> andn P n -> andn P n.+1
where "∧_{ i < n } P" := (andn (fun i => P) n).

and this would require some extra work.

Note that there exist variants of intuition which recognize general
connectives. The tactic gintuition is recognizing general
(non-recursive, 0-order) mixed-conjunctive/disjunctive connectives in
the style of firstorder. The tactic dintuition is recognizing
(non-recursive, 0-order) purely-conjunctive connectives as well as
similar general purely-disjunctive connectives.

From a user perspective, this overlapping of similar tactics each of
them with their own specificities is certainly frustrating. Maybe
could we see it as a sign that we are only at an early stage of the
history of the design of interactive proof methods, automation
procedures and tactic programming languages? Sufficient manpower and
funding to remedy this and to at least understand how to combine the
best of the ideas put in each of the different approaches into
optimally-designed interactive proof methods, automation procedures
and tactic programming languages has apparently not been found yet. I
sense that it may however progressively change... In the meantime, if
anyone on this list feels like he's willing to contribute fair
comparative analyses of the pros and cons of various ideas around,
that can certainly help.

Back to firstorder, the associated publication is at
"http://www-verimag.imag.fr/~corbinea/ftp/publis/ljti-rr.ps";.

Hugo

On Sat, Nov 07, 2015 at 01:57:08PM -0500, Jonathan Leivent wrote:
> 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