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