!4#3360 new ext lemma generation

Stream: mathlib4

[Jon Eugster]

In !4#3360 we have

@[ext]
structure NonemptyInterval (α : Type _) [LE α] extends α × α where
  fst_le_snd : fst ≤ snd

The generated ext-lemma looks like

NonemptyInterval.ext {α : Type _} [LE α] (x y : NonemptyInterval α)
  (fst : x.toProd.fst = y.toProd.fst) (snd : x.toProd.snd = y.toProd.snd) : x = y

while translating the mathlib3 version one-to-one, it would be

NonemptyInterval.ext {α : Type _} [LE α] (x y : NonemptyInterval α)
  (h : x.toProd = y.toProd) : x = y

and there was another Lemma Prod.ext so that using the tactic ext it would chain the two and using ext1 it would only do one step.

This change seems to come from the use of getStructureFieldsFlattened instead of getStructureFields in WithExtHyps. Is this the desired way ext works now? It seems to me that ext1 becomes a bit less useful that way.

[Eric Wieser]

I think this behavior is an effort to make the generated ext lemma not depend on the order of the base classes

[Eric Wieser]

That is, it emulates what ext would do to old-style structures in Lean 3

[Eric Wieser]

Unfortunately, docs#nonempty_interval was a new-style structure, so this is a behavior change,

[Eric Wieser]

A reasonable compromise would be to have @[ext (flat := ff)] to recover the old new-style structure behavior

[Jon Eugster]

I see, thanks for the explanation!

[Jon Eugster]

Eric Wieser said:

A reasonable compromise would be to have @[ext (flat := ff)] to recover the old new-style structure behavior

@Eric Wieser do you think std4#122 would be reasonable? It introduces an option tactic.ext.flatten that toggles this behaviour, with
default being the current state (i.e. flatten structures)

[Mario Carneiro]

I think a bit of syntax on the attribute makes more sense than an option. I don't like options that change the semantics of tactics / commands (as opposed to just turning off generation of things or affecting presentation)

[Mario Carneiro]

Also I would prefer for lean 4 docs not to talk about "old-style structures" in favor of things like "fields are flattened"

[Jon Eugster]

Thanks for the comment, that makes sense. I'll change both of it quickly :+1: