Slow lia goal

[samuelgruetter]

Here's a goal on which lia (and omega as well) is very slow:

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

Goal
  forall (r2 : Z) (L : nat),
  r2 = 8 * Z.of_nat L ->
  r2 <> 0 ->
  0 <= Z.of_nat L ->
  forall q r r1 : Z,
  (2 ^ r1 <> 0 -> r2 = 2 ^ r1 * q + r) ->
  (0 < 2 ^ r1 -> 0 <= r < 2 ^ r1) ->
  (2 ^ r1 < 0 -> 2 ^ r1 < r <= 0) ->
  (2 ^ r1 = 0 -> q = 0) ->
  (2 ^ r1 = 0 -> r = 0) ->
  forall q0 r0 M : Z,
  (M <> 0 -> 3 = M * q0 + r0) ->
  (0 < M -> 0 <= r0 < M) ->
  (M < 0 -> M < r0 <= 0) ->
  (M = 0 -> q0 = 0) ->
  (M = 0 -> r0 = 0) ->
  forall q1 : Z,
  (M <> 0 -> 4 = M * q1 + r1) ->
  (0 < M -> 0 <= r1 < M) ->
  (M < 0 -> M < r1 <= 0) ->
  (M = 0 -> q1 = 0) ->
  (M = 0 -> r1 = 0) ->
  forall q2 y1 y2 : Z,
  (M <> 0 -> y2 - y1 = M * q2 + r2) ->
  (0 < M -> 0 <= r2 < M) ->
  (M < 0 -> M < r2 <= 0) ->
  (M = 0 -> q2 = 0) -> (M = 0 -> r2 = 0) ->
  0 <= y2 - (y1 + q * 2 ^ r0 + 8) < M.
Proof.
  intros.
  Time lia.

Note that lia can't solve this, and that's fine, but I would like lia to fail faster, so that I can write proof scripts which try many things.
In Coq 8.9.0, this takes 80s, and in Coq master, this takes 15s using coqc from the command line, and interestingly, it takes 40s-50s in Proof General.

/cc @andres-erbsen @fajb

[ppedrot]

FTR, I don't see anything suspicious in the profiling on 110e87a. It is likely a genuinely hard problem, all the time is spent in CNF normalization of micromega.

[amahboubi]

@ppedrot : the goal features subterms like 2 ^ r0 or M * q2 or even 2 ^ r1 * q. If the corresponding hypotheses are really useful in the proof, then this is clearly not a goal lia or omega can possibly deal with. I guess this is what @samuelgruetter means when he wishes the tactics fail earlier.

[thery]

I think it has to do with the exponential CNF phase here is a more contrived example

Goal 
  forall x y,
   (x = 0 -> y = 0) ->
   (x = 1 -> y = 0) ->
   (x = 2 -> y = 0) ->
   (x = 3 -> y = 0) ->
   (x = 4 -> y = 0) ->
   (x = 5 -> y = 0) ->
   (x = 6 -> y = 0) ->
   (x = 7 -> y = 0) ->
   (x = 8 -> y = 0) ->
   (x = 9 -> y = 0) ->
   (x = 0 -> y = 0) ->
   (x = 1 -> y = 0) ->
   (x = 2 -> y = 0) ->
   (x = 3 -> y = 0) ->
   (x = 4 -> y = 0) ->
   (x = 5 -> y = 0) ->
   (x = 6 -> y = 0) ->
   (x = 7 -> y = 0) ->
   (x = 8 -> y = 0) ->
   (x = 9 -> y = 0) ->
   x = 1.
Proof.
  intros.
  Time lia.

[ppedrot]

@amahboubi indeed, but it's still hard to get a reasonable heuristic that wouldn't endanger the results of the tactics. It might be the case that you use the exponentials in some opaque way.

@thery I concur, but even if the algorithm is exponential there is room for improvement. With two trivial optimizations below (directly in OCaml but that should be backported to the Coq source), @samuelgruetter's example fails three times faster.

diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index cd620bd4a9..63d84544e7 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -1075,11 +1075,8 @@ let or_clause_cnf unsat deduce t0 f =
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1, 'a2) cnf -> ('a1,
     'a2) cnf -> ('a1, 'a2) cnf **)
 
-let rec or_cnf unsat deduce f f' =
-  match f with
-  | [] -> cnf_tt
-  | e::rst ->
-    app (or_cnf unsat deduce rst f') (or_clause_cnf unsat deduce e f')
+let or_cnf unsat deduce f f' =
+  CList.map_append (fun e -> or_clause_cnf unsat deduce e f') f
 
 (** val and_cnf : ('a1, 'a2) cnf -> ('a1, 'a2) cnf -> ('a1, 'a2) cnf **)
 
@@ -1162,7 +1159,7 @@ let ror_clause_cnf unsat deduce t0 f =
     let acc,tg = pat in
     (match ror_clause unsat deduce t0 e with
      | Inl cl -> (cl::acc),tg
-     | Inr l -> acc,(app tg l))) ([],[]) f
+     | Inr l -> acc,(l :: tg))) ([],[]) f
 
 (** val ror_cnf :
     ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list list ->
@@ -1174,7 +1171,7 @@ let rec ror_cnf unsat deduce f f' =
   | e::rst ->
     let rst_f',t0 = ror_cnf unsat deduce rst f' in
     let e_f',t' = ror_clause_cnf unsat deduce e f' in
-    (app rst_f' e_f'),(app t0 t')
+    (app rst_f' e_f'),(app t0 (List.concat @@ List.rev t'))
 
 (** val rxcnf :
     ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a3 -> ('a2, 'a3)
diff --git a/plugins/micromega/micromega.mli b/plugins/micromega/micromega.mli
index 6da0c754f4..bdd72ab19f 100644
--- a/plugins/micromega/micromega.mli
+++ b/plugins/micromega/micromega.mli
@@ -317,7 +317,7 @@ val ror_clause :
 
 val ror_clause_cnf :
   ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list -> ('a1, 'a2) clause
-  list -> ('a1, 'a2) clause list * 'a2 list
+  list -> ('a1, 'a2) clause list * 'a2 list list
 
 val ror_cnf :
   ('a1 -> bool) -> ('a1 -> 'a1 -> 'a1 option) -> ('a1 * 'a2) list list -> ('a1, 'a2)

The morale is that we shouldn't append lists one by one...

[amahboubi]

On the other hand, it is quite easy in this case to see that the formula is false, e.g. with M = 0 = y1 = y2. I suspect being able to test the property in parallel would provide the fastest failure in a number of cases.

[fajb]

It is good to know that the CNF can be a bottleneck.
@ppedrot do not hesitate to submit your optimisation.

Eventually, the solution is to not use a CNF...
What we would need is a decent sat solver/ SMT core to deal with propositional logic.
Maybe, intuition lia could be adapted to explore in a depth-first fashion, thus allowing lia to fail faster.

[ppedrot]

@fajb I am working on the Coq backport. Is it still the case that we generate micromega.ml out of the Coq file, or does the OCaml file already contain some handwritten tweaks?

[fajb]

Yes, micromega.ml is still extracted.
You need to un-comment and run MExtraction.v

[ppedrot]

The mli file seems to be handwritten though, as extracting it on master results in a slightly different file. Should I reextract it, or adapt it by hand?

[fajb]

I guess this is to pass the test-suite which indeed extracts in a slightly different way -- and complains about the formatting.
Because I do not know how to fix it, I ususally run the test-suite and copy the expected result back in micromega.ml/mli...

[thery]

@samuelgruetter your example seems to contain lots of conditionals with the same condition.
Factorizing out these hyps can drastically help omega/lia.

If you define

Ltac cond_hyps_factor :=
    repeat match goal with
           | [ H : ?x -> _, H' : ?x -> _ |- _ ] => 
                pose proof (fun u : x => conj (H u) (H' u)); clear H H' end.

now on your example

intros; cond_hyps_factor; lia

fails almost immediately.

Of course, this may work only if you have many expressions on the same modulo. I would be very interested to know if this little trick makes lia/omega usable again in your applicattion.

[fajb]

@thery very nice.
It may also make sense to do the same for any disjunction...

[thery]

apparently the benefit is not so big. I've been the victim of some cache effect of lia.
I thought that caching was only trigger for positive result.....

[samuelgruetter]

I experienced some inconsistent timings/surprises too while experimenting with lia timings. Is there a way to turn off lia caching?