## Stream: new members

### Topic: Comm ring for fin n

#### 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?

#### 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

#### 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

#### 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.

#### Reid Barton (Nov 16 2020 at 16:35):

Is it not true by rfl?

#### Reid Barton (Nov 16 2020 at 16:35):

oh in a variable type, perhaps not

#### Reid Barton (Nov 16 2020 at 16:36):

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

#### Reid Barton (Nov 16 2020 at 16:38):

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

#### 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.

#### Yakov Pechersky (Nov 16 2020 at 16:38):

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

#### Reid Barton (Nov 16 2020 at 16:38):

in that case, how about just using nat

#### Reid Barton (Nov 16 2020 at 16:39):

It's good for counting things :upside_down:

#### Reid Barton (Nov 16 2020 at 16:39):

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

#### 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.

#### 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

#### Yakov Pechersky (Nov 16 2020 at 16:40):

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

#### Yakov Pechersky (Nov 16 2020 at 16:40):

foldl (+) 0 ...

#### 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.

#### 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")

#### 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