lia does not terminate in the presence of a section variable

[fpottier]

Description of the problem

A statement that can be normally proved by lia causes divergence if the hypothesis unsigned n is turned into a section variable. Note that the definition of unsigned involves the very large constant wB (which is 2^63).

Note: this is not an artificial example... I have run into this problem in a real proof.

Thanks!

Small Rocq / Coq file to reproduce the bug

From Stdlib Require Import ZArith Lia.
From Stdlib Require Import Uint63 ZifyUint63.

Open Scope Z_scope.

Notation unsigned z :=
  (0 <= z < wB).

(* This proof works: *)

Goal forall n : Z, unsigned n -> 0 < n -> unsigned (n-1).
Proof. lia. Qed.

(* Now let's try the same thing again, using a section: *)

Section S.

Variable n : Z.
Variable bound_n : unsigned n.

Goal True.
Proof.
  lia. (* does not terminate! *)
Qed.

End S.

Version of Rocq / Coq where this bug occurs

No response

Interface of Rocq / Coq where this bug occurs

No response

Last version of Rocq / Coq where the bug did not occur

No response

[fpottier]

PS. I am using Rocq 9.1.

[yannl35133]

This issue got fixed by #21987

[yannl35133]

There is still an issue, because the following still doesn't terminate:

From Stdlib Require Import ZArith Lia.
From Stdlib Require Import ZifyUint63.

Section S.
Open Scope Z_scope.
Variable n : Z.
Variable bound_n : 0 <= n < 1.

Goal True.
Proof.
  lia. (* does not terminate! *)
Qed.

End S.

[yannl35133]

Got to the end of it:
The issue comes from PreOmega.euclidean_division_equations_cleanup which repeatedly destructs any hypothesis of the shape 0 <= ?x < _. However, using destruct on a section variable doesn't clear it. So this happens ad infinitum.
#21987 only "fixed it" because wB contains a call to Z.of_nat which gets simplified early during zify, and the PR made it so that any change to a section variable changes the status to proof variable, which do get erased after destruct.