Folding only applications

Question

The fold tactic replaces all occurrence of a term with another, so fold (id f) tries to replace all occurrences of f with (id f).

However, I want to only fold f if it occurs in the context (f [ ]), not if it occurs in the context ([ ] f). In particular repeat myfold (id f), should not loop.

Is there a general way to do this type of folding? The best I have right now is

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

But the above does not work for contexts of the form forall x, f x = f x.

Answer 1

You can use an intermediate value not containing f. Something like

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'.

Edit

If you actually want to just fold things in applicative contexts, you can use three intermediate values, like this:

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