Zulip Chat Archive

Stream: std4

Topic: ext is weaker


Scott Morrison (Nov 23 2022 at 15:40):

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 (Nov 23 2022 at 15:41):

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 (Nov 24 2022 at 04:02):

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

Mario Carneiro (Nov 24 2022 at 04:02):

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

Mario Carneiro (Nov 24 2022 at 04:03):

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 (Nov 24 2022 at 15:19):

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 (Nov 24 2022 at 15:20):

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

Junyan Xu (Nov 24 2022 at 15:51):

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.


Last updated: Dec 20 2023 at 11:08 UTC