nia fails slowly on an example of its incompleteness

[andres-erbsen]

Description of the problem

Require Import Lia ZArith.
Local Open Scope Z_scope.

Goal forall
  (m : Z)
  (Hm : 1 < m < m * m)
  (r3 q3 r4 q4 r0 q2 q0 q1 r1 r2 q r : Z)
  (H0 : 0 <= r < m * m)
  (H : (m * q3 + r3) * (m * q4 + r4) = m * m * q + r)
  (H4 : q3 * r4 = m * q0 + r0)
  (H5 : 0 <= r0 < m)
  (H9 : q2 + r0 + r3 * q4 = m * q1 + r1)
  (H10 : 0 <= r1 < m)
  (H14 : r3 * r4 = m * q2 + r2)
  (H15 : 0 <= r2 < m)
  (H20 : 0 <= r3 < m)
  (H25 : 0 <= r4 < m)
  (H1 : 0 <= q4 < m)
  (H2 : 0 <= q3 < m)
  (Ha : 0 <= m * q3 + r3 < m * m)
  (Hb : 0 <= m * q4 + r4 < m * m)
  , q0 + q1 + q3 * q4 = q /\ r1 * m + r2 = r.
Proof.
  intros.
  Time Fail nia. (* 10s *)
Abort.

The goal is actually true; it can be proven by asserting the first conjunct and ; nia. Both nia calls run fast in that case.

Ltac cleardisj :=
  repeat match goal with
  | H : _ -> _ |- _ => clear H
  | H : _ \/ _ |- _ => clear H
  end.
Ltac cleanby tac :=
  repeat lazymatch goal with
  | H : ?A -> ?B |- _ =>
      specialize (H ltac:(tac))
      || (assert (not A) as _ by (clear H; tac); clear H)
      || revert H
  | H : ?B |- _ =>
      (assert B as _ by (clear H; tac); clear H)
      || revert H
  end; intros; subst.
Ltac divby tac :=
  repeat lazymatch goal with
    H : 0 <= ?m * ?q + _ < ?m*?m |- _ =>
        try assert (0 <= q < m) by tac; revert H
  end; intros.

Goal forall 
  m M (Hm : 1 < m < M) (HM : M = m*m)
  a (Ha : 0 <= a < M)
  b (Hb : 0 <= b < M)
  ll (Hll : ll = (a mod m) * (b mod m))
  hl (Hhl : hl = (a/m) * (b mod m))
  lh (Hlh : lh = (a mod m) * (b/m))
  hh (Hll : hh = (a/m) * (b/m))
  tm (Htm : tm = (ll/m) + (hl mod m) + lh)
  rh (Hrh : rh = (hl/m) + (tm/m) + hh)
  rl (Hrl : rl = (tm * m mod M) + (ll mod m))
  ,
  rh = a * b / M /\
  rl = a * b mod M.
Proof.
  intros.
  subst M.
  rewrite Z.mul_mod_distr_r in Hrl by (cleardisj; lia). (* needed for last nia *)
  Time Z.div_mod_to_equations.
  Time cleanby ltac:(cleardisj; lia).
  Fail progress cleanby ltac:(cleardisj; nia).
  Time progress divby ltac:(cleardisj; lia).
  Time progress divby ltac:(cleardisj; nia).
  (* Time Fail nia. (* 9s *) *)
  match goal with |- ?A /\ _ => assert A; try split; trivial end.
  nia.
  nia.
Qed.

Coq Version

8.16.0