Weird behavior with Function.comp with and without Mathlib

Stream: mathlib4

[Valentin Vinoles]

Hello

I do not understand why the first example works and the second is not. It seems that rw [Function.comp] does not have the same behavior if mathlib is imported or not. Is it intended ?

Without Mathlib:

variable {α β : Type}

example (f : α → β) : id ∘ f = f := by
  apply funext        -- ⊢ ∀ (x : α), (id ∘ f) x = f x
  intro x             -- x: α
                      -- ⊢ (id ∘ f) x = f x
  rw [Function.comp]  -- ⊢ id (f x) = f x
  rw [id]             -- No goals

And with Mathlib:

import Mathlib

variable {α β : Type}

example (f : α → β) : id ∘ f = f := by
  apply funext        -- ⊢ ∀ (x : α), (id ∘ f) x = f x
  intro x             -- x: α
                      -- ⊢ (id ∘ f) x = f x
  rw [Function.comp]  -- ⊢ (fun x ↦ id (f x)) x = f x
  rw [id]             -- failed to rewrite using equation theorems for 'id'

[Kyle Miller]

mathlib overrides the equation theorems for Function.comp right here to use docs#Function.comp_def because the default for equation lemmas -- after a change to Lean in the last couple months -- is that they only apply to fully-applied functions (like (id ∘ f) x), but for operators like composition, you want to be able to rewrite the composition itself (like id ∘ f).

(Pinging @Eric Wieser about upstreaming this to std, since there was talk about this when the equation theorem was changed)

A workaround is to use unfold. You can use unfold id instead of rw [id].

[Valentin Vinoles]

@Kyle Miller
Thanks for your answer, but to be honest I am not sure I completely understand it.

[Valentin Vinoles]

With Mathlib imported, if I want to transform (g ∘ f) x into g (f x), how can I do that ?

[Kyle Miller]

You use docs#Function.comp_apply

variable {α β γ : Type}

example (f : α → β) (g : β → γ) (x y) : (g ∘ f) x = y := by
  rw [Function.comp_apply]
  -- ⊢ g (f x) = y
  sorry

[Kyle Miller]

Generally speaking, mathlib is designed where you rewrite using theorems, and you are not expected to unfold definitions.

[Valentin Vinoles]

Ho I see. I am doing really basic stuffs: my ultimate goal is to teach some basic formalization to undergraduate students. So I need to unfold if I want to prove stuffs about functions (like id ∘ f = f) . I can try do to it without Mathlib, but it has some nice tactics... Not sure what will be the best choice at the end !

[Valentin Vinoles]

Thanks anyway !

[Kyle Miller]

I mentioned it as a workaround earlier, but really I'd suggest using unfold if you're unfolding rather than rw

[Kyle Miller]

Well, I suppose that can potentially introduce fun terms, but you can follow that up with dsimp only