# Rewriting by eta-equivalence

**URL:** <https://discourse.rocq-prover.org/t/rewriting-by-eta-equivalence/356>\
**Category:** Using Rocq\
**Created:** [July 13, 2019, 3:56pm UTC](https://discourse.rocq-prover.org/t/rewriting-by-eta-equivalence/356 "2019-07-13T15:56:10Z")\
**Posts on this page:** 5\
**Page:** 1

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [July 13, 2019, 3:56pm UTC](https://discourse.rocq-prover.org/t/rewriting-by-eta-equivalence/356/1 "2019-07-13T15:56:10Z")

</div>

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.

```auto
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.

---

<div class="post-metadata">

**Author:** ![mwuttke97](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/mwuttke97/32/104_2.png) [@mwuttke97](https://discourse.rocq-prover.org/u/mwuttke97)\
**Post date:** [July 13, 2019, 5:08pm UTC](https://discourse.rocq-prover.org/t/rewriting-by-eta-equivalence/356/2 "2019-07-13T17:08:51Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![anton-trunov](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/anton-trunov/32/54_2.png) [@anton-trunov](https://discourse.rocq-prover.org/u/anton-trunov)\
**Post date:** [July 13, 2019, 5:57pm UTC](https://discourse.rocq-prover.org/t/rewriting-by-eta-equivalence/356/3 "2019-07-13T17:57:23Z")

</div>

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

```auto
repeat change (fun x => ?h x) with h.

```

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [July 13, 2019, 6:10pm UTC](https://discourse.rocq-prover.org/t/rewriting-by-eta-equivalence/356/4 "2019-07-13T18:10:46Z")

</div>

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

---

<div class="post-metadata">

**Author:** ![Lyxia](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lyxia/32/75_2.png) [@Lyxia](https://discourse.rocq-prover.org/u/Lyxia)\
**Post date:** [July 15, 2019, 2:33pm UTC](https://discourse.rocq-prover.org/t/rewriting-by-eta-equivalence/356/5 "2019-07-15T14:33:16Z")

</div>

I just found the section in the Coq manual about conversion: [Typing rules — Coq 8.18.0 documentation](https://coq.inria.fr/refman/language/cic.html#conversion-rules)

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