ext for DFinsupp.ext

Stream: mathlib4

[Antoine Chambert-Loir]

docs#DFinsupp.ext has no [ext]attribute while docs3#dfinsupp.ext has one.
Is there any reason for this?

[Ruben Van de Velde]

@[ext]
theorem ext {f g : Π₀ i, β i} (h : ∀ i, f i = g i) : f = g :=
  FunLike.ext _ _ h
#align dfinsupp.ext DFinsupp.ext

Looks like it's just not rendered in the docs

[Antoine Chambert-Loir]

But what surprises me is that on my current setup, apply DFinsupp.ext works, while ext doesn't
(and worked in the Lean3 version of the file I am presently porting…)

[Yury G. Kudryashov]

Do you have a #mwe ?

[Adam Topaz]

This is probably due to a change in the way the ext tactic works between lean3 and 4. In lean3, it was much more aggressive, essentially trying all possible ext lemmas as a failsafe, while the lean4 version doesn't do this.

[Yury G. Kudryashov]

Do LHS and RHS have type DFinsupp or some T where def T := DFinsupp?

[Adam Topaz]

In such situations in lean4, it usually means that some API is missing.

[Kevin Buzzard]

Well that's one interpretation; another is that ext! is missing.

[Antoine Chambert-Loir]

Here is a MWE :

import Mathlib.Algebra.Module.LinearMap
import Mathlib.RingTheory.GradedAlgebra.HomogeneousIdeal

variable {ι : Type _} [DecidableEq ι]


theorem DirectSum.mk_apply {β : ι → Type _} [∀ i, AddCommMonoid (β i)] (s : Finset ι)
    (f : ∀ i : s, β ↑i) (i : ι) :
    DirectSum.mk β s f i = if h : i ∈ s then f ⟨i, h⟩ else 0 :=
  rfl


theorem DirectSum.mk_eq_sum' {β : ι → Type _}
    [∀ i, AddCommMonoid (β i)]
    [∀ (i : ι) (x : β i), Decidable (x ≠ 0)] (s : Finset ι) (f : ∀ i, β i) :
    (DirectSum.mk β s (fun i => f i)) =
      s.sum (fun i => DirectSum.of β i (f i)) := by
  simp only [Finset.coe_sort_coe]
  -- ext does not work
  apply DFinsupp.ext
  intro i
  rw [DirectSum.mk_apply, DFinsupp.finset_sum_apply]
  split_ifs with hi
  · rw [Finset.sum_eq_single_of_mem i hi]
    · rw [← DirectSum.lof_eq_of ℕ, DirectSum.lof_apply]
    · intro j _ hij
      exact DirectSum.of_eq_of_ne _ _ _ _ hij
  · apply symm
    apply Finset.sum_eq_zero
    intro j hj
    exact DirectSum.of_eq_of_ne _ _ _ _ (ne_of_mem_of_not_mem hj hi)

[Eric Wieser]

Yury G. Kudryashov said:

Do LHS and RHS have type DFinsupp or some T where def T := DFinsupp?

So the answer to this is "Yes, with T = DirectSum"

[Eric Wieser]

I don't really like the idea of duplicating all the dfinsupp API for direct_sum, but duplicating ext seems fairly standard (we already do it for all the FunLike types)

[Antoine Chambert-Loir]

Yury G. Kudryashov said:

Do LHS and RHS have type DFinsupp or some T where def T := DFinsupp?

both live in ⨁ (i : ι), β i

[Antoine Chambert-Loir]

Eric Wieser said:

I don't really like the idea of duplicating all the dfinsupp API for direct_sum, but duplicating ext seems fairly standard (we already do it for all the FunLike types)

Do you mean I'm erring here?
(I don't like the idea of duplicating stuff, especially if I have to do it. IIRC, I had to write this in order to provide quotient of graded modules by homogeneous submodules with a grading.)

[Eric Wieser]

(⨁ i, β i is docs#DirectSum, Π₀ i, β i is docs#DFinsupp)

[Eric Wieser]

I think you only need to duplicate the ext lemma (and I think it is fine to do so)

[Yury G. Kudryashov]

The problem is that ext and some other tactics in Lean 4 (like simp) match lemmas based on types of terms. So, it is possible that some simp lemma about DFinsupp will not apply because you have (f : DirectSum _) instead of f : DFinsupp _.

[Yury G. Kudryashov]

BTW, are there any instances on DirectSum that don't agree with DFinsupp? If no, then should we make DirectSum reducible?

[Eric Wieser]

Yes, only direct_sum has the convolutive multiplication (it is to DFinsupp as AddMonoidAlgebra is to Finsupp)

[Eric Wieser]

In principle dfinsupp should have pointwise multiplication to match finsupp, though I don't think we ever added it

[Scott Morrison]

Kevin Buzzard said:

Well that's one interpretation; another is that ext! is missing.

How about someone implements ext! so that is applies all @[ext] lemmas, regardless of whether the DiscrTree approves, but then prints a message like "XYZ.ext applies here. If you would like to be able to use this with ext, please make a copy of this lemma written in terms of the type PQR."

[Eric Wieser]

Should it be ext!?, to fit the pattern of "tactics ending in ? shouldn't be committed"?

[Jon Eugster]

Added an implementation of ext!? to std4#120 where I also implemented ext? a while ago.
Screenshot_20230724_033331.png