Comm ring for `fin n`

Stream: new members

[Yakov Pechersky]

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]

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

[Reid Barton]

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]

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]

Is it not true by rfl?

[Reid Barton]

oh in a variable type, perhaps not

[Reid Barton]

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

[Reid Barton]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Reid Barton]

in that case, how about just using nat

[Reid Barton]

It's good for counting things :upside_down:

[Reid Barton]

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

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

foldl (+) 0 ...

[Yakov Pechersky]

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]

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]

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.