Rewriting by eta-equivalence

Using Coq
1

Is there a built-in tactic that would reduce fun x => f x to f or the other way around? cbv doesn’t do that. I guess you can rewrite eta, where eta is the lemma below, but maybe I’m missing something even simpler.

Lemma eta {A B} (f : A -> B) : (fun x => f x) = f.
Proof.
cbv. (* I would like to see f = f now *)
reflexivity. (* this proof works in any case, but sometimes syntax matters (rewriting, match...) *)
Qed.

I thought there were situations where fun x => f x is directly transformed into f but I can’t seem to find an example of that.

1 Like
2

What about change (fun x => f x) with f?

2 Likes
3

change understands patterns, so if you’d like to eta-reduce all things in your goal, you could use something like this:

repeat change (fun x => ?h x) with h.
5 Likes
4

I hadn’t thought about change and didn’t know it supports patterns!
Thanks a lot @mwuttke97 and @anton-trunov!

1 Like
5

I just found the section in the Coq manual about conversion: Typing rules — Coq 8.18.0 documentation

It has some relevant comments about eta:

We deliberately do not define η-reduction (…) This is because, in general, the type of t need not to be convertible to the type of fun x => t x.

2 Likes