仅折叠应用程序

Question

fold 策略将所有出现的术语替换为另一个术语，因此 fold (id f) 尝试将所有出现的 f 替换为 (id f)。

但是，我只想折叠出现在上下文 (f [ ]) 中的 f，而不是出现在上下文 ([ ] f) 中的折叠。特别是repeat myfold (id f)，不应该循环。

这种折叠有通用的方法吗？我现在最好的是

repeat match goal with
| |- context [(f ?x)] => change (f x) with ((id f) x)
end

但以上不适用于 forall x, f x = f x.

形式的上下文

Answer 1

您可以使用不包含 f 的中间值。像

let f' := fresh in
pose (id f) as f';
change f with f'
change (id f') with f'; (* undo the change in locations where we've already added id *)
subst f'.

编辑

如果你真的只想在应用上下文中折叠东西，你可以使用三个中间值，如下所示：

(* Copyright 2018 Google LLC.
   SPDX-License-Identifier: Apache-2.0 *)
Ltac myfold_id f :=
  let id_f := fresh in
  let id_f_good := fresh in
  let f' := fresh in
  pose (id f) as id_f;
  pose (id f) as id_f_good;
  pose f as f';
  repeat (change f with id_f at 1;
          lazymatch goal with
          | [ |- context[id_f _] ] => change id_f with id_f_good
          | _ => change id_f with f'
          end);
  subst id_f id_f_good f'.
Goal let f := id in (f = f, f 0) = (f = f, f 0).
Proof.
  intro f.
  (* (f = f, f 0) = (f = f, f 0) *)
  myfold_id f.
  (* (f = f, id f 0) = (f = f, id f 0) *)

仅折叠应用程序

Folding only applications

coq

coq-tactic