refactoring WithTop/WithBot as inductive types

Stream: mathlib4

[Kim Morrison]

We have long wanted to refactor WithTop and WithBot as one-field structures inductive types, rather than having them be synonyms for Option.

We've delayed doing this because today we rely on these being defeq in many places, in order to set up the order duals of various theories.

There is a plan to stop relying on this defeq (cf @Jovan Gerbscheid's new to_dual tactic), but there is not obstacle to getting started already, by making WithBot a one-field structure inductive type, and then defining WithTop as a synonym. This lets us get (more than?) half the work done now, and later we can break the defeq between the two.

I've started this in #27918. The files I've modified so far are working, but there are more to go.

If anyone would like to help (or take over!) getting this done, that would be amazing. (We are keen to get started on some new tactic work that will be easier if this refactor is settled sooner rather than later.)

[Eric Wieser]

One field structures or a custom inductive type?

[Eric Wieser]

The PR seems to do the latter

[Kim Morrison]

Yes. An inductive is the right solution here, right?

[Eric Wieser]

A one-field structure gives us more defeqs with option like (x.map f).toOption = x.toOption.map f

[Eric Wieser]

But making match about as annoying as it currently is

[Eric Wieser]

I'd argue that annoyance is a lean bug though (edit: lean4#9712):

-- status quo
def MyOption := Option Nat

@[match_pattern]
def MyOption.some : Nat → MyOption := Option.some

@[match_pattern]
def MyOption.null : MyOption := Option.none

def foo : MyOption → Nat
  | .some n => n
  | .null => 0

theorem wat : foo (.some 1) = 2 := by
  rw [foo] -- fails, equation lemma is wrong

-- one field structure
structure MyOptionStruct where
  toOption : Option Nat

@[match_pattern]
def MyOptionStruct.some : Nat → MyOptionStruct := fun n => ⟨.some n⟩

@[match_pattern]
def MyOptionStruct.null : MyOptionStruct := ⟨Option.none⟩

def foo : MyOptionStruct → Nat
  | .some n => n
  | .null => 0

theorem wat : foo (.some 1) = 2 := by
  rw [foo] -- fails

[Matthew Ballard]

Sébastien Gouëzel said:

Interesting (and surprising to me) comment of Sebastian Ullrich on the issue:

I believe this amounts to a misuse of def which is hard/unlikely to be addressed across the entire elaborator. Because of its context-dependent reducibility, the main difference of def to abbrev is performance-related, it should not be used to create semantically distinct types. Actually irreducible declarations like structure should be the preferred way for doing so.

I read this as a "won't fix", if I understand correctly.

I read this as directing us to Eric's approach.

Given this, some removal of current friction for this approach would be much appreciated.

[Eric Wieser]

I don't think there's much prior conversation right now as to whether one-field structures or custom inductives are better

[Matthew Ballard]

Is there an advantage to custom inductives?

[Eric Wieser]

Avoiding lean4#9712, and supporting obtain

[Jovan Gerbscheid]

I thought that the point was to move away from abusing Option related defeqs. So I'm in favour of the custom inductive approach.

[Eric Wieser]

I think defeq abuse here refers to type equalities like Option = WithTop or things that rely on them like Option.some x = WithTop.some x, not things like (x.map f).toOption = x.toOption.map f which we can still have with a one-field structure.

[Matthew Ballard]

I generally worry about the convenience (for all parties) of one custom inductive per instance but would be happy to be disabused.

[Yaël Dillies]

My (now old) PR #19668 feels relevant to this discussion

[Yaël Dillies]

cc @Anne Baanen since you were assigned to it

[Kim Morrison]

Any further comments here? If I push this through we will merge?

[Yaël Dillies]

Can we refactor them as one-field structures around Option first? This will already show where all issues are

[Kim Morrison]

Why? Don't we get better match statements with an inductive?

[Yaël Dillies]

I guess so

[Yaël Dillies]

Secretly my hope is that you first refactor WithTop and WithBot in such a way that they are defeq, as I know this will remove a lot of bad defeqs but still keep the good "dualising" defeq between (WithTop α)ᵒᵈ and WithBot αᵒᵈ. Without that defeq, you will really suffer, at least until the advent of to_dual

[Ruben Van de Velde]

That's what Kim is doing in #27918 right?

[Yaël Dillies]

Oh! I had completely missed that

[Matthew Ballard]

What API are we going to duplicate from the model type to provide? If that type has a large API surface, there is going to be tension in all directions - duplicate code, missing capabilities, etc.

Option might be small enough but I don’t know.

A version of deriving that clones API from a template type would be helpful and probably by the best approach.

[Eric Wieser]

Kim Morrison said:

Why? Don't we get better match statements with an inductive?

Sure, but we also get better match statements if we fix lean4#9712 (without which match_pattern isn't very useful)

[Eric Wieser]

What we get with the structure is nice defeqs around toOption/fromOption

[Matthew Ballard]

I guess [OptionLike T] is theoretically an option (heh) for consistent API but I’d worry the overhead would eat all the benefit

[Eric Wieser]

That gives us no match and no defeqs, so seems worse than all options suggested so far

[Matthew Ballard]

Sure but custom inductives come with no built in API

[Matthew Ballard]

Note: I’m just thinking out loud and not locked in on any option

[Matthew Ballard]

What why doesn’t that give a match?

[Eric Wieser]

You can only use match_pattern on things that reduce to constructors

[Matthew Ballard]

I wasn’t thinking about pulling back via an embedding/equivalence necessarily.

[Jovan Gerbscheid]

Eric Wieser said:

You can only use match_pattern on things that reduce to constructors

Why can't we have fully custom match patterns, the way we can with cases and induction?

[Eric Wieser]

That sounds like a much bigger ask than lean4#9712!

[Robin Arnez]

Jovan Gerbscheid schrieb:

Why can't we have fully custom match patterns

Well you want to make sure that you're still able to match on constructors and since you usually have these, there isn't really much room to put in custom eliminators... Also match heavily relies on being able to reduce everything fully which would definitely cause problems for custom eliminators.

[Kim Morrison]

I'd like to make progress here that doesn't depend on language features, or bug fixes that don't have an assigned owner.

It looks like we're going to postpone slightly the new machinery which had motivated me to clean this up, but hopefully it gets done by the time I actually need it. :-)

[Kim Morrison]

I have resumed work on this. I would love assistance if anyone is interested.

[Kim Morrison]

I have run into an annoying issue on the PR at #27918, where WithOne (and hence WithZero) are defined as Option. However later in their development, particularly Mathlib.Algebra.Order.GroupWithZero.Canonical, we abuse the defeq with WithBot.

Any suggestions here? I think we probably should just redefine WithOne as WithBot for now, and that seems like the more painful defeq to break at the moment (i.e. lose the defeq with Option instead). This will require adding an import, but I think that's okay.

If anyone would like to look at this file, please do checkout the branch! I'm happy to give write access, or merge changes into this branch. This is high priority again for me.

[Ruben Van de Velde]

Ah yeah, I think I recall being somewhat negatively surprised at that at some point, though I don't recall what I was doing. I might be able to find a bit of time to look at it

[Floris van Doorn]

Does this refactor mean that we will need to duplicate (a fraction of) the API for Option to the type synonyms (e.g. the 27 equivalences involving Option?).
That is probably just a cost we'll have to pay...

[Jovan Gerbscheid]

I don't think it makes sense to have many of these, other than an Option α ≃ WithBot α. It would seem more sensible to instead have some OrderIso when applicable.

[Ruben Van de Velde]

I've got some changes building; will see how for I get

[Ruben Van de Velde]

@Kim Morrison see #28957; I didn't make a pr to your fork because I started from a newer master

[Kim Morrison]

@Ruben Van de Velde, what shall we do with the old WithOne.map? Rename it to WithOne.mapMulHom?

[Kim Morrison]

(Why the double prime on your new version? I can't find any collision with a single primed version.)

[Kim Morrison]

@Ruben Van de Velde, I pushed a commit back to your PR doing the renames.

[Ruben Van de Velde]

@Kim Morrison thanks! WithZero.map' exists, but WithOne.map' doesn't

[Ruben Van de Velde]

@Kim Morrison Yaël is wondering about the mapD name to replace Option.elim in #30119; would you mind responding after you've cut the release?

[Jovan Gerbscheid]

I think mapD would have made sense if we had map? and map!. But map? is just called map, so I don't think mapD fits the pattern.

[Kim Morrison]

@Yaël Dillies, now that your #19668 has landed, might I interested you in fixing up Mathlib/Algebra/Order/GroupWithZero/Canonical.lean on #27918 (the WithBot_refactor branch)?

[Yaël Dillies]

Sure! although I would rather wait a few days for #30848 to be merged (which is also fitting in that I am mostly unavailable this coming week).