Folding only applications

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

fold

fold (id f)

f

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

f

(f [ ])

([ ] f)

repeat myfold (id f)

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.

forall x, f x = f x

1 Answer
1

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

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


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


(g f)

(g (id f))

g f

g (id f)

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.