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