Performence issue

[thery]

I have some performance issue with goals with large context. The following file takes 25s (only the last two assumptions are needed to solve it) (My real example takes more than 4m)

ex.txt

[pi8027]

IIUC, the source of this issue is that

1. the lia tactic itself does not know the fact that b : bool is true or false (see https://github.com/coq/coq/pull/11906#issuecomment-631191897),
2. the zify tactic teaches lia this fact by case analysis on b, and
3. it produces 1024 cases in your example.

[pi8027]

And this case analysis is performed here. I see the current implementation is too bad to handle the use of boolean predicates and relations in MathComp. https://github.com/coq/coq/blob/12e9f7ea1a2ae3111805fc42f8d75a1a24c36e3f/theories/micromega/ZifyBool.v#L16-L19 https://github.com/coq/coq/blob/12e9f7ea1a2ae3111805fc42f8d75a1a24c36e3f/theories/micromega/ZifyBool.v#L155-L161

[thery]

but what are these 10 booleans in my goal the tactic is finding?

[pi8027]

For example, p1Dp3: is_true (p1 != p3) and sam1C : is_true (codom sam1 \subset [:: pa; p2]) are handled in this way.

[thery]

but they don't contain arithmetic, so lia makes no use of it. Could we disable the bool stuff?

[pi8027]

Then, could you put the following lines at the beginning of your proof script? (NB: it makes lia less powerful in general.)

Ltac Zify.zify_post_hook ::=
  zify_ssreflect.SsreflectZifyInstances.divZ_modZ_to_equations.

[pi8027]

Or if you don't use the Euclidean division at all, its RHS can be idtac.

[thery]

Bingo!

Finished transaction in 0.237 secs (0.23u,0.004s) (successful)

[thery]

could we have a tactic pure_lia that would do lia but with this stuff disable?

[pi8027]

I think it is doable, but doing that without changing the Coq side properly seems another source of potential incompatibility issue. I will rather try to obtain better elim_bool_cstr.

[pi8027]

I think, ultimately, we need an SMT solver (or a rather ad-hoc combination of a SAT solver and a theory solver, at least) to address this kind of exponential blowup. The itauto tactic is probably useful on this point, but I didn't give it a look yet.

[thery]

Very good! Thanks to your new lia I've divided by 3 the compilation time of this file