Fetching all types with instances

Stream: metaprogramming / tactics

[Yakov Pechersky]

In #5664, we have a faster nat.bin_cast that can be used instead of nat.cast. However, they are provably equal only if the α : Type* is an add_monoid (where the has_zero and has_one make sense). Currently, there are such types -- fin n is not instanced as an add_monoid (although #5010 should help with that). I want to find out if there are other types where we have has_zero, has_one, and has_add, but are _not_ add_monoid.

[Yakov Pechersky]

What would be the best meta way of fetching these? How does one "import all"? Then I could try to write meta code that fetches types that satisfy any of the four classes, and find the intersection that I am interested in.

[Kevin Buzzard]

If you're trying to add things in fin n, you're doing it wrong, aren't you? If you're adding you should be using zmod n. I am slightly surprised there is an addition defined on fin n. This might be a historical artefact?

[Yakov Pechersky]

You can't use bit0 and bit1 without +

[Yakov Pechersky]

So as much as you want to avoid + on fin n, you need it to get nice 5 : fin 7.

[Kevin Buzzard]

fin n is supposed to be a canonical model of an abstract totally ordered set of size n. I don't want bit0 on it either!

[Yakov Pechersky]

As you can see in the PR, I do not provide monoid even though it is provable. I do give (*) simp lemmas though because even though one shouldn't multiply in fin n, if you somehow get stuck in that situation, then something would be able to help.

[Kevin Buzzard]

You also get rather un-nice 12 : fin 7 and this is what I'm objecting to.

[Kevin Buzzard]

If you want to treat these things as numbers you should be using zmod 7

[Kevin Buzzard]

That's my personal mental model of fin n, at any rate.

[Kevin Buzzard]

The elements of fin 7 aren't $\{0,1,2,\ldots,6\}$, they're $\{a_0,a_1,\ldots,a_6\}$

[Yakov Pechersky]

How do you distinguish fin.succ from fin.cast_succ then?

[Yakov Pechersky]

By referring to the total order, and saying "new bot" or "new top"?

[Yakov Pechersky]

How would one phrase, "the minor after removing the 3rd row and 4th column" if not making reference to 2 and 3? Perhaps it'd be better if they were enumerated starting from 1 like ordinals?

[Yakov Pechersky]

If we wanted to talk about S_n, one could imagine notation like (0 1 2 3) or (1 2 3 4) whichever you prefer. And while mathematically, the addition isn't relevant, it is what makes the notation work for how Lean numerals are, as far as I understand.

[Yakov Pechersky]

I hope it doesn't seem like I'm being difficult -- I'm truly trying to understand the limitations of formalization.

[Yakov Pechersky]

While it is unfortunate that 12 : fin 7 is possible, is that different than (6 : ℚ) / 4 being equal to (3 : ℚ) / 2? As soon as we start having some sort of numerical notation for things that aren't exactly nat, we'll run into the issue of noncanonical representations.

[Kevin Buzzard]

No, I'm just presenting some other point of view. We could have a map zmod n -> fin n. This is what my mental model is, I'm not saying it's what we have to do! I think it is deeply unfortunate that 12 : fin 7 works, because nobody can guess what that means.

[Kevin Buzzard]

It's all about junk values I guess.

[Yakov Pechersky]

Similar to your favorite 1 / 0 example.

[Yakov Pechersky]

Well I hope determining the meta way of identifying such non-add_monoid types will help understand if there are any other places where there are numerals but they don't behave exactly right.

[Alex J. Best]

I always thought addition / succ fin n should be endpoint absorbing, like (n - 1 : fin n) + 1 = n - 1, that seems quite handy in some contexts where you are indexing things, succ / add would be more of an "advance as far as possible" operation. People can always use zmod if they want a cyclic group, but thats quite a radical change :grinning:

[Yakov Pechersky]

That makes sense too, and then you have a subtraction which is dual.

[Yakov Pechersky]

But right now succ is defined as the embedding into the successor type, not within the type.

[Yakov Pechersky]

While + 1 is within the type.

[Yakov Pechersky]

I'd be totally cool with that redefinition -- probably a large undertaking though!

[Yakov Pechersky]

(Even if addition was defined in that way, 12 : fin 7 would still have a meaning, it would just be different than before.)

[Kevin Buzzard]

My impression is that there is some huge mess with cast and cast_succ right now. I would set it up in the following way. In the theory of simplicial sets there are maps from fin n to fin (n +1) called "skip t" and maps from fin (n + 1) to fin n called "collapse t and t+1". The combinatorics of the way these maps interact is very well-understood and these are the maps which should be used everywhere, plus some nice simp lemmas to deal with them.

[Kevin Buzzard]

https://en.wikipedia.org/wiki/Simplicial_set#Face_and_degeneracy_maps

[Kevin Buzzard]

The sigmas and the deltas are the maps you want, the lemmas are all there. @Reid Barton or @Johan Commelin did you ever make these maps in Lean?

[Johan Commelin]

yup

[Johan Commelin]

there is a branch sset that has this stuff

[Kevin Buzzard]

Stuff like "the minor after removing the 3rd row and 4th column" is probably not something you never actually say. You might have i : fin n and j : fin m and then you can remove the i'th row and the j'th column, this is fine. I am just explicitly suggesting that using numerals to talk about fin n should not be necessary. But of course my use cases for fin n might be very different from yours.

[Yakov Pechersky]

You're right that one might not need to use numerals for fin n. But they are defined at the moment, and without the PR I cited above, they are not add_monoid. However, they do have 0, 1, and + which allows them to be notated by numerals. Currently, one cannot prove that nat.cast and nat.bin_cast will give the same fin n.

I'm asking, what's the meta way to find the _other_ types where this lack of correspondence appears? Those might be other types that you could say shouldn't even have numerals work for them, but they do currently.

[Kevin Buzzard]

yeah, sorry, I should let you get back to the point :-)

[Eric Wieser]

Answering Kevin's earlier question, the skip and collapse maps are docs#fin.succ_above and docs#fin.pred_above I think

[Yakov Pechersky]

That's not exactly right about fin.pred_above