Zulip Chat Archive

Stream: metaprogramming / tactics

Topic: Fetching all types with instances


view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:18):

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.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:19):

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.

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 16:21):

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?

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:22):

You can't use bit0 and bit1 without +

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:22):

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

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 16:23):

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!

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:24):

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.

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 16:24):

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

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 16:24):

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

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 16:25):

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

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 16:26):

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

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:27):

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

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:27):

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

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:29):

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?

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:31):

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.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:34):

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

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:37):

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.

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 16:40):

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.

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 16:41):

It's all about junk values I guess.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:42):

Similar to your favorite 1 / 0 example.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:43):

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.

view this post on Zulip Alex J. Best (Jan 14 2021 at 16:44):

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:

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:46):

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

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:46):

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

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:46):

While + 1 is within the type.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:48):

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

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 16:58):

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

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 17:26):

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.

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 17:28):

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

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 17:30):

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?

view this post on Zulip Johan Commelin (Jan 14 2021 at 17:32):

yup

view this post on Zulip Johan Commelin (Jan 14 2021 at 17:32):

there is a branch sset that has this stuff

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 17:32):

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.

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 17:36):

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.

view this post on Zulip Kevin Buzzard (Jan 14 2021 at 17:41):

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

view this post on Zulip Eric Wieser (Jan 14 2021 at 19:31):

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

view this post on Zulip Yakov Pechersky (Jan 14 2021 at 19:33):

That's not exactly right about fin.pred_above


Last updated: May 09 2021 at 22:13 UTC