[Coq-Club] lia: strange performance behavior

[Armaël Guéneau]

Dear coq-club,

Consider the following proof script:


Require Import ZArith Psatz.
Open Scope Z_scope.

Goal forall a b c,
(((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\
((0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\
((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\
(0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\
((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\
((0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)) /\
((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\
(0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)
->
False.
Proof.
intros.
Time Fail Fail lia. (* Succeeds but takes 6s *)
(* trivially split on /\ by hand *)
repeat match goal with h: _ /\ _ |- _ => destruct h end.
Time lia. (* Takes 0.06s *)
Qed.


Does anyone have an explanation? Why is lia struggling so much on the
first goal, and why does manually splitting conjunctions makes it
suddenly much easier?

Cheers,
Armaël

[Frédéric Besson]

Hi Armaël,

I think this is sheer luck that splitting conjunctions improves
performance. My guess is that it is the order of the hypotheses that
matters.

To explain, you need to dig a bit into the algorithm:
To deal with propositional logic, lia puts the formula into a dnf.
Given the number of disjunctions of your formula this is very likely to
explode...
To improve efficiency, some arithmetic reasoning happens on-the-fly
during the dnf conversion.
(In your case, 0 < a and 0 < -a etc will eventually cancel out.)
If this happens early, it is very fast. If it happens later, there are
already many disjuncts and it is slow.

There is of course not completely satisfactory and there are much
better ways of combining propositional logic and arithmetics but this
requires a tighter integration with a SAT solver.

Best,
--
Frédéric

Post by Armaël Guéneau
Dear coq-club,
Require Import ZArith Psatz.
Open Scope Z_scope.
Goal forall a b c,
(((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\
((0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\
((0 < a \/ 0 < b \/ 0 < c) /\ (0 < - b \/ 0 < a \/ 0 < c)) /\
(0 < - a \/ 0 < b \/ 0 < c) /\ (0 < - a \/ 0 < - b \/ 0 < c)) /\
((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\
((0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)) /\
((0 < - c \/ 0 < a \/ 0 < b) /\ (0 < - b \/ 0 < - c \/ 0 < a)) /\
(0 < - a \/ 0 < - c \/ 0 < b) /\ (0 < - a \/ 0 < - b \/ 0 < - c)
->
False.
Proof.
intros.
Time Fail Fail lia. (* Succeeds but takes 6s *)
(* trivially split on /\ by hand *)
repeat match goal with h: _ /\ _ |- _ => destruct h end.
Time lia. (* Takes 0.06s *)
Qed.
Does anyone have an explanation? Why is lia struggling so much on the
first goal, and why does manually splitting conjunctions makes it
suddenly much easier?
Cheers,
Armaël