How to rw `f`to `fun x => f x`?

Stream: new members

[Adomas Baliuka]

I find myself using rw a lot to go between a function and lambdas. What's the idiomatic way to do this?

import Mathlib
open Real

/- TODO how to not need this lemma? -/
lemma Function.eq_lambda {α β : Type*} (f : α → β) : f = fun x ↦ f x := rfl

-- example use
noncomputable def sin_sin x := sin (sin x)

example : Continuous sin_sin := by
  rw [Function.eq_lambda sin_sin]
  simp [sin_sin]
  apply Continuous.comp' <;> apply continuous_sin

[Kevin Buzzard]

Try unfold sin_sin and then continuity?

[Adomas Baliuka]

Yes, continuity works. I want to know in general what to do when one has finside some expression and one needs fun x => f x. Or should such situations not happen?

[Kyle Miller]

https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Tactic/DefEqTransformations.lean has a number of tactics for transforming expressions in different ways. The eta_expand tactic does that transformation to all under-applied functions.

[Kyle Miller]

I'm not sure it's used anywhere in mathlib, so caveat emptor

[Adomas Baliuka]

Yes, I was looking for eta_expand. Thanks! Any advice how I could have found it myself?

[Kyle Miller]

(1) Guessing it might be called eta_expansion if you happen to know the greek letter associated to this lambda calculus rule, (2) consulting the not-yet-existing list of all the mathlib tactics in the mathlib docs (though someone's generated this in the meantime), (3) asking here and hoping someone familiar with a tactic is around (I wrote this one, so I knew it existed :smile:)

[Matt Diamond]

Are there cases where transformations between defeq terms are necessary? I would think definitional equality means X will suffice whenever Y will

[Adomas Baliuka]

In my original example, if you remove the eta_expand (or the lemma I made that does the same), the proof no longer works.

[Matt Diamond]

Right, I see... I'm surprised that it's necessary there

[Matt Diamond]

maybe it's a quirk of the way simp does unfolding... as Kevin pointed out, using unfold directly doesn't require the rewrite

[Adomas Baliuka]

Yes, I was wondering what's the point of unfold... I guess it does unfold better than simp

[Kyle Miller]

simp only applies equation lemmas, and equation lemmas are generally for fully applied functions. unfold will unfold a definition even if it's not fully applied.

[Kyle Miller]

I think there was a suggestion to have simp [!sin_sin] do unfold-style unfolding, but I'm not sure if that's graduated from being a mere idea.

[Kyle Miller]

I had this simp problem sort of in mind when I added eta_expand, but it's also there as an inverse to eta_reduce.

[Kyle Miller]

I think this sort of example might have been the inspiration:

example (f g : ℕ → ℝ) : Continuous (f + g) := by
  eta_expand
  simp only [Pi.add_apply]
  -- ⊢ Continuous fun a ↦ f a + g a
  sorry

[Matt Diamond]

@Kyle Miller While we're on the topic of defeq transformations, is there a reason this doesn't seem to work?

import Mathlib.Tactic.DefEqTransformations

example {α : Type*} (y : α) (f : α → α) : True := by
  let q := (fun x => f x) y
  beta_reduce at q -- no change
  trivial

Or am I just misunderstanding how it's meant to be used?

[Matt Diamond]

Does it only apply to types rather than terms?

[Kyle Miller]

Yeah, only types of local hypotheses, no let values.

[Kyle Miller]

You could make such a tactic that transforms the values though.

[Kyle Miller]

(Maybe it could be a configuration option to beta_reduce and all the other defeq tactics in that file, if this is useful to do.)

[Kevin Buzzard]

Matt Diamond said:

Are there cases where transformations between defeq terms are necessary? I would think definitional equality means X will suffice whenever Y will

Tactics like rw work up to syntactic equality, so sometimes you need to make a definitional change before rewriting.