diff options
| author | Brian Campbell | 2020-06-11 17:22:26 +0100 |
|---|---|---|
| committer | Brian Campbell | 2020-06-11 17:22:26 +0100 |
| commit | 9468ad12ea50d5fcafda669706b65005820a3ba9 (patch) | |
| tree | 182e8043b18ec5683bc337b590e540be174eb0d6 | |
| parent | d2b4a7a1d654cf8f315e2471b1470506255f3d68 (diff) | |
Coq: specialise the andor solvers to avoid excessive search and solve more goals
| -rw-r--r-- | lib/coq/Values.v | 13 |
1 files 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 := |