The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 11/09/2015 03:56 PM, Jonathan Leivent wrote:
> 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?

I eventually noticed that "Set Firstorder Depth 4" enables it to solve 
this goal by just "firstorder omega".

-- Jonathan