From 9468ad12ea50d5fcafda669706b65005820a3ba9 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Thu, 11 Jun 2020 17:22:26 +0100
Subject: Coq: specialise the andor solvers to avoid excessive search and solve
 more goals

---
 lib/coq/Values.v | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/lib/coq/Values.v b/lib/coq/Values.v
index 9b76ce62..b0d08670 100644
--- a/lib/coq/Values.v
+++ b/lib/coq/Values.v
@@ -2057,10 +2057,14 @@ Ltac default_andor :=
   repeat match goal with |- @ex _ _ => eexists end;
   rewrite ?Bool.eqb_true_iff, ?Bool.eqb_false_iff in *;
   match goal with
-  | H:?v = true -> _ |- _ = ?v && _ => eapply default_and_proof; eauto
-  | H:?v = true -> _ |- _ = ?v && _ => eapply default_and_proof2; eauto
-  | H:?v = false -> _ |- _ = ?v || _ => eapply default_or_proof; eauto
-  | H:?v = false -> _ |- _ = ?v || _ => eapply default_or_proof2; eauto
+  | H:?v = true -> _ |- _ = ?v && _ => solve [eapply default_and_proof; eauto 2]
+  | H:?v = true -> _ |- _ = ?v && _ => solve [eapply default_and_proof2; eauto 2]
+  | H:?v = false -> _ |- _ = ?v || _ => solve [eapply default_or_proof; eauto 2]
+  | H:?v = false -> _ |- _ = ?v || _ => solve [eapply default_or_proof2; eauto 2]
+  | H:?v = true -> _ |- _ = ?v && _ => solve [rewrite Bool.andb_comm; eapply default_and_proof; eauto 2]
+  | H:?v = true -> _ |- _ = ?v && _ => solve [rewrite Bool.andb_comm; eapply default_and_proof2; eauto 2]
+  | H:?v = false -> _ |- _ = ?v || _ => solve [rewrite Bool.orb_comm; eapply default_or_proof; eauto 2]
+  | H:?v = false -> _ |- _ = ?v || _ => solve [rewrite Bool.orb_comm; eapply default_or_proof2; eauto 2]
   end.
 
 (* Solving simple and_boolMP / or_boolMP goals where unknown booleans
@@ -2117,7 +2121,6 @@ Ltac squashed_andor_solver :=
   | |- context[?li =? ?ri] =>
     specialize (Z.eqb_eq li ri); generalize (li =? ri); intros
   end;
-  rewrite <- ?Z.eqb_eq in *;
   solve_bool_with_Z.
 
 Ltac run_main_solver_impl :=
-- 
cgit v1.2.3