Unexpected failure of rw tactic

Stream: new members

[Egor Morozov]

I'm sorry if something similar has been already discussed somewhere but I couldn't find.

I have a definition.

noncomputable def Laplacian (n : ℕ) : MvPolynomial (Fin n) ℝ →ₗ[ℝ] MvPolynomial (Fin n) ℝ where
  toFun p := ∑ i, pderiv i (pderiv i p)
  map_add' _ _ := by
    rw [← Finset.sum_add_distrib]
    simp only [map_add]
  map_smul' _ := by
    simp only [Derivation.map_smul, RingHom.id_apply]
    intro _
    rw [Finset.smul_sum]

notation "Δ" => Laplacian

Now when I try

example : Δ 1 (X 0) = 0 := by
  rw [Δ]

I get

tactic 'rewrite' failed, equality or iff proof expected
  MvPolynomial (Fin ?n) ℝ →ₗ[ℝ] MvPolynomial (Fin ?n) ℝ

Could someone explain what is the problem here?

[Robin Arnez]

rw handles identifiers specially, and Δ is not itself an identifier (but a keyword in this case). And alternative might be simp only [Δ ·] (simp has special handling for notation with \.s)

[Egor Morozov]

Okay, somehow lean4 simp only [Δ ·] works and after
dsimp I get what I want so thank you. But I steel don't understand how and why this works... I tried
rw with other linear maps and it was fine. Is there some standard place to read about it?

[Robin Arnez]

Hmm what are examples where it works?

[Egor Morozov]

I tried to find an easy example and came up with

import Mathlib

variable {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]
variable {ι : Type*} (B : Basis ι K V)

noncomputable def f := Basis.constr B K B

example : f B = LinearMap.id := by
  rw [f]
  sorry

However, I'm completely confused here. Clearly,
Basis.constr B K B has type V →ₗ[K] V but then f B just does not make sense... Actually, it shows that the types of f and Basis.constr B K B are different!

[Etienne Marion]

The expression Basis.constr B K B depends on all your variables above. The variable is not here to fix constants, it is here to avoid writing down the same variables in all your declarations. So what you wrote above is actually the same as

import Mathlib

open Module

noncomputable def f {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]
    {ι : Type*} (B : Basis ι K V) := Basis.constr B K B

example {K : Type*} [Field K] {V : Type*} [AddCommGroup V] [Module K V]
    {ι : Type*} (B : Basis ι K V) : f B = LinearMap.id := by
  rw [f]
  sorry

[Etienne Marion]

In your original question I think rw [Laplacian] might work, otherwise simp_rw [Laplacian] or simp [Laplacian] should work.

[Egor Morozov]

Etienne Marion said:

The expression Basis.constr B K B depends on all your variables above. The variable is not here to fix constants, it is here to avoid writing down the same variables in all your declarations. So what you wrote above is actually the same as

Oh, I see, thank you for clarification!

[Egor Morozov]

And rw [Laplacian] works indeed! So it is related with notation somehow??

[Robin Arnez]

Opposite: Identifiers are special, notation is treated like other terms

[Robin Arnez]

It basically expects you to have an a = b as usual