semi/irreducible attributes

Stream: mathlib4

[Johan Commelin]

#18164 tracks occurences of attribute [semireducible] and attribute [irreducible] as discussed yesterday in the porting meeting.

[Johan Commelin]

#18165 contains the script that generated the list

[Sebastien Gouezel]

Since I have important boring things to do, I started on this instead, in the branch branch#SG_no_irreducible. Anyone can contribute there, of course.

A question: with_one α is currently defined as a type copy of option α, which is made irreducible after the fact. Is it more Lean 4/port compatible to convert it to a single field structure?

[Eric Wieser]

What goes wrong if we drop the irreducible attributes without replacement?

[Sebastien Gouezel]

In fact with_one α is already ported, and the irreducible attribute is indeed just dropped. Is it going to create a mess where API of option leaks everywhere? Just for the record, here is one definition in the file:

def unone {x : with_one α} (hx : x ≠ 1) : α := with_bot.unbot x hx

Yes, it's abusing defeqs in every possible way (including the fact that with_bot α is yet another copy of option α).

[Sebastien Gouezel]

And the current Mathlib4 proof is the same:

def unone {x : WithOne α} (hx : x ≠ 1) : α :=
  WithBot.unbot x hx

[Yaël Dillies]

Also they should really be called .get, shouldn't they?

[Eric Wieser]

Those are only leaks if someone unfolds unone

[Eric Wieser]

Arguably we could solve that by wrapping all such defs in a do_not_unfold_me alias for id I guess a withOne.ofWithBot alias for id is probably a better solution there

[Eric Wieser]

For the lemmas it doesn't matter as long as the statements don't leak

[Kevin Buzzard]

I was involved with writing the Lean 3 API for some of the with_ stuff and I remember leaks being a real problem, but I might have been writing crappy code. I don't know whether we should (a) just press on (b) change the definition in Lean 4 or (c) change the definition in Lean 3 first.

There's a chance that the irreducible attribute is dropped in mathlib4 because the porting program was just silently ignoring attribute [irreducible] foo lines.

[Eric Wieser]

I don't think the porting program silently ignores many things, usually it generates comments that humans then ignore

[Kevin Buzzard]

I think that in the attribute [irreducible] case it was in the past silently ignoring this (that was my understanding of what Mario told me, but I might have misunderstood)

[Sebastien Gouezel]

#18168 removes a few of them. Only easy cases: move the attribute to the definition, and unfold the definition when needed in proofs.