`firstorder lia` fails with "No link."

[samuelgruetter]

Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Open Scope Z_scope.

Axiom stmt: Type.
Axiom P: (Z -> Prop) -> stmt -> Prop.

Goal forall x s s' m m',
  (m' <= m ->
   P (fun x : Z => 5 < x <= m) s ->
   P (fun x : Z => 2 < x <= 32) s') ->
  Z.max x m' <= m ->
  P (fun x : Z => 5 < x <= m) s ->
  P (fun x0 : Z => 2 < x0 <= 32) s'.
Proof.
  intros.
  firstorder lia.

fails with a cryptic Error: Tactic failure: No link., whereas this solves the goal:

  apply H. lia. assumption.
Qed.

I assume it fails because this goal is not first order logic?

Desired behavior: It should fail with "Not a first order logic goal" or it should solve the goal.

Coq version: 8.11.0

[KevOrr]

Running into this as well with

Require Import Lia.

Theorem foo P k (H : forall x, x < k -> P x) n (H2 : n < k - 1) : P n.
  firstorder lia.

Tracing through with Set Ltac Debug, it eventually calls lia in the context

  P : nat -> Type
  k : nat
  H : forall x : nat, x < k -> P x
  n : nat
  H2 : n < k - 1
  X : n < k -> P n
  ============================
  P n

That obviously fails, so it ends up calling lia without X in the context. This also fails, so firstorder fails. What's interesting to me is that it never tries applying H or X the goal, which would result in a subgoal that lia can solve.

[mrhaandi]

Here is another minimal example of the unexpected Tactic failure: No link. issue:

Require Import Lia.
Axiom P: Prop.

Goal forall (n : nat), (n - 0 = n -> P) -> P.
Proof.
  intros n H.
  Fail firstorder lia. (* Tactic failure: No link. *)
  apply H. lia. (* No more subgoals. *)
Qed.

In the above, firstorder lia does absolutely nothing before calling lia and failing.

[mrhaandi]

As a side note, the original example by @samuelgruetter (using Axiom P: (Z -> Prop) -> stmt -> Prop.) is more related to lia. The issue is that firstorder eagerly unfolds a comparison in Z which lia cannot handle without additional info. Therefore, with Require Import ZifyComparison. the tactic firstorder lia. solves the goal.