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