What is and isn't in scope for `ext`?

Stream: general

[Eric Wieser]

I recently made some changes to ext that allow it to recurse into tensor products and products when equating linear maps. I'm wondering where to draw the line on what should and what shouldn't be an ext lemma.

For instance, this is almost certainly a badext lemma, as the user could just apply induction:

@[ext]
lemma function.nat_ext {β : Type*} {f g : ℕ → β}
  (h0 : f 0 = g 0)
  (h : ∀ n, f n = g n → f n.succ = g n.succ) : f = g :=
funext $ λ x, nat.rec h0 h x

What about when the bundled function allows one of the inductive cases to be eliminated? Is this a bad ext lemma?

import algebra.group.hom

@[ext]
lemma zero_hom.nat_ext {β : Type*} [has_zero β] {f g : zero_hom ℕ β}
  (h : ∀ n, f n = g n → f n.succ = g n.succ) : f = g :=
zero_hom.ext $ λ x, nat.rec (f.map_zero.trans g.map_zero.symm) h x

In the same line of ext lemma, we have docs#add_monoid_hom.ext_nat which is marked ext, and docs#ring_hom.ext_nat which is not.

[Eric Wieser]

The actual context of the question is whether this should be an ext lemma:

/-- Two linear maps agree if they agree on 1, `ι`, and agree on a product if they agree on its parts. -/
@[ext]
def exterior_algebra.hom_extₗ {N : Type*} [add_comm_monoid N] [semimodule R N] {f g : exterior_algebra R M →ₗ[R] N}
  (h_one : f 1 = g 1)
  (h_mul : ∀ x y, f x = g x → f y = g y → f (x * y) = g (x * y))
  (h_ι : f.comp (ι R M) = g.comp (ι R M)) : f = g :=

[Mario Carneiro]

I don't think ext lemmas should be recursive

[Mario Carneiro]

which would exclude all three examples

[Eric Wieser]

Do you object to linear_map.prod_ext (#6124) then too?

[Mario Carneiro]

bad link

[Eric Wieser]

Fixed

[Mario Carneiro]

no, that's fine

[Mario Carneiro]

recursive here meaning that there are equalities in the assumptions of a hypothesis to the theorem

[Mario Carneiro]

the theorem hypotheses should just be plain equalities or universally quantified equalities

[Eric Wieser]

That's a reasonable rule

[Eric Wieser]

Which means that presumably ring_hom.ext_nat should be marked ext

[Mario Carneiro]

There's also the matter of "canonicality" though; too many ext lemmas and it's not clear what's going to get applied when you use ext, since you don't specify which ext lemma to apply

[Mario Carneiro]

it is basically the same kind of situation as typeclass instances being "unique"

[Mario Carneiro]

ring_hom.ext_nat looks more like a subsingleton instance to me

[Eric Wieser]

Mario Carneiro said:

docs#RingHom.ext_nat looks more like a subsingleton instance to me

Reviving an old thread since I can't find whether we discussed this elsewhere; should ext try subsingleton elimination at every step? Or should we instead add ext lemmas with no hypotheses for the special cases where we actually expect a subsingleton?

#8168 explores this latter option by adding theorem ext_id (f g : R →ₐ[R] A) : f = g, and this cleans up some side goals downstream