时间戳

首页 > 解决方案 > 仅折叠应用程序

coq - 仅折叠应用程序

问题描述

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

但是，我只想折叠f如果它出现在 context 中(f [ ])，而不是如果它出现在 context 中([ ] f)。特别是repeat myfold (id f)不应该循环。

有没有一种通用的方法来做这种折叠？我现在拥有的最好的是

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

但以上不适用于 form 的上下文forall x, f x = f x。

标签： coqcoq-tactic

解决方案

您可以使用不包含的中间值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) *)

推荐阅读