ext is weaker

Stream: std4

[Scott Morrison]

Because we index lemmas in ext differently in Lean 4, we have the following regression:

-- Works in Lean 3
import tactic.ext

@[ext]
structure A :=
(n : nat)

def B := A

example (x y : B) (w : x.n = y.n) : x = y := begin
  ext,
  exact w,
end

-- Doesn't work in Lean 4
import Std.Tactic.Ext

@[ext]
structure A where
  n : Nat

def B := A

example (x y : B) (w : x.n = y.n) : x = y := by
  ext     -- Does nothing
  exact w

[Scott Morrison]

Now, maybe this is an antipattern, but it is widely used in mathlib. We can add the extra ext lemmas for the synonyms, but if it's okay to just make ext more powerful I'd prefer that.

[Mario Carneiro]

This is expected behavior. It came up when we did the backport removal of the @[ext foo] attribute

[Mario Carneiro]

Typeclass search also doesn't unfold regular definitions, and this is useful behavior

[Mario Carneiro]

I don't think we should unfold definitions here and just require you to annotate the definition with @[ext] if you want to inherit the extensionality lemma

[Scott Morrison]

Okay. The common example of this is going to be defining the hom field of a category, where it's not just annotating a definition, but I think probably requires stating a new lemma.

[Scott Morrison]

At least in mathlib3 ext is still seeing through such cases.

[Junyan Xu]

At least in mathlib3 ext is still seeing through such cases.

An example where this causes problems: after changing irreducible to semireducible we need to change an ext to avoid an infinite loop.