“匹配”可以比“重写”更快

Question

在Coq写Ltac时，人们可能会想写

try match goal with
 |- context [?x && true] => rewrite andb_true_r
end

代替

try rewrite andb_true_r

没有毫无意义地调用rewrite - 这是一个更大的策略的内部循环，我们希望在大多数情况下重写失败。

但这实际上更快吗？或者rewrite失败的速度和我写的手写的match一样快吗？

Answer 1

在您自我回答的基础上，Coq对所使用的精确匹配策略很敏感。注意以下策略之间的区别：

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) *)

我怀疑rewrite正在使用类似于我用match写的constr_eq的匹配策略;它找到orb ?a ?b的出现，然后尝试从左到右实例化evars并根据需要进行语法相等检查。显然，这会产生很大的成本。我打开了an issue on Coq's bug tracker。

然而，这个成本可能是不可避免的，因为rewrite确实匹配moduloβ，不像你的match。考虑：

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 *)

在setoid_rewrite中加速更加明显，在许多情况下它会重写模数展开，因此可以不必要地减少你的目标，一次又一次地失败。

Answer 2

是的！在我的一个策略中，我实现了60％的加速。

以下是显示此行为的另一个微基准测试：

Require Import Coq.Bool.Bool.

Goal forall b, b = true.
intros.
(* Lets create a large goal *)
do 300 rewrite <- orb_false_r with (b := b).
Time do 300 try rewrite orb_true_r.
(* Finished transaction in 2.57 secs (2.431u,0.003s) (successful) *)
Time do 300 try lazymatch goal with |- context [_ || true] => rewrite orb_true_r end.
(* Finished transaction in 0.05 secs (0.05u,0.s) (successful) *)
Abort.