# Zulip Chat Archive

## 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: Dec 20 2023 at 11:08 UTC