Fin.Enum PR

Stream: batteries

[François G. Dorais]

I have a new WIP PR batteries#1007 for a replacement for Mathlib's FinEnum class. It's pretty big since there's a lot of machinery going on. It comes from my personal library, so it's not quite up to "standard form" yet. I'd like some feedback on how to bring it more "in line". I don't need much input on implementation details right now since I'm still tuning them.

This is needed because the Mathlib version is impractical. Instances rely on building a list of all elements of the type, which fits well with Fintype and Finset (which are both well designed) but is not practical for computation. The proposed alternative only builds a bijection between the type and Fin size, which can scale way beyond memory limitations.

[Violeta Hernández]

I don't really get what makes Fin.Enum distinct from FinEnum. Aren't both just data-carrying bijections between a type and some Fin n?

[François G. Dorais]

The types aren't very different (except that Equiv doesn't exist in Batteries). The instances are very different though. All the Mathlib instances require building an actual list of all elements of the type, which is prohibitive for Char and impossible for Char -> Bool. This implementation avoids that by just building the bijection and not the list.

[François G. Dorais]

In other words, all the hard work is in Fin.Coding not in Fin.Enum.

[François G. Dorais]

(Which reminds me I need to add an instance for Char...)

[Eric Wieser]

I like the new definition, but I think I'd prefer to see mathlib refactored to use it first, then upstream it later

[Eric Wieser]

In particular, having Equiv in mathlib feels like it makes a lot of constructions easier, especially with things like docs#finSumFinEquiv etc

[Mario Carneiro]

I think we should move Equiv to batteries actually

[Mario Carneiro]

It's a very simple and straightforward interface and it doesn't have poor computational behavior

[Eric Wieser]

But you can't pick the simp-normal form without having DFunlike too

[Eric Wieser]

Or at least, you'd end up with a different simp-normal form to mathlib

[Mario Carneiro]

I am okay with that

[Mario Carneiro]

I'm not sure it was a good idea to try to unify those across libraries in the first place

[Mario Carneiro]

somehow I suspect the call is going to be taken out of our hands anyway...

[Eric Wieser]

Mario Carneiro said:

I'm not sure it was a good idea to try to unify those across libraries in the first place

Perhaps, but if downstream libraries want to disagree with upstream ones, there ought to be a mechanism to unregister the simp lemmas

[Eric Wieser]

Otherwise it's easy to create loops

[Kim Morrison]

So far I haven't felt tempted to move Equiv up to Lean. :-) But I do encourage moving it to Batteries, particularly this PR seems be badly want it.

[Mario Carneiro]

Eric Wieser said:

Mario Carneiro said:

I'm not sure it was a good idea to try to unify those across libraries in the first place

Perhaps, but if downstream libraries want to disagree with upstream ones, there ought to be a mechanism to unregister the simp lemmas

that would indeed be nice

[François G. Dorais]

I'm not at all opposed to moving Equiv to Batteries and I am happy to refactor this PR after that's done.

[Eric Wieser]

Are you opposed to making the Enum refactor in mathlib first, so that we can leverage all the existing equivs there?

[Eric Wieser]

I think most of your Coding.lean file already exists scattered throughout mathlib

[François G. Dorais]

Can you find them all? I gave up after a few steps down the rabbit hole :-) I figured we could just alias or deprecate them when they are discovered.

[François G. Dorais]

It's also easier to maintain a coherent library of these standard codings.

[Eric Wieser]

I would hope that Loogle can find them fairly quickly

[François G. Dorais]

Didn't help me much but you are surely a better loogler than I am.

[François G. Dorais]

This is the kind of help I need!

[Eric Wieser]

@loogle Fin _ ⊕ Fin _ ≃ Fin _

[loogle]

:search: finSumFinEquiv, finSumFinEquiv_apply_left, and 4 more

[Eric Wieser]

(deleted)

[Eric Wieser]

@loogle |- _ ≃ Fin _

[loogle]

:search: finCongr, Fintype.equivFin, and 17 more

[Eric Wieser]

It's inconsistent whether the Fin is on the LHS or RHS

[François G. Dorais]

The Sum stuff is relevant but kind of trivial, we might as well alias those with Fin.Coding functions. Relying on Fintype and BigOperators is a no go. That's the rabbit hole!

[François G. Dorais]

Eric Wieser said:

Are you opposed to making the Enum refactor in mathlib first, so that we can leverage all the existing equivs there?

I am not opposed. I just don't think there is much to gain. Also, to a much lesser weight, I personally need it in Batteries sooner than later for at least two of my projects :-)

[François G. Dorais]

PS: The Fin.Enum name was chosen so that Mathlib could gently deprecate FinEnum. And also to allow future variations like Nat.Enum with a compatible API.

[Eric Wieser]

That's docs#Encodable I think

[François G. Dorais]

Yes, that's what I'm thinking about for Nat.Enum. We should keep that existing API in the back of our minds while thinking about the proposed API from this PR.

[Kyle Miller]

By the way, docs#Finite is essentially Prop version of Fin.Enum. It seems like once Fin.Enum exists it would be a reasonable next step to update that definition.

[Kyle Miller]

François G. Dorais said:

This is needed because the Mathlib version is impractical

I just want to mention that we know this too, and it's come up a few times in discussions — glad to see motion to get this done!

(I've also written my own Fin.Enum occasionally for projects, so looking forward to a well-developed one.)

[François G. Dorais]

Eric Wieser said:

Are you opposed to making the Enum refactor in mathlib first, so that we can leverage all the existing equivs there?

How about this process:

1. Merge the Batteries PR with Fin.Coding and Fin.Enum. Nothing there clashes with Mathlib.
2. Figure out how to harmonize Mathlib and Fin.Coding. (Leaving Fin.Enum alone, just updating Fin.Coding and Mathlib defs to match.)
3. Gently replace Mathlib's FinEnum with Batteries's Fin.Enum, reverting back to step 2 if that fails.

[Bhavik Mehta]

Flagging PR #15647 by @Tom Kranz which adds 86 lines to mathlib's FinEnum and makes a new 120-line long file with definitions and lemmas about it.

[François G. Dorais]

At a quick glance, this contribution focuses on implementing induction on cardinality for FinEnum. This is a fine and useful addition to Mathlib. However, the recursion principle has little computational value so there is little interest in having this in Batteries.

[James Gallicchio]

Can we also get a (proxy_equiv% based) deriving impl for Fin.Enum in this PR? I think that would make it a complete replacement for the version I have been using :P

[François G. Dorais]

@James Gallicchio Since proxy_equiv% is in Mathlib, the derive handler would have to be there. Though it could be upstreamed in the near future since there seems to be universal agreement for upstreaming Equiv to batteries.