Zulip Chat Archive

Stream: new members

Topic: Comm ring for `fin n`


view this post on Zulip Yakov Pechersky (Nov 16 2020 at 16:17):

I've been working on some things that use addition in fin n to keep count of a known finite set. As part of that, I found that I needed zero_add etc. I thought I would add the simple lemmas to data/fin at #5010. But the linter then informed me that the comm_ring definitions do exist, but aren't provided globally as instanced. Why is that? If add and mul are defined for fin, should at least the monoid and add_monoid instanced be made global?

view this post on Zulip Reid Barton (Nov 16 2020 at 16:29):

I don't think you're supposed to use + on fin n--but it exists in order to make numerals work

view this post on Zulip Reid Barton (Nov 16 2020 at 16:34):

if you want mod n arithmetic, there's another type for that; if you want to think of numbers that you know are less than n, then the definition of + isn't really appropriate

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 16:35):

I appreciate the fact that + and even more so * aren't supposed to be used for fin n. But seemingly basic things like 0 + k = k for some k : fin (n + 1) seem to me to be part of what makes numerals work. If one had a statement 0 + 1 = 1 where those numerals were in fin (n + 2), the current way to prove that is to operate on the coercion into nat.

view this post on Zulip Reid Barton (Nov 16 2020 at 16:35):

Is it not true by rfl?

view this post on Zulip Reid Barton (Nov 16 2020 at 16:35):

oh in a variable type, perhaps not

view this post on Zulip Reid Barton (Nov 16 2020 at 16:36):

but why did you have 0 + 1 in the first place?

view this post on Zulip Reid Barton (Nov 16 2020 at 16:38):

It seems like you could avoid that by not adding 0, or using fin.succ

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 16:38):

I see what you mean about not "counting" using fin n. That's where I got the addition from.

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 16:38):

Using fin.succ makes a chain of non-equal types.

view this post on Zulip Reid Barton (Nov 16 2020 at 16:38):

in that case, how about just using nat

view this post on Zulip Reid Barton (Nov 16 2020 at 16:39):

It's good for counting things :upside_down:

view this post on Zulip Reid Barton (Nov 16 2020 at 16:39):

it seems to me that {0,1,,n1}\{0, 1, \ldots, n-1\} isn't something that has an addition that's suitable for counting

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 16:40):

You're right. It was an exploration of first encoding that the maximum of countable elements is n, then counting them, instead of first counting them, then showing there are at most n of them.

view this post on Zulip Reid Barton (Nov 16 2020 at 16:40):

If you use + on fin, then you've introduced some mod which are artificial for the problem you're trying to solve

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 16:40):

And asking, at position i, how many elements have I seen so far?

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 16:40):

foldl (+) 0 ...

view this post on Zulip Yakov Pechersky (Nov 16 2020 at 16:41):

And as you're explaining, everything I'm doing will still make sense in nat, just deferring the boundedness check to the end.

view this post on Zulip Reid Barton (Nov 16 2020 at 16:43):

Basically you have to prove a bound at some point, and you can do it in three ways: at the end; along the way (with a type that changes); or by forcing it with mod, but then it will be hard to reason about the value you defined (and in particular, why mod "never did anything")

view this post on Zulip Kevin Buzzard (Nov 16 2020 at 17:48):

IIRC zmod n is defined to be a type alias for fin n if n>0, and there you have all the ring structure you expect. fin 0 is not a ring which makes doing ringy things on fin n messy.


Last updated: May 15 2021 at 23:13 UTC