Adding an AddCommMonoid instance breaks rw tactic

Stream: general

[Strategist _]

I've been working on proving some results about the heat equation in Lean 4, and I wanted to use a lemma that the heat equation operator is linear in a proof. However, when trying to rewrite a statement using the linearity lemma, it kept telling me that it couldn't find an instance of the pattern, even when I manually provided all the arguments so the pattern was identical to the input.

After a lot of experimentation, I discovered that when I comment out a specific AddCommMonoid instance, it does recognize the pattern in the rw, and everything works as expected.

Can anyone explain to me why the existence of that AddCommMonoid instance is causing rw to not recognize the pattern?

Here's a minimal working example:

import Mathlib.Analysis.Calculus.ContDiff.Defs
import Mathlib.MeasureTheory.Constructions.Pi
import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
import Mathlib.MeasureTheory.Measure.Haar.OfBasis

open Real
open Finset
open Fin
open MeasureTheory
open Nat
open MeasurableEquiv
open ENNReal
open Filter Topology
open NNReal

-- A bunch of definitions required to set up the statement
@[reducible]
noncomputable def Lp_loc (d : ℕ+) (p : ℝ≥0∞) : AddSubgroup ((Fin d → ℝ) →ₘ[volume] ℝ) where
  carrier := {f | (∀ (C : Set (Fin d → ℝ)), IsCompact C → Memℒp f p (MeasureTheory.Measure.restrict (volume : Measure (Fin d → ℝ)) C))}
  zero_mem' := by sorry
  add_mem' {f g} hf hg := by sorry
  neg_mem' {f} hf := by sorry
noncomputable def Wkp (d : ℕ+) (k : ℕ) (p : ℝ≥0∞) : AddSubgroup (Lp_loc d 1) where
  carrier := sorry
  zero_mem' := by sorry
  add_mem' := by sorry
  neg_mem' := by sorry
noncomputable def Wkp0 (d : ℕ+) (k : ℕ) (p : ℝ≥0∞) : AddSubgroup (Wkp d k p) where
  carrier := sorry
  zero_mem' := by sorry
  add_mem' := by sorry
  neg_mem' := by sorry

@[reducible]
noncomputable def Hk0 (d : ℕ+) (k : ℕ) := Wkp0 d k 2
instance instHk0Module {d : ℕ+} {k : ℕ} : Module ℝ (Hk0 d k) := sorry

noncomputable def weak_heat_operator_1D {d : ℕ+} (u : ℝ → Hk0 d 1) : (Hk0 d 1) → ℝ → ℝ := sorry
lemma weak_heat_operator_1D_linear {F : Type} [Fintype F] {d : ℕ+} {u : ℝ → Hk0 d 1} {t : ℝ} :
  ∀ (f : F → (Hk0 d 1)), weak_heat_operator_1D u (∑ (k : F), f k) t = ∑ (k : F), weak_heat_operator_1D u (f k) t := by sorry
-- Done setup definitions


-- This line somehow makes rw not recognize the linearity lemma
instance stupid_thing {d: ℕ+} {k : ℕ} : AddCommMonoid (Hk0 d k) := sorry

lemma test (um : ℕ → ℝ → (Hk0 1 1)) (dk : Fin N → { f : ℝ → ℝ // ContDiff ℝ ⊤ f }) (w : ℕ → (Hk0 1 1)) : ∀ (t : ℝ), weak_heat_operator_1D (fun τ ↦ um m τ) (∑ (k : Fin N), ((dk k).val t) • (w k)) t = 0 := by
  intro t
  rw [weak_heat_operator_1D_linear]

  -- Even specifying all the arguments manually doesn't work
  -- rw [@weak_heat_operator_1D_linear (Fin N) inferInstance 1 (fun τ ↦ um m τ) t (fun k ↦ (dk k).val t • w k)]
  sorry

[Aaron Liu]

That example doesn't work for me. What version of mathlib are you on?

[Yakov Pechersky]

You shouldn't need to give an AddCommMonoid instance to the AddSubgroup, it's already an AddMonoid

[Yakov Pechersky]

If you declare a separate instance, then things can't realize they refer to the same addition

[Strategist _]

Aaron Liu said:

That example doesn't work for me. What version of mathlib are you on?

"4.17.0-rc1" apparently

[Aaron Liu]

That's a Lean version :|

[Strategist _]

Aaron Liu said:

That's a Lean version :|

Whoops yeah it is. Misread what you were asking for. It's from this commit of mathlib 4 from back in February https://github.com/leanprover-community/mathlib4/commit/c7a2a04be15f08bc892687f61b11059b43c8cb3b

[Strategist _]

Yakov Pechersky said:

If you declare a separate instance, then things can't realize they refer to the same addition

Oh ok, so it's because the rw is looking for an AddMonoid instance, and the AddSubgroup version conflicts with the AddCommMonoid instance?

In that case, what do I do if I need specifically an AddCommMonoid instead of just and AddMonoid for some other purpose later? It doesn't seem like it can use inferInstance to create an AddCommMonoid by itself, presumably because when I make an AddSubgroup it doesn't specify that it's commutative.

[Aaron Liu]

If you just specify the add_comm field, Lean should be able to infer the rest, and it will unify without problems.

instance stupid_thing {d: ℕ+} {k : ℕ} : AddCommMonoid (Hk0 d k) where
  add_comm := sorry

[Eric Wieser]

Yakov Pechersky said:

If you declare a separate instance, then things can't realize they refer to the same addition

This isn't entirely true; if the additions are the same then usually lean can tell. The problem here is that one addition is "the thing you expect", and the other is (sorry : AddCommMonoid _).add, and those simply are not the same addition

[Yakov Pechersky]

Yes, I'm being a little narrow/imprecise with my definition of 'separate'