From 8f791df1886d8c80d22d4da19c4153513348f513 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Thu, 19 Sep 2019 09:21:59 -0400
Subject: [PATCH 1/4] profiling for lia in bsearch.v

---
 bedrock2/src/Examples/bsearch.v | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/bedrock2/src/Examples/bsearch.v b/bedrock2/src/Examples/bsearch.v
index 1ded38084..78968cc64 100644
--- a/bedrock2/src/Examples/bsearch.v
+++ b/bedrock2/src/Examples/bsearch.v
@@ -233,6 +233,7 @@ Ltac unsigned_sidecond :=
   wordOps_to_ZModArith;
   repeat ZModArith_step ltac:(lia4).
 
+Set Ltac Profiling.
 
 Local Unset Simplex. (* COQBUG(9615) *)
 Lemma bsearch_ok : program_logic_goal_for_function! bsearch.
@@ -306,3 +307,5 @@ Qed.
 (* SortedListMap *)
 
 Local Set Simplex.
+
+Goal False. idtac "End of binary search profiling.". Abort.

From e5753abb0cfb2994080f400d2d2ec57548e60377 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Thu, 19 Sep 2019 09:30:20 -0400
Subject: [PATCH 2/4] in lia preprocessing, replace Z.div_to_equations by
 Z.div_mod_to_equations, which leads to more challenging lia goals: after a
 few minutes, I get a stack overflow

---
 bedrock2/src/Examples/bsearch.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bedrock2/src/Examples/bsearch.v b/bedrock2/src/Examples/bsearch.v
index 78968cc64..17d388056 100644
--- a/bedrock2/src/Examples/bsearch.v
+++ b/bedrock2/src/Examples/bsearch.v
@@ -130,7 +130,7 @@ Ltac lia3 :=
   | |- _ => lia2
   end.
 
-Ltac lia4 := PreOmega.zify; rewrite ?Z2Nat.id in *; Z.div_to_equations; blia.
+Ltac lia4 := PreOmega.zify; rewrite ?Z2Nat.id in *; Z.div_mod_to_equations; blia.
 
 Module Z.
   Lemma mod_mul_l: forall (a b: Z), (b * a) mod b = 0.

From 05131f2582ae7df4890a3a32f59537740b95904d Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Thu, 19 Sep 2019 09:38:51 -0400
Subject: [PATCH 3/4] add cond_hyps_factor trick by @thery, the lia goals which
 previously caused a stack overflow can now be solved

---
 bedrock2/src/Examples/bsearch.v | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/bedrock2/src/Examples/bsearch.v b/bedrock2/src/Examples/bsearch.v
index 17d388056..861d4e31a 100644
--- a/bedrock2/src/Examples/bsearch.v
+++ b/bedrock2/src/Examples/bsearch.v
@@ -130,7 +130,12 @@ Ltac lia3 :=
   | |- _ => lia2
   end.
 
-Ltac lia4 := PreOmega.zify; rewrite ?Z2Nat.id in *; Z.div_mod_to_equations; blia.
+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.
+
+Ltac lia4 := PreOmega.zify; rewrite ?Z2Nat.id in *; Z.div_mod_to_equations; cond_hyps_factor; blia.
 
 Module Z.
   Lemma mod_mul_l: forall (a b: Z), (b * a) mod b = 0.

From 21f0b06d8d14a2347b2dca49fc37595acb901051 Mon Sep 17 00:00:00 2001
From: Samuel Gruetter <samuel.gruetter@epfl.ch>
Date: Thu, 19 Sep 2019 10:04:52 -0400
Subject: [PATCH 4/4] go back from Z.div_mod_to_equations to
 Z.div_to_equations, cond_hyps_factor makes lia 16% faster

---
 bedrock2/src/Examples/bsearch.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/bedrock2/src/Examples/bsearch.v b/bedrock2/src/Examples/bsearch.v
index 861d4e31a..c6a9e998d 100644
--- a/bedrock2/src/Examples/bsearch.v
+++ b/bedrock2/src/Examples/bsearch.v
@@ -135,7 +135,7 @@ Ltac cond_hyps_factor :=
            | [ H : ?x -> _, H' : ?x -> _ |- _ ] =>
                 pose proof (fun u : x => conj (H u) (H' u)); clear H H' end.
 
-Ltac lia4 := PreOmega.zify; rewrite ?Z2Nat.id in *; Z.div_mod_to_equations; cond_hyps_factor; blia.
+Ltac lia4 := PreOmega.zify; rewrite ?Z2Nat.id in *; Z.div_to_equations; cond_hyps_factor; blia.
 
 Module Z.
   Lemma mod_mul_l: forall (a b: Z), (b * a) mod b = 0.