how to prove Fin arithmetic

Stream: new members

[Bernardo Anibal Subercaseaux Roa]

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]

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]

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]

Thanks!! I didn't realize that n = 0 made it not be a field :) important corner case...

[Kevin Buzzard]

If you don't want this behaviour then you can use ZMod n which is always a ring

[Bernardo Anibal Subercaseaux Roa]

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]

That sounds fun! Look forward to seeing the result!

[Chris Wong]

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.