`match` 能比 `rewrite` 快吗

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

是的，是的！我的一项战术取得了 60% speed-up。

这是另一个 micro-benchmark 显示此行为的例子：

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.

Answer 2

基于您的 self-answer，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使用的匹配策略类似于我用constr_eq写的match；它查找 orb ?a ?b 的出现，然后尝试从左到右实例化 evar，并根据需要进行句法相等性检查。显然，这会产生很大的成本。我打开了 an issue on Coq's bug tracker.

但是，这个成本可能是不可避免的，因为 rewrite 会匹配模 β，这与您的 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 中更为明显，它在许多情况下会重写模展开，因此可能会不必要地减少你的目标，一遍又一遍地失败。

`match` 能比 `rewrite` 快吗

Can `match` be faster than `rewrite`

coq

coq-tactic