Zulip Chat Archive
Stream: new members
Topic: how to prove Fin arithmetic
Bernardo Anibal Subercaseaux Roa (Jan 30 2025 at 01:27):
Hi, I'm struggling to prove some basic Fin arithmetic like
lemma fin_add_cancel {n : Nat} (u v : Fin n) : u + (v - u) = v := by sorry
what does a short proof for that look like? is there a way of transforming the goal into a goal about Nat's with %
so that tactics like ring_nf
can be used?
Aaron Liu (Jan 30 2025 at 01:40):
This is what I came up with:
import Mathlib.Data.ZMod.Defs
import Mathlib.Tactic.Ring
lemma fin_add_cancel {n : Nat} (u v : Fin n) : u + (v - u) = v := by
match n with
| 0 => exact u.elim0
| n + 1 => ring
If n
is zero then Fin 0
does not form a ring because there is no element 0
. But we are provided with (u : Fin n)
so n
cannot be 0
. If n
is not zero then Fin n
is a CommRing
and ring
can solve it.
Aaron Liu (Jan 30 2025 at 01:55):
Here's a version that converts everything to a Nat
:
import Mathlib.Tactic.Lemma -- apparently the `lemma` syntax is defined in Mathlib
lemma fin_add_cancel {n : Nat} (u v : Fin n) : u + (v - u) = v := by
apply Fin.val_inj.mp
rw [Fin.val_add, /- no `Fin.val_sub`? -/ Fin.sub_def]
/- `rw [Fin.val_mk]` unifies with ↑u here -/
dsimp
rw [Nat.add_mod_mod, ← Nat.add_assoc, Nat.add_sub_of_le (Nat.le_of_lt u.isLt)]
rw [Nat.add_mod_left, Nat.mod_eq_of_lt v.isLt]
Bernardo Anibal Subercaseaux Roa (Jan 30 2025 at 02:34):
Thanks!! I didn't realize that n = 0
made it not be a field :) important corner case...
Kevin Buzzard (Jan 30 2025 at 07:42):
If you don't want this behaviour then you can use ZMod n
which is always a ring
Bernardo Anibal Subercaseaux Roa (Jan 30 2025 at 21:11):
thanks, ZMod n
ended up simplifying my life by a lot; for context, I'm trying to formalize some theorems about vertex transitive graphs, and I was trying to prove an almost trivial statement: cycle graphs are vertex-transitive. The modular arithmetic over Fin n
was being complicated, but everything went away when switching to ZMod n
Chris Wong (Jan 31 2025 at 09:32):
That sounds fun! Look forward to seeing the result!
Chris Wong (Jan 31 2025 at 09:33):
From what I've seen, Fin
is used when you want n
arbitrary labels, or to index into an array. For modular arithmetic indeed ZMod
is superior.
Last updated: May 02 2025 at 03:31 UTC