When writing Ltac in Coq, one might be tempted to write
try match goal with
|- context [?x && true] => rewrite andb_true_r
end
instead of
try rewrite andb_true_r
to not call rewrite pointlessly – this inside the inner loop of a larger tactic, and we expect the rewrite to fail in most cases.
But is that actually faster? Or does rewrite fail just as fast as the hand-written match that I wrote?
Building on your self-answer, Coq is sensitive to the exact matching strategy used. Note the difference between the following tactics:
Require Import Coq.Bool.Bool.
Goal forall b, b = true.
intros.
(* Create a large goal *)
do 300 rewrite <- orb_false_r with (b := b).
Time do 300 try idtac.
(* Finished transaction in 0.001 secs (0.004u,0.s) (successful) *)
Time do 300 try match goal with |- context [_ || true] => idtac end.
(* Finished transaction in 0.108 secs (0.108u,0.s) (successful) *)
Time do 300 try match goal with |- context [_ || ?b] => constr_eq b true end.
(* Finished transaction in 3.21 secs (3.208u,0.s) (successful) *)
Time do 300 try rewrite orb_true_r.
(* Finished transaction in 2.862 secs (2.863u,0.s) (successful) *)
I suspect that rewrite is using a matching strategy similar to the match I wrote with constr_eq; it finds looks at occurrences of orb ?a ?b, and then tries to instantiate evars from left to right and do syntactic equality checking as need be. This incurs a large cost, apparently. I've opened an issue on Coq's bug tracker.
However, this cost might be unavoidable, as rewrite does matching modulo β, unlike your match. Consider:
Goal forall b, b || (fun x => x) true = true.
intros.
Fail match goal with |- context [_ || true] => rewrite orb_true_r end.
rewrite orb_true_r. (* succeeds *)
The speedup is even more apparent in setoid_rewrite, which does rewriting modulo unfolding in many cases, and thus can needlessly perform reduction in your goal, failing over and over and over again.