Reasoning about Fin types

Stream: new members

[Ching-Tsun Chou]

Fin types are driving me crazy. How do I prove the following? Is there a general strategy?

example (n : ℕ) (k : Fin n) : k.succ - 1 = k.castSucc := by sorry

[suhr]

Well, you can always try to do it the ugly way:

example (n : Nat) (k : Fin n) : k.succ - 1 = k.castSucc := by
  match n with
  | .zero => exact k.elim0
  | .succ n =>
  refine Fin.ext ?_
  unfold Fin.castSucc Fin.succ
  simp [Fin.sub_def, OfNat.ofNat, Fin.instOfNat]
  show (n + 1 + 1 - 1 % (n + 1 + 1) + (↑k + 1)) % (n + 1 + 1) = ↑k
  sorry

[Weiyi Wang]

example (n : ℕ) (k : Fin n) : k.succ - 1 = k.castSucc := by
  rw [Fin.ext_iff]
  rw [Fin.coe_sub]
  simp only [Fin.val_one', Fin.val_succ, Fin.coe_castSucc]
  have : 1 % (n + 1) = 1 := by apply Nat.mod_eq_of_lt; simp; exact Fin.pos k
  rw [this]
  simp only [add_tsub_cancel_right]
  have : n + (↑k + 1) = n + 1 + ↑k := by ring
  rw [this]
  rw [Nat.add_mod]
  simp only [Nat.mod_self, zero_add, dvd_refl, Nat.mod_mod_of_dvd, Nat.mod_succ_eq_iff_lt,
    Nat.succ_eq_add_one, gt_iff_lt]
  refine Nat.lt_add_right 1 ?_
  exact k.isLt

My ugly proof with a bunch of apply? help

[Weiyi Wang]

The general I idea I had is to avoid working with Fin by reducing to Nat. The first few lines is to reduce to equality on Nat, and then push the cast inwards. Once it is left with only ↑k, unleash all the theorem/bruteforce available for Nat

[Ching-Tsun Chou]

Thanks about the advice about general strategies! I found the following proof using rw?. I really hope there is a decision procedure for this sort of things.

example (n : ℕ) (k : Fin n) : k.succ - 1 = k.castSucc := by
  rw [sub_eq_iff_eq_add]
  simp

[Ching-Tsun Chou]

Alas, Fin types are still driving me crazy. The following proposition seems so painfully obvious, but I can't figure out how to prove it. My informal reasoning: Fin (↑k + 1 + 1) has at least 2 elements with 0 being the smallest one. ↑↑k + 1 is certainly not 0. So the inequality must hold. But how do I formalize this argument?

example (n : ℕ) (k : Fin n) : (0 : Fin (↑k + 1 + 1)) < ↑↑k + 1 := by sorry

[Aaron Liu]

Have you considered using docs#Fin.last

[Aaron Liu]

You can recover the original lemma by setting (n := ↑k)

import Mathlib

example (n : Nat) : (0 : Fin (n + 1 + 1)) < n + 1 := by
  convert @Fin.last_pos n
  ext
  simp [Fin.val_add]

[Ching-Tsun Chou]

After some trial and error, I finally figured out that the best way to deal with Fin types is to avoid them as much as possible by reformulating my definitions and intermediate results to use Nat instead.

[Malvin Gattinger]

About casting: I noticed in another project that using ▸ to change the Fin type is bad but using docs#Fin.cast is good, in the sense that there are more simp lemmas kicking in.

(This is about working with two differen Fin types, not about converting to Nat.)