bug in `@[ext]` with `extends`

Stream: std4

[Jireh Loreaux]

The behavior of the @[ext] attribute on structures with extends clauses seems suboptimal to me, and doesn't match what happens when the extends fields are inlined. Below, I would expect both occurrences to generate Prod''.ext. That way, when this ext lemma is called, we can stop at an earlier step with ext1. Right now, for extends fields, it seems that @[ext] calls the ext lemmas on the structures being extended.

import Mathlib.Tactic.Basic

@[ext]
structure Prod' (α β : Type _) extends Prod α β

@[ext]
structure Prod'' (α β : Type _) where
  toProd := Prod α β

#check Prod'.ext
/-
Prod'.ext.{u_1, u_2} {α : Type u_1} {β : Type u_2} (x y : Prod' α β)
    (fst : x.toProd.fst = y.toProd.fst)
    (snd : x.toProd.snd = y.toProd.snd) : x = y
-/

#check Prod''.ext
/-
Prod''.ext.{u_1, u_2} {α : Type u_1} {β : Type u_2} (x y : Prod'' α β)
    (toProd : x.toProd = y.toProd) : x = y
-/

[Jireh Loreaux]

@Mario Carneiro :up:. I guess ext is in Std now. You can move it to that stream of it you want.

[Notification Bot]

This topic was moved here from #mathlib4 > bug in @[ext] with extends by Mario Carneiro.

[Mario Carneiro]

Lol, this has literally gone back and forth between these two behaviors already. There is a flag @[ext (flat := false)] to control it

[Jireh Loreaux]

Hah! I was just looking at that flag and thought it might exist for this purpose. I can just use that flag. Where is the prior discussion about this behavior?

[Mario Carneiro]

https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/!4.233360.20new.20ext.20lemma.20generation/near/351102875