The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 11/08/2015 11:23 AM, Hugo Herbelin wrote:
> 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.

That seems like all non-(mutually-)recursive inductive types - is that 
correct?

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

OK.

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

That's good to know.

Is it the case that even though these variants of intuition are not 
documented, they will be maintained as much as the vanilla intuition tactic?

>  From a user perspective, this overlapping of similar tactics each of
> them with their own specificities is certainly frustrating.

The lack of predictability is frustrating (along with the bugs, of 
course) to me.  It seems like firstorder would (if it were fixed) 
perform some automated forward chaining - much like that Hint FChain 
idea I proposed last week, as long as all such hints are posed into the 
goal as hypotheses.  However, deciding whether it would do all forward 
chaining or not is difficult.

For example, I can come up with goals requiring forward chaining that 
firstorder solves quite readily, and others that it doesn't. Here's one 
it doesn't solve:

Goal forall (P : nat -> nat -> Prop),
    (forall i j, P i j -> i + j < 2) ->
    forall x y z, P x y -> P z y -> y > 0 -> x + z < 1.
Proof.
  intros P R x y z Pxy Pyz ygt0.
  Fail firstorder omega.

However, an extra level of firstorder does solve it:

  firstorder (firstorder omega).

I think I see why, based on debugging the goals that are handed to the 
tactic arg (omega in this case), but I'm not sure.  It looks like each 
level of firstorder will parameterize the R formula just once - and 
since omega requires both R x y : x + y < 1 and R x z : x + z < 1, two 
invocation levels of firstorder are needed. But, I don't know if this is 
generally the case.  Could something like:

  Ltac fo n tac := firstorder (tac || lazymatch n with S ?N => fo N tac 
end).

be used to solve any first-order goal, given sufficiently high n? If 
not, what are the properties that first-order goals have to have to be 
solvable this way?

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

Fair enough.  "Help wanted" sign noted...

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

A bit over my head on the first reading...

-- Jonathan