Equiv

Stream: std4

[James Gallicchio]

Is Equiv a reasonable Std addition? I'm working on incorporating SciLean's Enumtype and having Equiv would make it a good deal cleaner. Seems highly useful in programming contexts.

[Eric Wieser]

Would docs#FunLike and docs#EquivLike move with it?

[Eric Wieser]

And docs#Function.Embedding ?

[François G. Dorais]

I think Equiv would be good in Std. It's useful to transport structure and I also use it a lot to manipulate encodings (I guess that's what Enumtype is about).

FunLike and EquivLike are interesting abstractions but I don't see the necessity to move these at the same time. I thinkFunction.Embedding doesn't need to move at all and the main connection with Equiv is noncomputable.

[Eric Wieser]

If we don't move FunLike, then now std and mathlib have different ways to write function application, and simp lemmas are going to be a mess

[Eric Wieser]

François G. Dorais said:

I thinkFunction.Embedding doesn't need to move at all and the main connection with Equiv is noncomputable.

The main connection in my mind is docs#Equiv.toEmbedding, which is definitely computable...

[François G. Dorais]

I don't think it's necessary for Equiv to have function application API in Std, that can stay in Mathlib. That's not the kind of thing that's useful for programming.

[Scott Morrison]

I think the problem here is that every e.toFun x is "the wrong way to write it" according to Mathlib. Without moving FunLike, you can't talk about e.toFun x and still have these lemma ergonomic in Mathlib. Hopefully I'm wrong here....?

[François G. Dorais]

I think I understand the issue. It sounds like something that would need a surgical division.

[Eric Wieser]

Scott's summary is exactly the point I was trying to make

[Eric Wieser]

Two reasonable options in my mind are:

• Move FunLike too. This means you also need Function.Injective to move, which I can see being undesirable
• Create a PreFunlike in Std which provide PreFunLike.coe (and no injectivity field), and then have FunLike in mathlib extend it. All the mathlib lemmas would still be about PreFunLike.coe, so the issue Scott describes wouldn't occur (or call it FunLike and FaithfulFunLike)

[Eric Wieser]

In essence, the purpose of PreFunLike is just to restore the Lean3 coeFn behavior where all function coercions used the same head symbol...

[François G. Dorais]

After taking a look at Mathlib's Equiv API and comparing with my own version, I see that they are wildly different and incompatible in many ways. I think it even makes sense to have two Equiv types with a bridge to connect the two when necessary!

To see the incompatibility from the other point of view: for my main application of Equiv, the forward function is actually implemented by an Array and having a coercion to function would be very annoying! The important feature of Equiv for me is composability, the forward and reverse functions are "implementation details".

[Eric Wieser]

It's probably also worth noting that Enumtype already exists in some form in mathlib as docs#FinEnum

[Eric Wieser]

Perhaps we should refactor it there in mathlib first before attempting to move it to Std4

[François G. Dorais]

Maybe it's easier to approach the issue differently. It's not about moving Equiv from Mathlib to Std, it's that both Mathlib and Std have some need for an Equiv type. The two types may as well be the same for binary compatibility. However, there is no need for the two API to be the same. That is not sustainable. We can't think of Std as "the part of Mathlib that's not math".

I think it makes sense to proceed this way:

1. Move the Equiv type (only) to Std.
2. Develop a Std.Equiv API, probably borrowing lots of code from Mathlib but with no aim for compatibility. In particular no ≃, ↪, ↑.
3. Reimplement some parts of the Mathlib Equiv API using Std.Equiv to avoid code duplication while maintaining Mathlib's API as-is.

That does mean that some things will have different names in Std and Mathlib but that's bound to happen anyway.

[Eric Wieser]

I don't see why we wouldn't make the API the same given we have the option to

[Eric Wieser]

If Std and mathlib disagree on how to write function application that's a pretty major disagreement. And if your Equiv doesn't use function application then I'm not sure how it's used at all...

[François G. Dorais]

@Eric Wieser It's not a disagreement about how to write function application: there simply is no need for the coercion to function in Std, it's not a useful feature.

[Eric Wieser]

Well that's a disagreement about whether to write e.toFun x or e x

[François G. Dorais]

The equivs are composed to construct more complex equivs without fussing about implementation details.

[Eric Wieser]

Are you saying toFun is not part of the API at all?

[François G. Dorais]

It is, but it's an implementation detail.

[François G. Dorais]

For me, the equiv is a way not to worry about the functions.

[Eric Wieser]

What _is_ in the API then?

[François G. Dorais]

Groupoid laws.

[François G. Dorais]

And transport defs.

[Eric Wieser]

Do you envisage having APi that says List X is equivalent to List Y when X is equivalent to Y? If so, would Std contain the lemma about how that acts on nil / cons?

[François G. Dorais]

I have that equivalence in my API, I never needed to know it preserves operations. That would be an isomorphism, not just an equivalence.

[Eric Wieser]

I think I'm missing the application here. If all you ever do with equivs is construct more equivs with them, what's the computational application that justifies them being data?

[François G. Dorais]

Here's an example where Equiv comes in extremely handy. Some of my students are doing research on finite automata. The more efficient implementations of transitions and reachability algorithms use Boolean matrix multiplication. These matrix algorithms are implemented using arrays, but the machine states are typically more complex, with data about how the machine was constructed or the purpose of each state. To connect these two, I need an Equiv from my machine's state type to Fin n (say). How that Equiv works is irrelevant. There's a transport function that uses that Equiv so I can use matrix multiplication for calculation. The correctness proofs do have to fiddle with the forward and reverse functions but they only need to know that they are inverses of each other, so the Equiv is really a black box.

[James Gallicchio]

hm, this spawned a lot of conversation...

I'm not opposed to refactoring FinEnum; I think it was probably designed before any programming usage was intended. But if FinEnum uses Equiv, I'd still want to move Equiv into Std.

We've discussed moving FunLike before. But I am guessing we'd want to refactor out the injectivity field as Eric said.

[Eric Wieser]

I think a lot of my confusion would be resolved by seeing actual code written against the current docs#Equiv that demonstrates a practical situation where application is irrelevant. It sounds like @François G. Dorais's Equiv would have a strict subset of the API it has in mathlib4, so that demo could be built without first extracting to Std4.

[Eric Wieser]

FinEnum as it currently exists in mathlib is probably ok computationally for the typeclass, but all the instances are awful as they go back and forth via lists. A complete redesign along the lines of Enumtype certainly seems like a reasonable choice.

[James Gallicchio]

Eric Wieser said:

seeing actual code written against the current docs#Equiv that demonstrates a practical situation where application is irrelevant.

It's never irrelevant -- but in my application, it didn't matter whether I wrote e x or e.toFun x because I wasn't proving anything and therefore didn't need any simp lemmas. But that's a bad excuse for not moving it to Std :-)

[James Gallicchio]

I'll start working on a refactor of FinEnum.

[François G. Dorais]

That's right, it's not irrelevant but it's a black box and doesn't need special treatment. That said, I much prefer writing e.toFun x than e x since it's hard to see invisible things :-)

[James Gallicchio]

(you can see the equivalence e, so it doesn't feel quite as invisible as coercions usually are...)

[James Gallicchio]

BTW, what's the reason for FunLike to have the injectivity constraint? Is it acting as a safeguard against FunLike instances that are antipatterns?

[Eric Wieser]

It's to allow ext (and a handful of similar lemmas) to be generalized

[Eric Wieser]

So you can write FunLike.ext and it works for Embedding, Equiv, AddHom, etc

[Eric Wieser]

I think Std4 could probably justify dropping the injectivity bit if movingFunction.Injective is undesirable (but maybe it's not?)

[James Gallicchio]

It seems useful in Std4, but I can imagine situations coming up where people want the notation without proving injectivity. Would it be reasonable to refactor in Mathlib the injectivity as another class? (LawfulFunLike? FunLike.Inj?)

[Eric Wieser]

I think the current name is best kept as the injective version

[François G. Dorais]

I think it's fine to have a plain ToFun class in Std that can act as a grandparent to all of these. I can also get used to the coercion if that's what everybody wants.

[James Gallicchio]

To save on name bikeshedding, maybe we should just not prematurely refactor; once someone has a FunLike that's not trivially injective we can come back to it :joy:

[François G. Dorais]

(I was using ToFun as a description, not a suggestion. I'm actually surprised to see that it doesn't already exist somewhere.)

[Eric Wieser]

Well, the builtin is docs#CoeFun but that has elaboration magic that we don't want

[François G. Dorais]

@Eric Wieser I love that magic but I hate it sometimes. I often have to make silly aliases to make things work. How often do you run into this and how?

[Eric Wieser]

How often do I run into magic that we don't want with CoeFun, you mean?

[Eric Wieser]

If we used the default CoeFun then algebraMap R A r would be (algebraMap R A).toAddMonoidHom.toAddHom.toFun r or something, which is then syntactically different from (algebraMap R A).toMonoidHom.toMulHom.toFun r, and now we have a whole tree of different paths to rewrite between when we don't care about any of them.

[François G. Dorais]

Things that don't hook right? Other things that can only be fixed by first rewriting into something with no magic...

(This is re the first part only.)

[Eric Wieser]

I'm afraid I'm not sure which message you're referring to (and I think there's a typo that's not helping)

[François G. Dorais]

Lag confusion... "the first part" was an answer to the sentence that ends with "you mean?"

[Eric Wieser]

I assume "hook" means "look" (as opposed to "hook right (arrow)" aka docs#Embedding)

[François G. Dorais]

No, it means hook as in fishing. It's an analogy with getting the right bait for the fish. Sorry for using that analogy, I thought it was common.

[Mario Carneiro]

I think it would be reasonable to move Equiv to Std, along with a minimal FunLike port including Function.Injective. (injective, surjective, bijective were once part of lean 3 core, and most things in the lean 3 core library are candidates for std, even if they have since migrated out of the core library.) FinEnum / Enumtype is a different matter and should probably not be discussed in this topic

[Mario Carneiro]

We had to do something similar when porting Int/Rat lemmas, we had to move NatCast for consistency with mathlib even though it's just notation

[Mario Carneiro]

I think the main usage of Equiv is as a "vocabulary type", we want everyone talking about equivs to use the same type to do so

[Mario Carneiro]

It's also not horrible computationally, although it's not something you want to use unless you have to

[James Gallicchio]

I'm hoping we can get Lean to inline enough stuff to find idempotent e \circ e.symm applications and csimp them away, but that's a ways off :)

[Mario Carneiro]

that would be cool, but csimp definitely doesn't support it

[James Gallicchio]

ah, right, only constants. well. another thing to put on the pile of "useful if csimp supported non-constant rewrites"